aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* [stm] Warn about costly Undo operations in batch mode [BZ#5677]Gravatar Emilio Jesus Gallego Arias2017-09-27
* Merge PR #1055: Remove STM vernacularsGravatar Maxime Dénès2017-09-22
|\
* \ Merge PR #1070: Remove remaining occurrences of -just-parsing.Gravatar Maxime Dénès2017-09-22
|\ \
| * | Remove remaining occurrences of -just-parsing.Gravatar Guillaume Melquiond2017-09-21
* | | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
|/ /
| * Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
|/
* Using an algebraic type for distinguishing toplevel input from location in file.Gravatar Hugo Herbelin2017-09-14
* Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.Gravatar Maxime Dénès2017-08-29
|\
* | [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
* | Merge PR #917: Moving --print-version to -print-version for consistency.Gravatar Maxime Dénès2017-08-01
|\ \
| | * [general] Remove spurious dependency of highparsing on toplevel.Gravatar Emilio Jesus Gallego Arias2017-07-31
* | | [toplevel] Remove long ago deprecated and NOOP options.Gravatar Emilio Jesus Gallego Arias2017-07-27
| |/ |/|
* | Merge PR #902: Only perform profile initialization and printing when the flag...Gravatar Maxime Dénès2017-07-26
|\ \
| | * Adding -print-version in addition to -print-version for consistency.Gravatar Hugo Herbelin2017-07-25
* | | Adding a V8.7 compatibility version number.Gravatar Hugo Herbelin2017-07-21
| |/ |/|
| * Also a less intrusive Profile.init_profile.Gravatar Hugo Herbelin2017-07-20
|/
* Adding support for bindings tags to explicit prefix/suffix rather than colors.Gravatar Hugo Herbelin2017-07-08
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* "There are pending proofs" error message now lists the name of the proofs.Gravatar Théo Zimmermann2017-06-16
* Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\
* \ Merge PR#758: [toplevel] Print error header on fatal batch error.Gravatar Maxime Dénès2017-06-14
|\ \
* \ \ Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\ \ \
| | | * Add support for Coq 8.6.Gravatar Guillaume Melquiond2017-06-14
| | | * Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| | | * Remove support for Coq 8.3.Gravatar Guillaume Melquiond2017-06-14
| | | * Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
| | | * Add a version to be used when parsing compatibility notations mentioning old ...Gravatar Guillaume Melquiond2017-06-14
| |_|/ |/| |
* | | Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
| * | [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
|/ /
| * [toplevel] Print error header on fatal batch error.Gravatar Emilio Jesus Gallego Arias2017-06-10
|/
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [emacs] [toplevel] Make emacs flag local to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-06-01
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge PR#645: [stm] Tweak debug options.Gravatar Maxime Dénès2017-05-25
|\
* \ Merge PR#406: coq makefile2Gravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \
| | * | Document --print-version in UsageGravatar Enrico Tassi2017-05-23
| | * | Put the list of Coq sources subdirectories in one placeGravatar Enrico Tassi2017-05-23
| | * | Usage.print_config moved to EnvarsGravatar Enrico Tassi2017-05-23
| |/ /
| * | Merge PR#644: [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Gravatar Maxime Dénès2017-05-20
| |\ \
| * \ \ Merge PR#640: [toplevel] Restore 8.6 goal printing behavior.Gravatar Maxime Dénès2017-05-20
| |\ \ \
| | | | * [stm] Tweak debug options.Gravatar Emilio Jesus Gallego Arias2017-05-18
| | |_|/ | |/| |
| | | * [toplevel] [stm] Avoid edit_at in batch mode (bug #5520)Gravatar Emilio Jesus Gallego Arias2017-05-18
| | |/ | |/|
| | * [toplevel] Restore 8.6 goal printing behavior.Gravatar Emilio Jesus Gallego Arias2017-05-17
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
| |\ \ | | |/ | |/|
| | * Removing a variable warned unused.Gravatar Hugo Herbelin2017-05-14
| | * Merge PR#604: FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print...Gravatar Maxime Dénès2017-05-10
| | |\
| * | \ Merge PR#615: coqtop -help: don't die if coqlib can't be foundGravatar Maxime Dénès2017-05-09
| |\ \ \
| * | | | [toplevel] Fix a couple of logical errors in error printing.Gravatar Emilio Jesus Gallego Arias2017-05-05
| | | * | Fix bug #3659: -time should understand multibyte encodings.Gravatar Pierre-Marie Pédrot2017-05-05