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
2021-04-14
Add test for -schedule-vio-checking
Gaëtan Gilbert
2021-04-14
Put async worker id in universe names
Gaëtan Gilbert
2021-02-26
[coqc] Don't allow to pass more than one file to coqc
Emilio Jesus Gallego Arias
2021-01-27
[sysinit] move initialization code from coqtop to here
Enrico Tassi
2021-01-27
[sysinit] new component for system initialization
Enrico Tassi
2020-11-12
Change Dumpglob.pause and Dumpglob.continue into push and pop
Lasse Blaauwbroek
2020-05-12
Interleave commandline require/set/unset commands
Lasse Blaauwbroek
2020-04-15
[proof] Merge `Proof_global` into `Declare`
Emilio Jesus Gallego Arias
2020-03-21
Reorder the load/require cmd-options and set/unset cmd-options
Lasse Blaauwbroek
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2020-03-03
[loadpath] Rework and simplify ML loadpath handling
Emilio Jesus Gallego Arias
2019-12-12
Fix #11195 and add other improvements: try loading .vio (and not just .vo) if...
charguer
2019-11-20
From CoqIDE or -vos or -vok compilation, load .vo when .vos is missing (fixin...
charguer
2019-11-01
Implementing support for vos/vok files.
charguer
2019-09-09
Merge PR #10605: [toplevel] Make all argument lists to be in user-declared or...
Hugo Herbelin
2019-08-26
[glob/aux files] Remove undocumented Stdout dump, cleanup flags.
Emilio Jesus Gallego Arias
2019-07-31
[toplevel] Make all argument lists to be in user-declared order.
Emilio Jesus Gallego Arias
2019-07-08
A classification of command line options.
Hugo Herbelin
2019-07-08
Toplevel: structuring source code.
Hugo Herbelin
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2019-06-04
Remove the discharge segment from vo files.
Pierre-Marie Pédrot
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
