coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/indtypes.ml

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 #22114: Remove the name field from projections.
committed
Pierre-Marie Pédrot
Remove the name field from projections.
committed
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

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 #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 #21600: Do not introduce recursive rtrees for non-recursive nesting inductive types
committed
Pierre-Marie Pédrot
Do not introduce recursive rtrees for non-recursive nesting inductive types.
committed
coqbot-app[bot]
Merge PR #21593: Stronger invariants in recursive tree computation in Indtypes
committed
Pierre-Marie Pédrot
More precise type for rtree environments in Indtypes.
committed
Pierre-Marie Pédrot
Invariant in Indtypes rtree environment.
committed
Pierre-Marie Pédrot
Enforce that Norec nodes are always associated to norec in Indtypes.
committed
Pierre-Marie Pédrot
Introduce a dedicated type for recursive environment nodes in Indtypes.
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

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

February 2025

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

January 2025

coqbot-app[bot]
Merge PR #20026: Rename Coq -> Rocq in various comments and doc
committed
Pierre Roux
Rename Coq -> Rocq in various comments and doc
committed
coqbot-app[bot]
Merge PR #19988: More informative print for inductive missing constraints error
committed
Gaëtan Gilbert
Have an env for every inductive_error
committed

November 2024

coqbot-app[bot]
Merge PR #19831: When a record cannot be declared with primitive projections, explain why
committed
Gaëtan Gilbert
When a record cannot be declared with primitive projections, explain why
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 #19528: Allow levels not mentioned in the conclusion to be template (typically `eq` is now template poly)
committed
Gaëtan Gilbert
Allow levels not mentioned in the conclusion to be template
committed

January 2024

coqbot-app[bot]
Merge PR #18229: The kernel does not care about whether a subtype of an inductive type is nested or not
committed

December 2023

Hugo Herbelin
Merging Mrec and Nested(NestedInd) which behave the same kernel-wise.
committed
Hugo Herbelin
Indtypes: better locality and control of a List.nth failure.
committed

November 2023

coqbot-app[bot]
Merge PR #18331: Fully sort polymorphic inductives
committed
Gaëtan Gilbert
Declarations.mind_kelim : family ==> mind_squashed : bool
committed
Gaëtan Gilbert
Be compatible with variable relevance inductives
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

July 2023

coqbot-app[bot]
Merge PR #17830: A small potpourri of miscellaneous typos, reformatting, renaming
committed