coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/inductive.mli

September 2026

coqbot-app[bot]
Merge PR #22524: Stop relying on CanOrd in Inductive.
committed
Pierre-Marie Pédrot
Stop relying on CanOrd in Inductive.
committed

June 2026

coqbot-app[bot]
Merge PR #22070: Store template inductive data abstracted w.r.t. template levels.
committed
Pierre-Marie Pédrot
Store template inductive data abstracted w.r.t. template levels.
committed

February 2026

coqbot-app[bot]
Merge PR #21450: Add elaboration of qualities
committed
Tomas Diaz
feat: Add elaboration of fresh qualities
committed

January 2026

coqbot-app[bot]
Merge PR #21491: Simplify squashed_gen / allowed_elimination_gen API
committed
Gaëtan Gilbert
Simplify squashed_gen / allowed_elimination_gen API
committed
Gaëtan Gilbert
Minor cleanups around is_squashed_gen
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
Johann Rosain
Rename Constraint(s) to UnivConstraint(s) for a more consistent naming
committed

October 2025

coqbot-app[bot]
Merge PR #20506: An elimination constraint graph to manage elimination of sort variables
committed
Johann Rosain
Use elimination graph at elaboration
committed
Johann Rosain
Use elimination graph to manage elimination in the kernel
committed

April 2025

coqbot-app[bot]
Merge PR #20397: More uniform elimination management
committed
Johann Rosain
Kernel: removal of families, factorisation of elimination
committed

March 2025

coqbot-app[bot]
Merge PR #20303: Induction schemes refresh template universes
committed
Gaëtan Gilbert
Induction schemes refresh template universes
committed
Gaëtan Gilbert
instantiate_template_universes doesn't need a full mind_specif
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
Inductive.param_univs pass the entire default sort instead of the level
committed

January 2025

coqbot-app[bot]
Merge PR #20102: Typecheck pseudo sort poly inductives in kernel using above prop qvar
committed
Gaëtan Gilbert
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 #19970: retype template poly as though sort poly restricted to above_prop
committed
Gaëtan Gilbert
Cleanup "polyprop" / SingletonInductiveBecomesProp
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 #19228: Do not create global constraints for applied template polymorphic types
committed
Gaëtan Gilbert
Fix pretyping of template poly with constraints
committed

June 2024

coqbot-app[bot]
Merge PR #19262: Laxer kernel typing rule for template inductive types.
committed
Pierre-Marie Pédrot
Laxer kernel typing rule for template inductive types.
committed

April 2024

coqbot-app[bot]
Merge PR #18938: Add EConstr.ERelevance abstraction barrier to force normalizing relevances
committed
Gaëtan Gilbert
Add EConstr.ERelevance abstraction barrier to force normalizing relevances
committed
coqbot-app[bot]
Merge PR #18867: Don't make Prop inductives template to control eliminator generation
committed
coqbot-app[bot]
Merge PR #18864: Call guard checking with evar handlers in higher layers
committed
Gaëtan Gilbert
Don't make Prop inductives template to control eliminator generation
committed

March 2024

Gaëtan Gilbert
add ?evars argument to inductive.ml functions
committed

February 2024

coqbot-app[bot]
Merge PR #18038: Add rewrite rules to Coq
committed
Yann Leray
Add kernel (lazy) reduction for rewrite rules
committed
coqbot-app[bot]
Merge PR #18584: Nicer elimination error messages for sort poly inductives
committed

January 2024

Gaëtan Gilbert
Nicer elimination error messages for sort poly inductives
committed

November 2023

coqbot-app[bot]
Merge PR #18331: Fully sort polymorphic inductives
committed
Gaëtan Gilbert
Fully sort polymorphic inductives
committed
Gaëtan Gilbert
Complex squash API in declarations.mli (not yet used)
committed
Gaëtan Gilbert
Remove Inductive.mind_arity (returning rel_context * Sorts.family)
committed
Gaëtan Gilbert
Be compatible with variable relevance inductives
committed
coqbot-app[bot]
Merge PR #18280: Move relevance outside of case_info
committed