coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/genlambda.mli

September 2026

coqbot-app[bot]
Merge PR #22435: Remove dead API from Genlambda.
committed
Pierre-Marie Pédrot
Remove dead API from Genlambda.
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

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
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
Remove some cruft from the Genlambda API.
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

November 2023

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

November 2022

coqbot-app[bot]
Merge PR #16692: Remove the support of metavariables from native and VM compilation.
committed
Pierre-Marie Pédrot
Remove the support of metavariables from native and VM compilation.
committed
coqbot-app[bot]
Merge PR #16780: Share the Lambda code generation phase in VM and native compilation
committed
Pierre-Marie Pédrot
Factorize the lambda_of_constr function in Genlambda.
committed
Pierre-Marie Pédrot
Factorize the makeblock function in Genlambda.
committed
Pierre-Marie Pédrot
Factorize the expand_constructor function in Genlambda.
committed
coqbot-app[bot]
Merge PR #16671: Share the VM and native lambda AST in a single type.
committed

October 2022

Pierre-Marie Pédrot
Additional sharing of some lambda code.
committed
Pierre-Marie Pédrot
Move remove_let from Vlambda to Genlambda.
committed
Pierre-Marie Pédrot
Carefully share the simplify operation in Genlambda.
committed
Pierre-Marie Pédrot
Share some utility functions on the Genlambda type.
committed
Pierre-Marie Pédrot
Share the VM and native lambda AST in a single type.
committed