coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/nativecode.ml

October 2026

coqbot-app[bot]
Merge PR #22542: Replace and deprecate the aliased _env variants of Names sets and maps
committed

September 2026

Pierre-Marie Pédrot
Use the now correct set and maps Names APIs.
committed
coqbot-app[bot]
Merge PR #22399: Make Nativecode.string_of_kn really injective for good.
committed

August 2026

Pierre-Marie Pédrot
Make Nativecode.string_of_kn really injective for good.
committed

June 2026

coqbot-app[bot]
Merge PR #22108: Cleanup of the file kernel/nativecode.ml
committed
Elliott
removed a useless semicolon that could cause confusion
committed
Elliott
removed a useless if statement (in a branch where the condition is known) and made simplifications allowed by this removal.
committed

January 2026

coqbot-app[bot]
Merge PR #21533: Stop exposing implementation internals in Environ API.
committed
Pierre-Marie Pédrot
Stop exposing implementation internals in Environ API.
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
coqbot-app[bot]
Merge PR #21449: Centralize the Nativenorm global state in a reference-passed record
committed
Pierre-Marie Pédrot
Pass Nativecode symbols by reference.
committed
Pierre-Marie Pédrot
Pass Nativecode.global_stack by reference rather than globally.
committed
Pierre-Marie Pédrot
Move various native code counters to the local state.
committed
Pierre-Marie Pédrot
Move the Nativecode name counter to the local state.
committed
Pierre-Marie Pédrot
Centralize the Nativenorm global state in a reference-passed record.
committed

December 2025

coqbot-app[bot]
Merge PR #21411: Split sort substitution from accumulator construction in native compilation
committed
Pierre-Marie Pédrot
Split sort substitution from accumulator construction in native compilation.
committed
coqbot-app[bot]
Merge PR #21409: Fix native conversion of polymorphic code after #21405.
committed
Pierre-Marie Pédrot
Fix native conversion of polymorphic code after #21405.
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
coqbot-app[bot]
Merge PR #21140: Use user equality in comparison of native values.
committed

September 2025

Pierre-Marie Pédrot
Use user equality in comparison of native values.
committed
coqbot-app[bot]
Merge PR #21069: Declarations support mixed record/nonrecord inductive blocks
committed
Gaëtan Gilbert
Declarations support mixed record/nonrecord inductive blocks
committed
coqbot-app[bot]
Merge PR #21049: Check correctness of canonical constant and inductive names when typing.
committed
Pierre-Marie Pédrot
Store canonical constant and inductive names explicitly in environments.
committed
coqbot-app[bot]
Merge PR #20910: Move Obj.magic outside mk_cofix_accu
committed

July 2025

Gaëtan Gilbert
Move Obj.magic outside mk_cofix_accu
committed

June 2025

coqbot-app[bot]
Merge PR #20719: Tweak the native compilation scheme of cofixpoints.
committed
Gaëtan Gilbert
Nicer formatting of output native code
committed
coqbot-app[bot]
Merge PR #20696: nativecode don't generate forcecofix for non coinductive primproj
committed
Pierre-Marie Pédrot
Tweak the native compilation scheme of cofixpoints.
committed
Gaëtan Gilbert
nativecode don't generate forcecofix for non coinductive primproj
committed
Gaëtan Gilbert
nativevalues don't put finiteness info in annot_sw
committed
coqbot-app[bot]
Merge PR #20704: Stop using "dummy_value" in native compute
committed
coqbot-app[bot]
Merge PR #20703: Nativecode factorize restarting envs
committed
Gaëtan Gilbert
Avoid using dummy_value for returning data from native compute
committed
Gaëtan Gilbert
Nativecode.get_symbols avoid using dummy_value
committed
Gaëtan Gilbert
Nativecode factorize restarting envs
committed
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