coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/cClosure.ml

October 2026

coqbot-app[bot]
Merge PR #22527: Do not use -unbox-closures
committed
Jan-Oliver Kaiser
Lift big closures to reduce memory consumption
committed

August 2026

coqbot-app[bot]
Merge PR #22381: Fix reification of FCase(Invert) in cclosure
committed
Gaëtan Gilbert
Fix reification of FCase(Invert) in cclosure
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
remove pattern-matching when the return types are convertible
committed
coqbot-app[bot]
Merge PR #19414: Fix FIrrelevant conversion in RR
committed
coqbot-app[bot]
Merge PR #22090: Abstract the val variant of context datatypes.
committed
Pierre-Marie Pédrot
Abstract the val variant of context datatypes.
committed

May 2026

Yann Leray
Add higher-order substitution to CClosure so that rewrite rules don't call term_of_fconstr
committed
coqbot-app[bot]
Merge PR #22032: Laxer normal form criterion for strong kernel normalization.
committed
Pierre-Marie Pédrot
Laxer normal form criterion for strong kernel normalization.
committed
coqbot-app[bot]
Merge PR #21973: Clean up function CClosure.get_branch
committed

April 2026

Yann Leray
Clean up function CClosure.get_branch
committed
coqbot-app[bot]
Merge PR #21972: Remove double universe substitution in branches
committed
Yann Leray
Remove double universe substitution in branches
committed
coqbot-app[bot]
Merge PR #21864: Remove calls to CanOrd module in rewrite rule CClosure implementation.
committed
Pierre-Marie Pédrot
Remove calls to CanOrd module in rewrite rule CClosure implementation.
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 #21767: Qglobal is not QVar
committed
Gaëtan Gilbert
QGlobal is not QVar
committed
coqbot-app[bot]
Merge PR #21806: Remove unused has_eta output of inductive_make_projections
committed
Gaëtan Gilbert
Remove unused has_eta output of inductive_make_projections
committed
coqbot-app[bot]
Merge PR #21792: Fix has_dependent_elim to handle postponed eta
committed
Gaëtan Gilbert
Fix has_dependent_elim to handle postponed eta
committed
coqbot-app[bot]
Merge PR #21698: Fix missing univ subst of array instance in lazy
committed
Gaëtan Gilbert
Fix missing univ subst of array instance in lazy
committed
coqbot-app[bot]
Merge PR #21697: Fix missing relevance substitution for fprod
committed
Gaëtan Gilbert
Fix missing relevance substitution for fprod
committed

February 2026

coqbot-app[bot]
Merge PR #21612: Remove unnecessary type annotations (4.14)
committed
Yann Leray
Remove unnecessary type annotations (4.14)
committed
coqbot-app[bot]
Merge PR #21606: cclosure less polymorphic types for rewrite rules
committed
Gaëtan Gilbert
cclosure less polymorphic types for rewrite rules
committed

January 2026

coqbot-app[bot]
Merge PR #21416: feat: Allow primitive projections with postponed eta (sort poly)
committed
coqbot-app[bot]
Merge PR #21508: Stop unifying sorts in the kernel.
committed
Pierre-Marie Pédrot
Simplify quality APIs that do not require a QGraph anymore.
committed
Pierre-Marie Pédrot
Stop unifying sorts in the kernel.
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

December 2025

coqbot-app[bot]
Merge PR #21354: Add printer for lift through a new type of weakenings
committed
Yann Leray
Add documentation for CClosure.to_constr and overhaul documentation for esubst lifts
committed

November 2025

coqbot-app[bot]
Merge PR #21272: Instances-mod-elim-constraints
committed
Yann Leray
Revert qnorm
committed
coqbot-app[bot]
Merge PR #21284: Reimplement abstract in a purely functional way.
committed
Pierre-Marie Pédrot
Reimplement abstract in a purely functional way.
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