aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Expand)AuthorAge
* Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
* [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
|\ \ \
| | * | Usage.print_config moved to EnvarsGravatar Enrico Tassi2017-05-23
| |/ /
| | * [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
| |/
| * 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 omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| * [toplevel] Use exception information for error printing.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/
* 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
|/
* 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
* | [toplevel] Remove the feedback feeder printing only on exit.Gravatar Emilio Jesus Gallego Arias2017-04-07
|/
* [toplevel] Remove exception error printer in favor of feedback printer.Gravatar Emilio Jesus Gallego Arias2017-04-05
* Merge PR#390: Updates to the Pretty Printing InfrastructureGravatar Maxime Dénès2017-03-22
|\
| * [pp] Move terminal-specific tagging to the toplevel.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * [pp] Remove special tag type and handler from Pp.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * [pp] Make feedback the only logging mechanism.Gravatar Emilio Jesus Gallego Arias2017-03-21
| * [error] Move back fatal_error to toplevelGravatar Emilio Jesus Gallego Arias2017-03-21
| * [pp] Prepare for serialization, remove opaque glue.Gravatar Emilio Jesus Gallego Arias2017-03-21
* | [toplevel] Remove unusable option -notopGravatar Emilio Jesus Gallego Arias2017-03-14
|/
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
* Fix bug in warnings: -w foo was silent when foo did not exist.Gravatar Maxime Dénès2016-11-14
* [toplevel] Remove undocumented "just_parsing" flag.Gravatar Emilio Jesus Gallego Arias2016-10-17
* [toplevel] Remove duplicate beautify flags.Gravatar Emilio Jesus Gallego Arias2016-10-17
* Removing export of location_table outside of cLexer.Gravatar Hugo Herbelin2016-10-17
* Merge PR #224 into v8.6Gravatar Pierre-Marie Pédrot2016-10-12
|\
* | Remove the -no-compat-notations flag.Gravatar Maxime Dénès2016-10-06
* | Remove the Set Verbose Compat option and turn the warning on by default.Gravatar Maxime Dénès2016-10-06
| * [pp] Remove duplicate color logger.Gravatar Emilio Jesus Gallego Arias2016-09-30
|/
* -profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)Gravatar Enrico Tassi2016-09-29
* coqc: print debug feedback coming from workersGravatar Enrico Tassi2016-09-13
* fix get_host_port error message (#4724)Gravatar Enrico Tassi2016-08-23
* Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
|\
| * Do not assume the "TERM" environment variable is always set (bug #5007).Gravatar Guillaume Melquiond2016-08-11
* | Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* | Moving the typing_flags to the environment.Gravatar Pierre-Marie Pédrot2016-06-18
* | --print-version produces machine readable version infoGravatar Enrico Tassi2016-06-16
* | Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\ \