aboutsummaryrefslogtreecommitdiff
path: root/toplevel/usage.ml
AgeCommit message (Expand)Author
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
2016-06-05-profileltac -> -profile-ltac, as per @herbelinJason Gross
2016-06-05LtacProf for Coq trunkJason Gross
2016-05-19fix blanks in usage messageEnrico Tassi
2016-05-19coqc: support -o option to specify output file nameEnrico Tassi
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2015-09-25Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
2015-09-25Updating the documentation and the toolchain w.r.t. the change in -compile.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:23:04 +0000