aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2021-04-23Relying on the abstract notion of streams with location for parsing.Hugo Herbelin
2021-04-14Add test for -schedule-vio-checkingGaëtan Gilbert
2021-04-14Put async worker id in universe namesGaëtan Gilbert
2021-03-11noglob/dumpglob should be in coqc specific usageGaëtan Gilbert
2021-03-03[build] Split stdlib to it's own opam package.Emilio Jesus Gallego Arias
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
2021-02-25Merge PR #13863: Get rid of the compilation date from the binaries to make th...coqbot-app[bot]
2021-02-19Merge PR #13865: [coqtop] be verbose only in interactive modecoqbot-app[bot]
2021-02-16[coqtop] be verbose only in interactive modeEnrico Tassi
2021-02-16Get rid of the compilation date from the binaries to make them more stable.Guillaume Melquiond
2021-02-04Remove deprecated -inputstate command line argumentGaëtan Gilbert
2021-01-27[coqtop] handle -print-module-uid after initializationEnrico Tassi
2021-01-27[coqc] move -output-context from sysinit/coqargs to coqc properEnrico Tassi
2021-01-27[sysinit] move initialization code from coqtop to hereEnrico Tassi
2021-01-27[sysinit] new component for system initializationEnrico Tassi
2021-01-26[coqargs] use option injection for -wEnrico Tassi
2020-12-03[coqide] fix procedure to parse argumentsEnrico Tassi
2020-11-23Update compat infrastructure for 8.14Enrico Tassi
2020-11-20Configure default value of -native-compilerPierre Roux
2020-11-16[gc] Set GC policy as best-fit in OCaml >= 4.10.0Emilio Jesus Gallego Arias
2020-11-12Merge PR #13253: Change Dumpglob.pause and Dumpglob.continue into push and popcoqbot-app[bot]
2020-11-12Change Dumpglob.pause and Dumpglob.continue into push and popLasse Blaauwbroek
2020-11-09[compat] remove 8.10Enrico Tassi
2020-10-21[coqinit] Cosmetics on long list append.Emilio Jesus Gallego Arias
2020-10-21[coqinit] Respect order of ML includesEmilio Jesus Gallego Arias
2020-10-12Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocolcoqbot-app[bot]
2020-10-09Add 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 CoqEmilio Jesus Gallego Arias
2020-09-01Unify the shelvesMaxime Dénès
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
2020-08-26Move given_up goals to evar_mapMaxime Dénès
2020-07-11Merge PR #12635: Correct comment and clarify constantPierre-Marie Pédrot
2020-07-02Correct comment and clarify constantJim Fehrle
2020-07-01[state] Consolidate state handling in VernacstateEmilio Jesus Gallego Arias
2020-06-13[toplevel] Annotate tailcall functionsEmilio Jesus Gallego Arias
2020-05-26Fix usage of -rifrom, -refrom.Théo Zimmermann
2020-05-18Update to 8.13.Théo Zimmermann
2020-05-12Interleave commandline require/set/unset commandsLasse Blaauwbroek
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-16Merge PR #12070: Ignore -native-compiler option when disabledPierre-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 PfeditEmilio Jesus Gallego Arias
2020-04-15Ignore -native-compiler option when disabledPierre Roux
2020-04-08Merge PR #12005: Remove deprecated coqtop optionsEmilio Jesus Gallego Arias
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-02Remove deprecated -require option.Théo Zimmermann
2020-04-01Merge 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 GEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 06:43:09 +0000