coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/nativelib.ml

May 2026

coqbot-app[bot]
Merge PR #22051: Stop using global lazy for temp dir in nativelib
committed
Gaëtan Gilbert
Stop using global lazy for temp dir in nativelib
committed

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

June 2025

coqbot-app[bot]
Merge PR #20704: Stop using "dummy_value" in native compute
committed
Gaëtan Gilbert
Avoid using dummy_value for returning data from native compute
committed

April 2025

coqbot-app[bot]
Merge PR #20376: Improve Boot.Env API and callers
committed

March 2025

Gaëtan Gilbert
Don't call Boot.Env.init in the kernel (native compute)
committed
Gaëtan Gilbert
Nativelib no need for implicit -nI $rocq-runtime/library
committed

February 2025

coqbot-app[bot]
Merge PR #20190: Handle queries in rocqshim when possible
committed
Gaëtan Gilbert
Access Boot.Env.ocamlfind directly instead of through Envars
committed

October 2024

coqbot-app[bot]
Merge PR #19734: Rocqify the core.
committed
Pierre-Marie Pédrot
Rocqify the core.
committed
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

July 2024

coqbot-app[bot]
Merge PR #19314: Fix exception catchalls
committed
Gaëtan Gilbert
Fix exception catchalls
committed

March 2024

coqbot-app[bot]
Merge PR #17392: Add general option -output-directory
committed

February 2024

Hugo Herbelin
Add support for absolute native-output-dir.
committed

June 2022

coqbot-app[bot]
Merge PR #15560: [build] Consolidation of build system infrastructure
committed
Emilio Jesus Gallego Arias
[build] Consolidation of build system infrastructure
committed

May 2022

coqbot-app[bot]
Merge PR #16008: [native compiler] Don't search for coqlib too eagerly.
committed
Emilio Jesus Gallego Arias
[native compiler] Don't search for coqlib too eagerly.
committed

March 2022

coqbot-app[bot]
Merge PR #15769: Fixing small typo in error message
committed
Martin Bodin
typicaly → typically
committed

December 2021

coqbot-app[bot]
Merge PR #15271: Delay removing native_compute .ml files until exit
committed
Gaëtan Gilbert
Delay removing native_compute .ml files until exit
committed

September 2021

coqbot-app[bot]
Merge PR #14059: [build] [tools] Consolidation of directory handling code
committed
Emilio Jesus Gallego Arias
[build] [tools] Consolidation of directory handling code
committed

June 2021

Pierre-Marie Pédrot
Merge PR #14474: [native] Improve error message for ocaml compiler stack overflow
committed
Pierre Roux
[native] Improve error message for ocaml compiler stack overflow
committed

May 2021

Théo Zimmermann
Add examples from former detailed tactic examples chapter to their new location.
committed
coqbot-app[bot]
Merge PR #14225: [build] Some more fixes to Dune-Make bridge + ci-* targets
committed
Emilio Jesus Gallego Arias
[build] Some more fixes to Dune-Make bridge + ci-* targets
committed

April 2021

coqbot-app[bot]
Merge PR #13617: [build] Use dune to build OCaml code.
committed
Emilio Jesus Gallego Arias
[build] Use dune to build OCaml code.
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 #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
coqbot-app[bot]
Merge PR #13193: [build] [native] Don't assume installed native libraries are in custom output path
committed

October 2020

Emilio Jesus Gallego Arias
[build] [native] Don't assume installed native libraries are in custom output path
committed

April 2020

Pierre-Marie Pédrot
Merge PR #12039: Do not erase native files in debug mode
committed
Maxime Dénès
Do not erase native files in debug mode
committed

March 2020

Hugo Herbelin
Merge PR #11559: Remove year in headers.
committed
Théo Zimmermann
Update headers in the whole code base.
committed
Pierre-Marie Pédrot
Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.
committed
Emilio Jesus Gallego Arias
[exninfo] Deprecate aliases for exception re-raising.
committed