aboutsummaryrefslogtreecommitdiff
path: root/toplevel/usage.ml
AgeCommit message (Expand)Author
2021-01-27[sysinit] new component for system initializationEnrico Tassi
2020-10-09Add an XML message for "Show Proof Diffs"Jim Fehrle
2020-05-26Fix usage of -rifrom, -refrom.Théo Zimmermann
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-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
2020-02-20[init] Add `-boot` option to avoid binding `Coq.` prefix.Emilio Jesus Gallego Arias
2020-02-09Remove the Template Check option.Pierre-Marie Pédrot
2020-01-29[rfc] [mltop] Removal of dynamic loading of object and `.ml` filesEmilio Jesus Gallego Arias
2019-10-04Allow SProp default onGaëtan Gilbert
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
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-08A classification of command line options.Hugo Herbelin
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-08Command line: adding variants for Require, aligning on the vernac syntax.Hugo Herbelin
2019-05-14Usage: Fixing wrong description of load_vernac_object and similar.Hugo Herbelin
2019-05-14Adding missing newline in coqc usage.Hugo Herbelin
2019-05-14Usage: fixing indentation for set/unset options.Hugo Herbelin
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-04-16Command-line setters for optionsGaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-02-22[library] Remove `-boot` option.Emilio Jesus Gallego Arias
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
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2018-11-15coqide: use correct toplevel name in filesGaëtan Gilbert
2018-11-05Pass native and VM flags to the kernel through environmentMaxime Dénès
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
2018-03-08Merge PR #6582: Mangle auto-generated namesMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-17Implement name mangling optionJasper Hugunin
2017-10-11Remove GeoProof support.Maxime Dénès
2017-08-01[flags] Remove XML output flag.Emilio Jesus Gallego Arias
2017-07-25Adding -print-version in addition to -print-version for consistency.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-05-25Merge PR#645: [stm] Tweak debug options.Maxime Dénès
2017-05-23Document --print-version in UsageEnrico Tassi
2017-05-23Usage.print_config moved to EnvarsEnrico Tassi
2017-05-18[stm] Tweak debug options.Emilio Jesus Gallego Arias
2017-05-05coqtop -help: don't die if coqlib can't be foundGaetan Gilbert
2017-04-27Warning 29: non escaped end of line may be non portableGaetan Gilbert
2017-03-14[toplevel] Remove unusable option -notopEmilio Jesus Gallego Arias
2016-11-21Stop parsing -compat-notations options, which are no longer supported (bug #3...Guillaume Melquiond
2016-11-14Do not mention "none" in warnings doc, as it is there for compatibility.Maxime Dénès
2016-11-04Add documentation for [Set Warnings] and the -w option.Cyprien Mangin
2016-09-17Fix indentation of -profile-ltac in -helpJason Gross
2016-06-16--print-version produces machine readable version infoEnrico Tassi
2016-06-14Merge remote-tracking branch 'origin/pr/166' into trunkEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:08:17 +0000