coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/conversion.ml

October 2026

coqbot-app[bot]
Merge PR #22528: Add constant unfolding heuristic based on definitional heights.
committed
Gaspar Ricci
Add constant unfolding heuristic based on definitional heights. - Behind flag `Kernel Conversion Height Heuristic` - When a constant is defined, its definitional height [h] is computed and stored. This operation is done by the kernel and the height is trusted. Thus, it is computed even when the flag is off. - Over-approximates dependencies between constants. I.e. if [c1] depends on [c2] => h1 > h2. - During conversion, if two constants have the same strategy, the heuristic prefers unfolding the one with greatest height. - When this and the dependency heuristic are active simultaneously, the latter takes over.
committed

August 2026

coqbot-app[bot]
Merge PR #22379: Prune context annotations to remove local defs when they are substituted
committed
coqbot-app[bot]
Merge PR #22393: Use substituted univ instances for convert_branches/convert_return_clause
committed
Gaëtan Gilbert
Use substituted univ instances for convert_branches/convert_return_clause
committed
Yann Leray
Prune context annotations to remove local defs when they are substituted
committed

July 2026

coqbot-app[bot]
Merge PR #22299: Kernel: physical-equality fast paths in conversion's `compare_under`
committed
Valerii Huhnin
kernel: physical-equality fast paths in conversion's compare_under
committed

June 2026

coqbot-app[bot]
Merge PR #19414: Fix FIrrelevant conversion in RR
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

Yann Leray
Add higher-order substitution to CClosure so that rewrite rules don't call term_of_fconstr
committed
coqbot-app[bot]
Merge PR #22002: Rely on user name equality for kernel conversion fast path.
committed
Pierre-Marie Pédrot
Rely on user name equality for kernel conversion fast path.
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

March 2026

coqbot-app[bot]
Merge PR #21688: Fix double substitution in letins from indices in match return clause
committed
Gaëtan Gilbert
Fix double substitution in letins from indices in match return clause
committed
Gaëtan Gilbert
Fix typo in convert_return_clause
committed
coqbot-app[bot]
Merge PR #21696: Fix missing stack conversion for fcaseinvert
committed
coqbot-app[bot]
Merge PR #21695: Fix typo in frel/frel conversion skip_irrelevant_stacks
committed
Gaëtan Gilbert
Fix missing stack conversion for fcaseinvert
committed
Gaëtan Gilbert
Fix typo in frel/frel conversion skip_irrelevant_stacks
committed

February 2026

coqbot-app[bot]
Merge PR #21514: Add Kernel Conversion Dep Heuristic flag for smarter constant unfolding.
committed
Jason Gross
Add Kernel Conversion Dep Heuristic flag for smarter constant unfolding.
committed

January 2026

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
Pierre-Marie Pédrot
More precise type for UVar unification functions.
committed
coqbot-app[bot]
Merge PR #21459: Move sort cumulativity constraint types out of the kernel.
committed
Pierre-Marie Pédrot
Replace QCumulConstraints.t by ElimConstraints.t in kernel internals.
committed

November 2025

coqbot-app[bot]
Merge PR #21272: Instances-mod-elim-constraints
committed
Yann Leray
Conversion mod qgraph
committed
Yann Leray
Instances mod elim (wrong graph)
committed
Yann Leray
Revert qnorm
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
coqbot-app[bot]
Merge PR #21165: Add qnorm function to conversion and cclosure
committed
Yann Leray
Add quality normalisation function to conversion and cclosure
committed

February 2025

coqbot-app[bot]
Merge PR #20165: Export a view type over Environ.env for Serlib and abstract env away.
committed
coqbot-app[bot]
Merge PR #19851: CClosure: absorb arguments in FConstruct
committed

January 2025

Pierre-Marie Pédrot
Abstract away Environ.env.
committed
Gaëtan Gilbert
Stricter code around reduced constructors in conversion
committed
Gaëtan Gilbert
CClosure: absorb arguments in FConstruct
committed

December 2024

coqbot-app[bot]
Merge PR #19853: Perform whd in a separate function in Conversion.eqappr.
committed

November 2024

coqbot-app[bot]
Merge PR #19880: Remove outdated comment in conversion.ml
committed
Gaëtan Gilbert
Remove outdated comment in conversion.ml
committed
Pierre-Marie Pédrot
Perform whd in a separate function in Conversion.eqappr.
committed

October 2024

coqbot-app[bot]
Merge PR #19692: Update the OCaml headers to reflect the fact Coq is now Rocq.
committed