aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqtop.ml
AgeCommit message (Expand)Author
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[sysinit] move initialization code from coqtop to hereEnrico Tassi
2021-01-27[sysinit] new component for system initializationEnrico Tassi
2020-11-16[gc] Set GC policy as best-fit in OCaml >= 4.10.0Emilio Jesus Gallego Arias
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-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-06Clean and fix definitions of options.Théo Zimmermann
2020-04-01Merge PR #11306: Centralize the flag handling native compilation.Maxime Dénès
2020-03-21Reorder the load/require cmd-options and set/unset cmd-optionsLasse Blaauwbroek
2020-03-18Update 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-03[loadpath] Rework and simplify ML loadpath handlingEmilio Jesus Gallego Arias
2020-02-26[native compiler] Allow to set OCaml include dirs for compilationEmilio Jesus Gallego Arias
2020-02-26[native compiler] Allow to set the output directory for cmx objectsEmilio Jesus Gallego Arias
2019-12-22Centralize the flag handling native compilation.Pierre-Marie Pédrot
2019-12-09Fixes #11254 (not requiring coqlib to be set to report about coqtop version).Hugo Herbelin
2019-11-01a tentative patch to allow interactive session to load .vos files; (recall th...charguer
2019-09-04Merge PR #10612: Fix feedback levelsEmilio Jesus Gallego Arias
2019-08-30[library] Move library to vernacEmilio Jesus Gallego Arias
2019-08-29Fix a few wrong uses of `msg_notice`Maxime Dénès
2019-07-08Usage: bypassing a useless detour via a reference.Hugo Herbelin
2019-07-08An even more uniform treatment of the -help option across executables.Hugo Herbelin
2019-07-08Removing -filterops "hack" from coqtop.Hugo Herbelin
2019-07-08Some common points between coqc and other coq binaries.Hugo Herbelin
2019-07-08Passing command-line option async_proofs_worker_priority functionally.Hugo Herbelin
2019-07-08An attempt to reorganize further coqtop initialization into semantic units.Hugo Herbelin
2019-07-08Adding methods help and parse_extra to custom toplevels data.Hugo Herbelin
2019-07-08Function print_memory_stat: getting rid of a mutable.Hugo Herbelin
2019-07-08A classification of command line options.Hugo Herbelin
2019-07-08Toplevel: structuring init_toplevel.Hugo Herbelin
2019-06-18[errors] remove "is_handled" logic, turn unhandled into anomaliesEmilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-21[loadpath] Make loadpath handling self-contained and move to vernacEmilio Jesus Gallego Arias
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-04-30Merge PR #10019: Update behavior of -emacs to support showing diffs in ProofG...Emilio Jesus Gallego Arias
2019-04-29[toplevel] Only print welcome header in standard coqtop.Emilio Jesus Gallego Arias
2019-04-28Update behavior of -emacs to support showing diffs in ProofGeneral (master br...Jim Fehrle
2019-04-16Command-line setters for optionsGaëtan Gilbert
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-28Show diffs in error messages if color is enabledJim Fehrle
2019-02-26Initialize styles so textual markers are used when color is not enabledJim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:12:03 +0000