index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
nativelib.ml
Age
Commit message (
Expand
)
Author
2020-03-03
[exninfo] Deprecate aliases for exception re-raising.
Emilio Jesus Gallego Arias
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
2020-01-13
Native compute: cleanup temporary files on program exit
Gaëtan Gilbert
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
Better error message when OCaml compiler not found for native compute
Maxime Dénès
2018-11-05
Pass native and VM flags to the kernel through environment
Maxime Dénès
2018-10-02
Merge PR #8572: [config] Miscellaneous cleaning of configuration variables.
Pierre-Marie Pédrot
2018-10-01
[nit] Qualify `Envars` use.
Emilio Jesus Gallego Arias
2018-09-26
[ocaml] Update required OCaml version to 4.05.0
Emilio Jesus Gallego Arias
2018-09-24
[kernel] Compile with almost all warnings enabled.
Emilio Jesus Gallego Arias
2018-07-24
Properly disable native compilation when -native-compiler is unset.
Pierre-Marie Pédrot
2018-02-27
Update headers following #6543.
Théo Zimmermann
2018-02-09
[nativecomp] Remove ad-hoc handling of Dynlink exception.
Emilio Jesus Gallego Arias
2017-11-28
Fix native compute for byte compiled Coq.
Gaëtan Gilbert
2017-10-10
[flambda] [native] Pass `-Oclassic` to the native compiler.
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
2017-06-02
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-05-27
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2016-09-29
UPDATE: reference to a deprecated variable "Filename.temp_dir_name" was repla...
Matej Kosik
2016-07-03
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-06-29
A new infrastructure for warnings.
Maxime Dénès
2016-05-31
Feedback cleanup
Emilio Jesus Gallego Arias
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-13
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-08
Be more verbose about failure to compile libraries to native code.
Guillaume Melquiond
2015-07-18
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-07-10
Native compiler: make non-fatal linking errors silent except in debug mode.
Maxime Dénès
2015-07-09
Improve semantics of -native-compiler flag.
Maxime Dénès
2015-06-22
Merge remote-tracking branch 'forge/v8.5'
Pierre Boutillier
2015-06-22
All invocations to ocaml compilers go through ocamlfind
Pierre Boutillier
2015-06-15
Native compiler: do not catch exceptions not related to dynlink.
Maxime Dénès
2015-05-17
Fixing bug #4201: The native compiler is not race-free.
Pierre-Marie Pédrot
2015-02-04
Nativelib: catch Unix_error (like no ocamlopt found)
Enrico Tassi
2015-01-13
Native compiler: if debug flag not present, remove .native 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-11-10
Better printing of dynlink errors in native compiler.
Maxime Dénès
2014-06-16
Preemptively remove files from native compilation.
Guillaume Melquiond
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-12-29
Avoid generating .ml files in native compiler.
Maxime Dénès
2013-10-28
Native compiler: library compilation errors are now non fatal.
mdenes
2013-08-22
Misc changes around coqtop.ml :
letouzey
2013-03-13
Restrict (try...with...) to avoid catching critical exn (part 8)
letouzey
[next]