index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
nativelib.mli
Age
Commit message (
Expand
)
Author
2020-11-09
Remove the native symbol registering from the safe environment.
Pierre-Marie Pédrot
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-02-26
[native compiler] Allow to set OCaml include dirs for compilation
Emilio Jesus Gallego Arias
2020-02-26
[native compiler] Allow to set the output directory for cmx objects
Emilio Jesus Gallego Arias
2019-07-04
Merge PR #10359: Remove dependency of native_compile on global env for symbols
Maxime Dénès
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-12
Remove dependency of native_compile on global env for symbols
Gaëtan Gilbert
2019-04-16
[doc] [kernel] Add docstrings for native interface functions.
Emilio Jesus Gallego Arias
2019-04-16
Better error message when OCaml compiler not found for native compute
Maxime Dénès
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-08-17
Add native compute profiling, BZ#5170
Paul Steckler
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-01-15
Make -print-mod-uid accept a list of files.
Maxime Dénès
2015-01-12
Update headers.
Maxime Dénès
2014-12-16
Fix for #3154: use CUnix.sys_command to call native compiler.
Maxime Dénès
2014-05-22
Fix native_compute for systems with a limited size for the command line.
Guillaume Melquiond
2014-04-29
Native compiler: hide compiled files in a .coq-native subdirectory.
Maxime Dénès
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2013-01-22
New implementation of the conversion test, using normalization by evaluation to
mdenes
