coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/declarations.mli

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

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
coqbot-app[bot]
Merge PR #21774: Track inductives that depend on indices not mattering
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 #21663: Support for matching global sorts
committed
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
Yann Leray
Support for matching global sorts
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 #21416: feat: Allow primitive projections with postponed eta (sort poly)
committed
Tomas
feat: Allow prim projections with postponed eta conversion (sort poly)
committed
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

October 2025

coqbot-app[bot]
Merge PR #21174: Deprecate Names.Label
committed
Gaëtan Gilbert
Deprecate Names.Label
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

July 2025

coqbot-app[bot]
Merge PR #20140: Changes towards a proper RR typechecker
committed

June 2025

Yann Leray
Fix and rename machine_rewrite_rule
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
Monomorphize Declarations.declaration_arity
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 #20061: Remove unused module-related API.
committed
Pierre-Marie Pédrot
Remove unused module-related API.
committed
coqbot-app[bot]
Merge PR #19995: Abstract away the representation of module-related types
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

September 2024

coqbot-app[bot]
Merge PR #19509: Compare projections by repr name in RRs
committed
Yann Leray
Compare projections by repr name in RRs
committed

June 2024

coqbot-app[bot]
Merge PR #19233: template_universes don't duplicate level data
committed
Gaëtan Gilbert
template_universes don't duplicate level data
committed
coqbot-app[bot]
Merge PR #18973: Add primitive string type.
committed
Rodolphe Lepigre
Add a primitive string type.
committed

April 2024

coqbot-app[bot]
Merge PR #18800: Allow matching on quality instances
committed