coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/nativecode.mli

January 2026

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
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

October 2025

coqbot-app[bot]
Merge PR #21174: Deprecate Names.Label
committed
Gaëtan Gilbert
Deprecate Names.Label
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

April 2024

coqbot-app[bot]
Merge PR #18883: Mark arrays, products, and plain constants, as potentially needing a delayed evaluation during native_compute (fix #18703).
committed
Guillaume Melquiond
Mark arrays, products, and plain constants, as potentially needing a delayed evaluation during native_compute (fix #18703).
committed

February 2024

coqbot-app[bot]
Merge PR #17674: Store VM bytecode in a dedicated vo segment
committed
Pierre-Marie Pédrot
Generalize the type of constant bodies.
committed
coqbot-app[bot]
Merge PR #18038: Add rewrite rules to Coq
committed
Yann Leray
Add minimal support for native and checker for rewrite rules
committed

November 2023

coqbot-app[bot]
Merge PR #17836: Kernel sort polymorphism
committed
Gaëtan Gilbert
sort poly (with simple squashing model and no inductive output in qsort)
committed

October 2023

coqbot-app[bot]
Merge PR #18198: Remove unused constructors in nativecode
committed
Gaëtan Gilbert
Remove unused constructors in nativecode
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 #16671: Share the VM and native lambda AST in a single type.
committed

October 2022

Pierre-Marie Pédrot
Share the VM and native lambda AST in a single type.
committed

June 2021

Pierre-Marie Pédrot
Merge PR #14417: Move cooking types to Declarations from Opaqueproof
committed
Gaëtan Gilbert
Move cooking_info from Opaqueproof to Declarations
committed

May 2021

Théo Zimmermann
Add examples from former detailed tactic examples chapter to their new location.
committed

March 2021

coqbot-app[bot]
Merge PR #13956: Remove useless prefix argument in native compilation.
committed
Pierre-Marie Pédrot
Remove useless prefix argument in native compilation.
committed

February 2021

Pierre-Marie Pédrot
Merge PR #13853: Delay the dynamic linking of native-code libraries until native_compute is called.
committed
Guillaume Melquiond
Delay the dynamic linking of native-code libraries until native_compute is called (fix #13849).
committed
coqbot-app[bot]
Merge PR #13202: Infrastructure for fine-grained debug flags
committed
Maxime Dénès
Infrastructure for fine-grained debug flags
committed

November 2020

coqbot-app[bot]
Merge PR #13358: Merge the Linked / LinkedInteractive native link information constructors
committed
Pierre-Marie Pédrot
Statically ensure that native update locations are of form Linked*.
committed
coqbot-app[bot]
Merge PR #13297: Remove the native symbol registering from the safe environment.
committed
Pierre-Marie Pédrot
Remove the native symbol registering from the safe environment.
committed

March 2020

Hugo Herbelin
Merge PR #11559: Remove year in headers.
committed
Théo Zimmermann
Update headers in the whole code base.
committed

July 2019

Maxime Dénès
Merge PR #10359: Remove dependency of native_compile on global env for symbols
committed

June 2019

Clément Pit-Claudel
Merge PR #10320: Update headers to the new year.
committed
Théo Zimmermann
Update ml-style headers to new year.
committed
Gaëtan Gilbert
Move type definition Nativecode.symbols to Nativevalues
committed

May 2019

Talia Ringer
Merge remote-tracking branch 'origin/master' into stm+doc_hook
committed
Gaëtan Gilbert
Merge PR #10174: Further cleanup of the side-effect machinery
committed
Pierre-Marie Pédrot
Parameterize the constant_body type by opaque subproofs.
committed

July 2018

Pierre-Marie Pédrot
Merge PR #7746: Many small cleanups removing unused arguments and functions
committed
Gaëtan Gilbert
Nativecode compile_mind, compile_mind_field: remove unused arguments
committed

June 2018

Maxime Dénès
Merge PR #7679: Clean native compilation of primitive projections
committed
Pierre-Marie Pédrot
More straightforward native compilation of primitive projections.
committed

May 2018

Pierre-Marie Pédrot
Merge PR #7521: Fix soundness bug with VM/native and cofixpoints
committed
Maxime Dénès
Unify pre_env and env
committed