coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/declareops.ml

October 2026

coqbot-app[bot]
Merge PR #22528: Add constant unfolding heuristic based on definitional heights.
committed
Gaspar Ricci
Add constant unfolding heuristic based on definitional heights. - Behind flag `Kernel Conversion Height Heuristic` - When a constant is defined, its definitional height [h] is computed and stored. This operation is done by the kernel and the height is trusted. Thus, it is computed even when the flag is off. - Over-approximates dependencies between constants. I.e. if [c1] depends on [c2] => h1 > h2. - During conversion, if two constants have the same strategy, the heuristic prefers unfolding the one with greatest height. - When this and the dependency heuristic are active simultaneously, the latter takes over.
committed

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

June 2026

coqbot-app[bot]
Merge PR #22128: Tiny simplification in declareops inductive_make_projections
committed
Gaëtan Gilbert
Tiny simplification in declareops inductive_make_projections
committed
coqbot-app[bot]
Merge PR #22114: Remove the name field from projections.
committed
Pierre-Marie Pédrot
Remove the name field from projections.
committed

May 2026

coqbot-app[bot]
Merge PR #21994: Minor code factorization in Declareops.
committed
Pierre-Marie Pédrot
Minor code factorization in Declareops.
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 #21677: Improved handling of disabled VM
committed
Gaëtan Gilbert
VM error when encountering non compiled constant (from disabled VM)
committed
Gaëtan Gilbert
More robust handling of env typing flags wrt configure VM/native disabling
committed
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
coqbot-app[bot]
Merge PR #21774: Track inductives that depend on indices not mattering
committed
Gaëtan Gilbert
Fix has_dependent_elim to handle postponed eta
committed
Jason Gross
Track inductives that depend on indices not mattering
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

February 2026

coqbot-app[bot]
Merge PR #21514: Add Kernel Conversion Dep Heuristic flag for smarter constant unfolding.
committed
Jason Gross
Add Kernel Conversion Dep Heuristic flag for smarter constant unfolding.
committed
coqbot-app[bot]
Merge PR #21531: Only allow universe level comparisons to fail with type-in-type
committed
Yann Leray
Add ignore_elimination_constraints typing flag
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

December 2025

coqbot-app[bot]
Merge PR #21195: Add parsing and interpretation of elimination constraints
committed
Johann Rosain
Add support for parsing elimination constraints
committed

September 2025

coqbot-app[bot]
Merge PR #21069: Declarations support mixed record/nonrecord inductive blocks
committed
Gaëtan Gilbert
Declarations support mixed record/nonrecord inductive blocks
committed
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

March 2025

coqbot-app[bot]
Merge PR #20344: Hashconsing try to avoid recomputing hashes
committed
Gaëtan Gilbert
Hashconsing try to avoid recomputing hashes
committed

February 2025

coqbot-app[bot]
Merge PR #20178: Keep qvar in template poly entry and declarations
committed
Gaëtan Gilbert
Kernel keep qvar information for template inductives
committed
Gaëtan Gilbert
Remove separation between RegularArity and TemplateArity
committed

January 2025

coqbot-app[bot]
Merge PR #20152: Small cleanups around inductive_arity
committed
Gaëtan Gilbert
inline map_decl_arity in hcons_ind_arity
committed
coqbot-app[bot]
Merge PR #19985: Stop using lbound:Prop
committed
Gaëtan Gilbert
Stop using lbound:Prop in higher layers
committed
coqbot-app[bot]
Merge PR #20102: Typecheck pseudo sort poly inductives in kernel using above prop qvar
committed
Gaëtan Gilbert
Kernel interface for template poly says whether it's pseudo sort poly
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