coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/inductive.ml

October 2026

coqbot-app[bot]
Merge PR #22620: Fix recursive-call errors in fixpoint binder types
committed
Thomas Lamiaux
Fix recursive-call errors in fixpoint binder types
committed

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

August 2026

coqbot-app[bot]
Merge PR #22384: Only count uniform arguments that correponds to lambdas
committed
Yann Leray
Count uniform arguments that correponds to lambdas
committed
coqbot-app[bot]
Merge PR #22388: Compute rectrees for cofixpoints in the right environment
committed
Yann Leray
Compute rectrees for cofixpoints in the right environment
committed
coqbot-app[bot]
Merge PR #22392: Forbid recursive calls in nested cofixpoints outside of the main branch
committed
Yann Leray
Forbid recursive calls in nested cofixpoints outside of the main branch
committed

June 2026

coqbot-app[bot]
Merge PR #22127: Fix de Bruijn index bug in inductive_of_mutfix.find_ind
committed
Jason Gross
Fix de Bruijn index bug in find_ind for fixpoint structural argument type
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

May 2026

coqbot-app[bot]
Merge PR #22047: Test for uniform parameters with correct bounds
committed
Yann Leray
Test for uniform parameters with correct bounds
committed
coqbot-app[bot]
Merge PR #22018: Have {find,drop}_uniform_parameters work with mutual fixpoints correctly
committed
coqbot-app[bot]
Merge PR #22022: Always check nested fix lambda domains
committed
Yann Leray
Always check nested fix lambda domains
committed
Yann Leray
Have {find,drop}_uniform_parameters work with mutual fixpoints correctly
committed

April 2026

coqbot-app[bot]
Merge PR #21897: Fix regression that prevented some mutual fixpoints involving nested inductives
committed
Yann Leray
Fix regression that prevented some mutual fixpoints involving nested inductives
committed
coqbot-app[bot]
Merge PR #21854: Have stricter checks in guard conditions
committed
Yann Leray
Stop accepting Metas in guard checker
committed
Yann Leray
Reorder and cleanup in inductive_of_mutfix.find_ind
committed
Yann Leray
Strictify guard environment lookups
committed
Yann Leray
Stop passing stack to projection argument in subterm_specif
committed
Yann Leray
Clean up guard environments in subterm_specif on fixpoints
committed
coqbot-app[bot]
Merge PR #21859: More specific anomalies in contract_case
committed

March 2026

Gaëtan Gilbert
More specific anomalies in contract_case
committed
coqbot-app[bot]
Merge PR #21845: Pass correct environment to reduction in guard checker
committed
Yann Leray
Fix guard environments in subterm_specif on fixpoints
committed
coqbot-app[bot]
Merge PR #21767: Qglobal is not QVar
committed
Gaëtan Gilbert
QGlobal is not QVar
committed
coqbot-app[bot]
Merge PR #21804: Fix anomaly in fix guard check reducing nested cofix
committed
Gaëtan Gilbert
Fix anomaly in fix guard check reducing nested cofix
committed
coqbot-app[bot]
Merge PR #21798: Correctly analyze rec call arguments for uniformity check in the guard.
committed
Pierre-Marie Pédrot
Slightly stricted invariant in uniform guard analysis.
committed
Pierre-Marie Pédrot
Correctly analyze rec call arguments for uniformity check in the guard.
committed
coqbot-app[bot]
Merge PR #21796: Make clearer filter_stack_domain return SArg
committed
Thomas Lamiaux
make clearer filter_stack_domain return SArg
committed
coqbot-app[bot]
Merge PR #21748: Clean up internals of the Inductive module
committed
Pierre-Marie Pédrot
Small simplification in Inductive commutative cut API.
committed
Pierre-Marie Pédrot
Remove the additional expanded tree argument in Inductive.check_cofix.
committed
Pierre-Marie Pédrot
Stop computing arrays for nothing in Inductive.dest_subterms.
committed
Pierre-Marie Pédrot
Remove the cache from the guard checker.
committed
Pierre-Marie Pédrot
Remove redundant check in Inductive.build_recargs.
committed
coqbot-app[bot]
Merge PR #21681: Group all operations on subterms in a single module, simplify on_branches
committed
Yann Leray
Make subterm type private
committed
Yann Leray
Group all operations on subterms in a single module, simplify on_branches
committed