coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/nativelambda.ml

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

January 2025

coqbot-app[bot]
Merge PR #19990: VM/native: primitive strings can be included in values
committed
Gaëtan Gilbert
VM/native: primitive strings can be included in values
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

May 2024

coqbot-app[bot]
Merge PR #19015: Factor the lambda compilation passes of VM and native
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

March 2024

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 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
Pierre-Marie Pédrot
Move prefix-related code from Nativelambda to Nativecode.
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
Remove Lproj from the set of substitutible values in native.
committed
Pierre-Marie Pédrot
Additional sharing of some lambda code.
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
Pierre-Marie Pédrot
Simplify the case annotation type stored in native lambda AST.
committed
Pierre-Marie Pédrot
Tweak the Lproj native constructor to look like the VM one.
committed
Pierre-Marie Pédrot
Remove the unused Lif constructor from Nativelambda.lambda.
committed
Pierre-Marie Pédrot
Remove the unused Lrec constructor from Nativelambda.lambda.
committed
Pierre-Marie Pédrot
Move the prefix computation from lambda phase to code in native compiler.
committed

September 2022

coqbot-app[bot]
Merge PR #16442: Introduce a dedicated type for evar instances.
committed
Pierre-Marie Pédrot
Introduce a dedicated type for evar instances.
committed
coqbot-app[bot]
Merge PR #16480: Generalize kernel evar handling
committed
Pierre-Marie Pédrot
Wrap the evar expander type into an explicit record.
committed

May 2022

coqbot-app[bot]
Merge PR #16017: Cleanup of native compilation
committed
Pierre-Marie Pédrot
Fix the compilation of lazy values in native compiler.
committed

May 2021

coqbot-app[bot]
Merge PR #14337: Remove the delayed name substitution mechanism from the kernel
committed
Théo Zimmermann
Add examples from former detailed tactic examples chapter to their new location.
committed
Pierre-Marie Pédrot
Remove the useless to_patch_substituted indirection.
committed
Pierre-Marie Pédrot
Eagerly perform substitution in constant bodies.
committed

March 2021

coqbot-app[bot]
Merge PR #14007: Never store persistent arrays as VM structured values.
committed
Pierre-Marie Pédrot
Similar fix for native compilation.
committed

January 2021

coqbot-app[bot]
Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)
committed
Pierre-Marie Pédrot
Change the representation of kernel case.
committed

December 2020

coqbot-app[bot]
Merge PR #13537: More efficient implementation for substitutions.
committed
Pierre-Marie Pédrot
Optimization: take advantage that we don't use arrays anymore in substitutions.
committed

November 2020

coqbot-app[bot]
Merge PR #13358: Merge the Linked / LinkedInteractive native link information constructors
committed
Pierre-Marie Pédrot
Merge the Linked and LinkedInteractive constructors.
committed

October 2020

coqbot-app[bot]
Merge PR #13075: Introducing the foundations for a name-alias-agnostic API
committed