aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
...
* | | 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
| | * | | coqtop -help: don't die if coqlib can't be foundGravatar Gaetan Gilbert2017-05-05
| |/ / /
| * | | Adding an option "Printing Unfocused".Gravatar Pierre Courtieu2017-05-04
| | | * FIx bug #5300: uncaught exception in "Print Assumptions".Gravatar Cyprien Mangin2017-05-03
| | |/
| * | Warning 29: non escaped end of line may be non portableGravatar Gaetan Gilbert2017-04-27
| * | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| * | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| * | [toplevel] Remove unused parameter from `Vernac.process_expr`.Gravatar Emilio Jesus Gallego Arias2017-04-25
| * | [toplevel] Use exception information for error printing.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| * | [toplevel] Don't check proofs in -quick mode.Gravatar Emilio Jesus Gallego Arias2017-04-24
| * | [toplevel] Don't mask critical exceptions in vernac interpretation.Gravatar Emilio Jesus Gallego Arias2017-04-24
|/ /
* | Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\ \
| * | [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
* | | [toplevel] Fix printing of parsing errors + corner case.Gravatar Emilio Jesus Gallego Arias2017-04-19
|/ /
| * Fixing bug #5470 (anomaly on notations with misused "binder" type).Gravatar Hugo Herbelin2017-04-14
| * Fixing bug #5469 (notation format not recognizing curly braces).Gravatar Hugo Herbelin2017-04-14
* | [toplevel] Don't print goals if there is no pending proof.Gravatar Emilio Jesus Gallego Arias2017-04-13
* | Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \
| * | [toplevel] [stm] cleanup in module openGravatar Emilio Jesus Gallego Arias2017-04-12
| * | [vernac] vernacentries.mli cleanupGravatar Emilio Jesus Gallego Arias2017-04-12
| * | [stm] Port the toplevel to the STM.Gravatar Emilio Jesus Gallego Arias2017-04-12
* | | Merge PR#547: [toplevel] Remove the feedback printer only on exit.Gravatar Maxime Dénès2017-04-10
|\ \ \
| | * | [stm] remove process_error_hookGravatar Emilio Jesus Gallego Arias2017-04-07
| |/ / |/| |
* | | Merge PR#461: [camlpX] Remove camlp4 compat layer.Gravatar Maxime Dénès2017-04-07
|\ \ \
| | * | [toplevel] Remove the feedback feeder printing only on exit.Gravatar Emilio Jesus Gallego Arias2017-04-07
| |/ / |/| |
* | | Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)Gravatar Matthieu Sozeau2017-04-07
| * | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
|/ /
| * Fix a few programming pearls related to Time, Fail and Redirect.Gravatar Maxime Dénès2017-04-06
| * Merge branch 'origin/v8.5' into v8.6.Gravatar Hugo Herbelin2017-04-06
| |\
* | | [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-04-05
* | | Merge PR#502: [pp] Add anomaly header to error messages.Gravatar Maxime Dénès2017-04-04
|\ \ \
| | * | Instances should obey universe binders even when defined by tactics.Gravatar Gaetan Gilbert2017-04-03
* | | | [nit] Fix a couple incorrect uses of msg_error.Gravatar Emilio Jesus Gallego Arias2017-03-24