coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/indTyping.ml

September 2026

coqbot-app[bot]
Merge PR #22516: Stop performing universe abstraction in the kernel
committed
Pierre-Marie Pédrot
Extrude universe abstraction of inductive types out of the kernel.
committed
Pierre-Marie Pédrot
Do not rely on unsubstituted instances in inductive variance analysis.
committed

July 2026

coqbot-app[bot]
Merge PR #22150: Reduce definitional UIP pattern matching when the global return type is convertible with the type in the (unique) branch
committed

June 2026

nicolas tabareau
avoid letins in indices
committed
coqbot-app[bot]
Merge PR #22176: Centralize bound universe computation in inductive types
committed
Pierre-Marie Pédrot
Centralize substitution of bound universes in inductive typing.
committed
Pierre-Marie Pédrot
Extrude substitution of template computation in IndTyping.
committed
Pierre-Marie Pédrot
Minor code reorganization in IndTyping.
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
Pierre-Marie Pédrot
Preserve bound universe names in template inductive types.
committed
Pierre-Marie Pédrot
Do not return the inductive entry in IndTyping.get_template.
committed

May 2026

coqbot-app[bot]
Merge PR #21952: Always provide primitive eta when `check_eliminations` is disabled
committed
Kanghee Park
Give primitive eta when elimination checks are disabled
committed

March 2026

coqbot-app[bot]
Merge PR #21767: Qglobal is not QVar
committed
Gaëtan Gilbert
QGlobal is not QVar
committed
coqbot-app[bot]
Merge PR #21785: Records in constant sort can have postponed eta (with proj in variable sort)
committed
Gaëtan Gilbert
Records in constant sort can have postponed eta (with proj in variable sort)
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 #21760: Simplify and fix Indtyping.compute_elim_squash
committed
Gaëtan Gilbert
Fix declaring inductive in impredicative Set with large arguments
committed
Gaëtan Gilbert
Simplify Indtyping.compute_elim_squash
committed

February 2026

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
Yann Leray
Only allow universe level comparisons to fail with type-in-type
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 #21501: Various fixes around bound universe instances in kernel and checker
committed
Pierre-Marie Pédrot
Add missing checks for sort binders in kernel.
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
coqbot-app[bot]
Merge PR #21486: Remove the coupling between sort constraint addition and rigidity check
committed
Pierre-Marie Pédrot
Move the quality checks of Environ.push_context to the callers.
committed

December 2025

coqbot-app[bot]
Merge PR #21391: Reintroduce Univ.ContextSet.t and fix kernel APIs to use it
committed
Pierre-Marie Pédrot
Fix kernel APIs to take Univ.ContextSet rather than the PConstraints one.
committed
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 to manage elimination in the kernel
committed

April 2025

coqbot-app[bot]
Merge PR #20496: Use record instead of tuple for UVars.bound_names
committed
Soudant
Changed bound_names from product to record, with fields quals (for qualities) and univs (for universes),
committed
coqbot-app[bot]
Merge PR #20397: More uniform elimination management
committed
Johann Rosain
Kernel: removal of families, factorisation of elimination
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