aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
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-06-08Command line: adding variants for Require, aligning on the vernac syntax.Hugo Herbelin
2019-06-04Remove the discharge segment from vo files.Pierre-Marie Pédrot
2019-05-25Coqc: Treat unknown arguments starting with dash as unknown options rather th...Hugo Herbelin
2019-05-23Fixing typos - Part 3JPR
2019-05-21[loadpath] Make loadpath handling self-contained and move to vernacEmilio Jesus Gallego Arias
2019-05-14Coqc: Ensure that at most one file is given when -o is also given.Hugo Herbelin
2019-05-14Coqc: Ensure exclusiveness of options -quick and -vio2vo.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-14Ensuring suffix of file to compile also for -vio2vo checking.Hugo Herbelin
2019-05-14Option -check-vio-tasks: fail gracefully when not finding expected integers.Hugo Herbelin
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-05-04Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.Pierre-Marie Pédrot
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-29Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ...Maxime Dénès
2019-04-28Update behavior of -emacs to support showing diffs in ProofGeneral (master br...Jim Fehrle
2019-04-25[vernac] [ast] Make location info an attribute of vernaculars.Emilio Jesus Gallego Arias
2019-04-16Command-line setters for optionsGaëtan Gilbert
2019-04-12Unify Set and Unset handling for optionsGaëtan Gilbert
2019-04-09[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.Emilio Jesus Gallego Arias
2019-04-02Remove -compat 8.7Jason Gross
2019-03-29[parser] initialization based on Loc.t rather than Loc.sourceEnrico Tassi
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
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-03-01Move test_mode from Flags to Vernacentries (use point)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-20[paths] Try to be more portable on Win32Emilio Jesus Gallego Arias
2019-02-20Merge PR #9560: [coqlib] Remove `-boot` option for setting the coqlibEnrico Tassi
2019-02-18Sphinx: fail when a command failsGaëtan Gilbert
2019-02-14[coqlib] Remove `-boot` option for setting the coqlibEmilio Jesus Gallego Arias
2019-02-11[coqargs] Minor refactoring of error functions.Emilio Jesus Gallego Arias
2019-02-11[stm] -async-proofs-tac-j accepts only >= 1 (fix #9533)Enrico Tassi
2019-02-08Merge PR #9525: Remove global output_native_objects flag.Emilio Jesus Gallego Arias
2019-02-08Merge PR #9523: Make boot flag into a normal option (no global flag).Emilio Jesus Gallego Arias
2019-02-08Merge PR #9481: [parsing] Use AST node for main parsing entry.Enrico Tassi
2019-02-08coqargs: use algebraic datatype for -native-compilerGaëtan Gilbert
2019-02-08Remove global output_native_objects flag.Gaëtan Gilbert
2019-02-08Make boot flag into a normal option (no global flag).Gaëtan Gilbert
2019-02-05[parsing] Use AST node for main parsing entry.Emilio Jesus Gallego Arias
2019-02-05Remove the Plexing.Error exception.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 14:47:10 +0000