aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2019-09-02Merge PR #10562: [library] Move library to vernacMaxime Dénès
2019-09-02Merge PR #9918: Fix #9294: critical bug with template polymorphismPierre-Marie Pédrot
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-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2019-08-26[glob/aux files] Remove undocumented Stdout dump, cleanup flags.Emilio Jesus Gallego Arias
2019-08-24[dune] Migrate static Dune files to Dune 1.10Emilio Jesus Gallego Arias
2019-08-14[vernac] Refactor Vernacular Control Attributes into a listEmilio Jesus Gallego Arias
2019-08-09Merge PR #10641: Fix regression of #10637 (-emacs arg should set color to `EM...Emilio Jesus Gallego Arias
2019-08-08Fix regression of #10637 (-emacs arg sets color to `EMACS)Jim Fehrle
2019-07-31[toplevel] Make all argument lists to be in user-declared order.Emilio Jesus Gallego Arias
2019-07-29Tentatively providing a localization function to ad-hoc camlp5 parsers.Pierre-Marie Pédrot
2019-07-25Remove deprecated `Backtrack` commandMaxime Dénès
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
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-07-08Toplevel: structuring source code.Hugo Herbelin
2019-06-30Merge PR #10356: Re-add the "Show Goal" command for Prooftree in PG.Emilio Jesus Gallego Arias
2019-06-25Re-add the "Show Goal" command for Prooftree in PG.Jim Fehrle
2019-06-24[test-suite] Fix printers testGaëtan Gilbert
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