aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqtop.ml
AgeCommit message (Expand)Author
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
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
2019-02-08Merge PR #9525: Remove global output_native_objects flag.Emilio Jesus Gallego Arias
2019-02-08coqargs: use algebraic datatype for -native-compilerGaëtan Gilbert
2019-02-08Make 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-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-28Merge PR #8826: [toplevel] Allow to specify default options.Pierre-Marie Pédrot
2018-11-27Merge PR #8986: Put -indices-matter in typing_flagsMaxime Dénès
2018-11-26Put -indices-matter in typing_flagsGaëtan Gilbert
2018-11-24[toplevel] Allow to specify default options.Emilio Jesus Gallego Arias