index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
toplevel
Age
Commit message (
Expand
)
Author
2020-11-20
Configure default value of -native-compiler
Pierre Roux
2020-11-16
[gc] Set GC policy as best-fit in OCaml >= 4.10.0
Emilio Jesus Gallego Arias
2020-11-12
Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and pop
coqbot-app[bot]
2020-11-12
Change Dumpglob.pause and Dumpglob.continue into push and pop
Lasse Blaauwbroek
2020-11-09
[compat] remove 8.10
Enrico Tassi
2020-10-21
[coqinit] Cosmetics on long list append.
Emilio Jesus Gallego Arias
2020-10-21
[coqinit] Respect order of ML includes
Emilio Jesus Gallego Arias
2020-10-12
Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol
coqbot-app[bot]
2020-10-09
Add an XML message for "Show Proof Diffs"
Jim Fehrle
2020-09-17
[install] Rewording of primitive floats.
Emilio Jesus Gallego Arias
2020-09-17
[build] Don't link `num` anymore in Coq
Emilio Jesus Gallego Arias
2020-09-01
Unify the shelves
Maxime Dénès
2020-08-27
[numeral] [plugins] Switch from `Big_int` to ZArith.
Emilio Jesus Gallego Arias
2020-08-26
Move given_up goals to evar_map
Maxime Dénès
2020-07-11
Merge PR #12635: Correct comment and clarify constant
Pierre-Marie Pédrot
2020-07-02
Correct comment and clarify constant
Jim Fehrle
2020-07-01
[state] Consolidate state handling in Vernacstate
Emilio Jesus Gallego Arias
2020-06-13
[toplevel] Annotate tailcall functions
Emilio Jesus Gallego Arias
2020-05-26
Fix usage of -rifrom, -refrom.
Théo Zimmermann
2020-05-18
Update to 8.13.
Théo Zimmermann
2020-05-12
Interleave commandline require/set/unset commands
Lasse Blaauwbroek
2020-04-16
Make cumulative sprop a typing flag, deprecate command line -sprop-cumulative
Gaëtan Gilbert
2020-04-16
Merge PR #12070: Ignore -native-compiler option when disabled
Pierre-Marie Pédrot
2020-04-15
[proof] Move functions related to `Proof.t` to `Proof`
Emilio Jesus Gallego Arias
2020-04-15
[proof] Merge `Proof_global` into `Declare`
Emilio Jesus Gallego Arias
2020-04-15
[proof] Move proof_global functionality to Proof_global from Pfedit
Emilio Jesus Gallego Arias
2020-04-15
Ignore -native-compiler option when disabled
Pierre Roux
2020-04-08
Merge PR #12005: Remove deprecated coqtop options
Emilio Jesus Gallego Arias
2020-04-06
Clean and fix definitions of options.
Théo Zimmermann
2020-04-02
Remove deprecated -require option.
Théo Zimmermann
2020-04-01
Merge PR #11306: Centralize the flag handling native compilation.
Maxime Dénès
2020-03-25
[pcoq] Inline the exported Gramlib interface instead of exposing it as G
Emilio Jesus Gallego Arias
2020-03-25
[parsing] Move `coq_parsable` custom logic to Grammar.
Emilio Jesus Gallego Arias
2020-03-25
[parsing] Remove redundant interfaces from Pcoq
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-04
[boot] Don't initialize coqlib when `-boot` is passed.
Emilio Jesus Gallego Arias
2020-03-04
Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.
Pierre-Marie Pédrot
2020-03-03
[loadpath] Rework and simplify ML loadpath handling
Emilio Jesus Gallego Arias
2020-03-03
[exninfo] Deprecate aliases for exception re-raising.
Emilio Jesus Gallego Arias
2020-03-01
[parser] lk_int -> lk_nat
Maxime Dénès
2020-03-01
Refactor lookaheads using DSL
Maxime Dénès
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-02-20
[init] Add `-boot` option to avoid binding `Coq.` prefix.
Emilio Jesus Gallego Arias
2020-02-13
[coqinit] Removed unused `with_ml` parameter.
Emilio Jesus Gallego Arias
2020-02-13
[build] Consolidate stdlib's .v files under a single directory.
Emilio Jesus Gallego Arias
2020-02-13
Merge PR #11521: Remove Goptions.opt_name field
Pierre-Marie Pédrot
2020-02-13
Merge PR #11457: [toplevel] Refactor control loop
Hugo Herbelin
2020-02-12
[toplevel] Make toplevel loop tail-recursive again
Emilio Jesus Gallego Arias
[next]