coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/declareops.mli

September 2026

coqbot-app[bot]
Merge PR #22516: Stop performing universe abstraction in the kernel
committed
Pierre-Marie Pédrot
Extrude universe abstraction of general definitions out of the kernel.
committed

April 2026

coqbot-app[bot]
Merge PR #21901: Do not store recursive trees anymore in inductive blocks.
committed
Pierre-Marie Pédrot
Do not store recursive trees anymore in inductive blocks.
committed

March 2026

coqbot-app[bot]
Merge PR #21806: Remove unused has_eta output of inductive_make_projections
committed
Gaëtan Gilbert
Remove unused has_eta output of inductive_make_projections
committed
coqbot-app[bot]
Merge PR #21792: Fix has_dependent_elim to handle postponed eta
committed
Gaëtan Gilbert
Fix has_dependent_elim to handle postponed eta
committed
coqbot-app[bot]
Merge PR #21666: Use automata rather than regular trees for guard checking.
committed
Pierre-Marie Pédrot
Store inductive automata next to their regular tree in Declarations.
committed

January 2026

coqbot-app[bot]
Merge PR #21438: feat: Allow primitive projections with postponed eta (no sort poly)
committed
Tomas Diaz
feat: Allow primitive projections with postponed eta
committed

September 2025

coqbot-app[bot]
Merge PR #21067: Remove redundant mind_ntypes field of mind_body
committed
Gaëtan Gilbert
Remove redundant mind_ntypes field of mind_body
committed

January 2025

coqbot-app[bot]
Merge PR #20152: Small cleanups around inductive_arity
committed
Gaëtan Gilbert
Stop exporting Declareops.map_decl_arity
committed
coqbot-app[bot]
Merge PR #19995: Abstract away the representation of module-related types
committed
Pierre-Marie Pédrot
Consolidate the module hashconsing functions in Mod_declarations.
committed
Pierre-Marie Pédrot
Move the module-related definitions from Declarations to a new module.
committed

December 2024

coqbot-app[bot]
Merge PR #19943: GADT-based representation of module / module types.
committed
Pierre-Marie Pédrot
GADT-based representation of module / module types.
committed

October 2024

coqbot-app[bot]
Merge PR #19692: Update the OCaml headers to reflect the fact Coq is now Rocq.
committed
Pierre-Marie Pédrot
Update the OCaml headers to reflect the fact Coq is now Rocq.
committed

July 2024

coqbot-app[bot]
Merge PR #19160: Avoid retypechecking repeated subterms in typeops
committed
Gaëtan Gilbert
Try to reuse partial hashconsing for definition bodies
committed

February 2024

coqbot-app[bot]
Merge PR #17674: Store VM bytecode in a dedicated vo segment
committed
Pierre-Marie Pédrot
Generalize the type of constant bodies.
committed
coqbot-app[bot]
Merge PR #18038: Add rewrite rules to Coq
committed
Yann Leray
Apply review suggestions
committed

November 2023

coqbot-app[bot]
Merge PR #18241: Simplify the encoding of the recursive disjunctive-conjunctive structure of (co)inductive types in rtree.ml by taking nodes of arrays of arrays
committed
coqbot-app[bot]
Merge PR #17836: Kernel sort polymorphism
committed
Gaëtan Gilbert
Enable variable relevance projections
committed
Gaëtan Gilbert
sort poly (with simple squashing model and no inductive output in qsort)
committed
Gaëtan Gilbert
Move universe polymorphism APIs to new file UVars before sort poly
committed
Hugo Herbelin
Node of arrays of arrays in rtree.ml so as to save tricky encodings.
committed

April 2022

coqbot-app[bot]
Merge PR #15954: Declareops.inductive_make_projection doesn't return option
committed
Gaëtan Gilbert
Declareops.inductive_make_projection doesn't return option
committed

July 2021

coqbot-app[bot]
Merge PR #14654: A few terminology changes in module names of the universe API
committed
Hugo Herbelin
Renaming Univ.AUContext into Univ.AbstractContext.
committed

June 2021

Pierre-Marie Pédrot
Merge PR #14417: Move cooking types to Declarations from Opaqueproof
committed
Gaëtan Gilbert
Move cooking_info from Opaqueproof to Declarations
committed

July 2020

Pierre-Marie Pédrot
Merge PR #11604: Primitive persistent arrays
committed
Maxime Dénès
Primitive persistent arrays
committed

March 2020

Hugo Herbelin
Merge PR #11559: Remove year in headers.
committed
Théo Zimmermann
Update headers in the whole code base.
committed

June 2019

Clément Pit-Claudel
Merge PR #10320: Update headers to the new year.
committed
Théo Zimmermann
Update ml-style headers to new year.
committed

May 2019

Talia Ringer
Merge remote-tracking branch 'origin/master' into stm+doc_hook
committed
Gaëtan Gilbert
Merge PR #10174: Further cleanup of the side-effect machinery
committed
Pierre-Marie Pédrot
Parameterize the constant_body type by opaque subproofs.
committed