coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/genlambda.ml

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 #21741: Fix forgotten univ subst when inlining in VM/native
committed
Gaëtan Gilbert
Fix forgotten univ subst when inlining in VM/native
committed
coqbot-app[bot]
Merge PR #21679: Optimize a fast-path in Genlambda compilation.
committed

February 2026

Pierre-Marie Pédrot
Optimize a fast-path in Genlambda compilation.
committed

November 2025

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 #21174: Deprecate Names.Label
committed
Gaëtan Gilbert
Deprecate Names.Label
committed

September 2025

coqbot-app[bot]
Merge PR #21073: Use user names to cache computation of inductive case tables in Genlambda
committed
Pierre-Marie Pédrot
Use user names to cache computation of inductive case tables in Genlambda.
committed
coqbot-app[bot]
Merge PR #21031: Slightly better compilation of functional cases in the VM / native.
committed

August 2025

Pierre-Marie Pédrot
Slightly better compilation of functional cases in the VM / native.
committed

June 2025

coqbot-app[bot]
Merge PR #20690: Wrap Lambda nodes in a dummy indirection.
committed

May 2025

Pierre-Marie Pédrot
Wrap Lambda nodes in a dummy indirection.
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

June 2024

coqbot-app[bot]
Merge PR #18973: Add primitive string type.
committed
Rodolphe Lepigre
Statically enforce primitive string size invariant.
committed
Rodolphe Lepigre
Add a primitive string type.
committed

May 2024

coqbot-app[bot]
Merge PR #19014: Track unused constant arguments in Genlambda and erase them.
committed
coqbot-app[bot]
Merge PR #19046: Fix debug printing of Lambda projections.
committed
Pierre-Marie Pédrot
Fix debug printing of Lambda projections.
committed
Pierre-Marie Pédrot
Track unused constant arguments in Genlambda and erase them.
committed
coqbot-app[bot]
Merge PR #19015: Factor the lambda compilation passes of VM and native
committed
Pierre-Marie Pédrot
Restrict lambda remove_let optimization to syntactic values.
committed
Pierre-Marie Pédrot
Use the same optimization passes for the VM and native.
committed
Pierre-Marie Pédrot
Use the same criterion in the VM and native for substitutable atoms.
committed

April 2024

coqbot-app[bot]
Merge PR #18938: Add EConstr.ERelevance abstraction barrier to force normalizing relevances
committed
Gaëtan Gilbert
Add EConstr.ERelevance abstraction barrier to force normalizing relevances
committed
coqbot-app[bot]
Merge PR #18864: Call guard checking with evar handlers in higher layers
committed

March 2024

Gaëtan Gilbert
Monomorphize cclosure.evar_handler
committed
coqbot-app[bot]
Merge PR #18692: Remove the Lforce node from the generic lambda AST.
committed
Pierre-Marie Pédrot
Remove the Lforce node from the generic lambda AST.
committed

February 2024

coqbot-app[bot]
Merge PR #18038: Add rewrite rules to Coq
committed
Yann Leray
Add symbols, patterns, rewrite rule fields
committed

November 2023

coqbot-app[bot]
Merge PR #18331: Fully sort polymorphic inductives
committed
Gaëtan Gilbert
Complex squash API in declarations.mli (not yet used)
committed
coqbot-app[bot]
Merge PR #18340: Fix const_relevance and default qvar handler with sort polymorphism
committed
Gaëtan Gilbert
qvar_irrelevant in default_evar_handler: assert that the qvar is known
committed
Gaëtan Gilbert
Move evar_handler type to cclosure and make evar_handler argument implicit
committed
coqbot-app[bot]
Merge PR #18280: Move relevance outside of case_info
committed
Gaëtan Gilbert
Move relevance outside of case_info
committed
coqbot-app[bot]
Merge PR #17836: Kernel sort polymorphism
committed
Gaëtan Gilbert
Enable variable relevance projections
committed

May 2023

coqbot-app[bot]
Merge PR #17633: Move Termops.decompose_app_vect to EConstr, rename decompose_app->decompose_app_list, decompose_app_vect->decompose_app
committed
Gaëtan Gilbert
Rename decompose_app->decompose_app_list, decompose_app_vect->decompose_app
committed