coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of kernel/nativelib.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

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

January 2025

coqbot-app[bot]
Merge PR #20026: Rename Coq -> Rocq in various comments and doc
committed
Pierre Roux
Rename Coq -> Rocq in various comments and doc
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 2021

Théo Zimmermann
Add examples from former detailed tactic examples chapter to their new location.
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

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

March 2020

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

February 2020

Maxime Dénès
Merge PR #11581: [native compiler] Add options to set object directories.
committed
Emilio Jesus Gallego Arias
[native compiler] Allow to set OCaml include dirs for compilation
committed
Emilio Jesus Gallego Arias
[native compiler] Allow to set the output directory for cmx objects
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
Remove dependency of native_compile on global env for symbols
committed

April 2019

Emilio Jesus Gallego Arias
Merge PR #9898: Better error message when OCaml compiler not found for native compute
committed
Emilio Jesus Gallego Arias
[doc] [kernel] Add docstrings for native interface functions.
committed
Maxime Dénès
Better error message when OCaml compiler not found for native compute
committed

March 2018

Maxime Dénès
Merge PR #6855: Update headers following #6543.
committed

February 2018

Théo Zimmermann
Update headers following #6543.
committed

November 2017

Maxime Dénès
Merge PR #6065: [api] Deprecate all legacy uses of Names in core.
committed
Emilio Jesus Gallego Arias
[api] Deprecate all legacy uses of Names in core.
committed

August 2017

Maxime Dénès
Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170
committed
Paul Steckler
Add native compute profiling, BZ#5170
committed

July 2017

Pierre-Marie Pédrot
Bump year in headers.
committed

June 2017

Maxime Dénès
Merge PR#713: Bump year in headers.
committed
Maxime Dénès
Bump year in headers.
committed

April 2016

Pierre Courtieu
Merge remote-tracking branch 'OFFICIAL/trunk' into morefresh
committed

January 2016

Pierre-Marie Pédrot
Merge branch 'v8.5'
committed
Maxime Dénès
Update copyright headers.
committed

January 2015

Maxime Dénès
Merge branch 'v8.5' into trunk
committed
Maxime Dénès
Make -print-mod-uid accept a list of files.
committed
Maxime Dénès
Update headers.
committed

December 2014

Maxime Dénès
Fix for #3154: use CUnix.sys_command to call native compiler.
committed

May 2014

Guillaume Melquiond
Fix native_compute for systems with a limited size for the command line.
committed

April 2014

Maxime Dénès
Native compiler: hide compiled files in a .coq-native subdirectory.
committed

March 2014

Pierre Letouzey
Remove many superfluous 'open' indicated by ocamlc -w +33
committed

January 2013

mdenes
New implementation of the conversion test, using normalization by evaluation to native OCaml code.
committed