index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
toplevel
/
ccompile.ml
Age
Commit message (
Expand
)
Author
2019-05-21
[loadpath] Make loadpath handling self-contained and move to vernac
Emilio Jesus Gallego Arias
2019-05-14
Ensuring suffix of file to compile also for -vio2vo checking.
Hugo Herbelin
2019-04-09
[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.
Emilio Jesus Gallego Arias
2019-03-27
[vernac] Adapt to removal of imperative proof state.
Emilio Jesus Gallego Arias
2019-02-22
[library] Remove `-boot` option.
Emilio Jesus Gallego Arias
2019-02-08
Merge PR #9525: Remove global output_native_objects flag.
Emilio Jesus Gallego Arias
2019-02-08
coqargs: use algebraic datatype for -native-compiler
Gaëtan Gilbert
2019-02-08
Remove global output_native_objects flag.
Gaëtan Gilbert
2019-02-08
Make boot flag into a normal option (no global flag).
Gaëtan Gilbert
2019-02-01
[toplevel] Split interactive toplevel and compiler binaries.
Emilio Jesus Gallego Arias
2018-11-27
Make `-async-proofs on` effective with `coqc`
Maxime Dénès
2018-11-24
[toplevel] Move compilation-related functions to their own module.
Emilio Jesus Gallego Arias
