aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Expand)AuthorAge
* 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
|\
* \ Merge remote-tracking branch 'origin/pr/182' into trunkGravatar Enrico Tassi2016-06-14
|\ \
* \ \ Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \ \
* | | | Moving back Ltac profiling to the Ltac folder.Gravatar Pierre-Marie Pédrot2016-06-14
| * | | STM: each proof block can be enabled separatelyGravatar Enrico Tassi2016-06-06
| * | | STM: proof block detection made optional + simple testGravatar Enrico Tassi2016-06-06
* | | | -profileltac -> -profile-ltac, as per @herbelinGravatar Jason Gross2016-06-05
* | | | LtacProf for Coq trunkGravatar Jason Gross2016-06-05
|/ / /
| * | STM delegation policy can be customizedGravatar Enrico Tassi2016-05-31
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
|/ /
| * coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-09
|\
| * Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* | Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * Fix bug #4705: coqtop accepts both -emacs and -ideslave.Gravatar Pierre-Marie Pédrot2016-05-03
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\|
| * Restore warnings produced by the interpretation of the command lineGravatar Hugo Herbelin2016-01-22
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | Remove deprecated command-line options such as "-as".Gravatar Guillaume Melquiond2016-01-06
* | CLEANUP: simplifying "Coqtop.init_gc" implementationGravatar Matej Kosik2015-12-18
* | CLEANUP: removing unnecessary wrapper functionGravatar Matej Kosik2015-12-18
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-15
|\|
| * Flag -compat 8.4 now loads Coq.Compat.Coq84.Gravatar Maxime Dénès2015-12-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-15
|\|
| * Remove -vm flag of coqtop.Gravatar Maxime Dénès2015-10-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-10
|\|
| * Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * Spawn: use each socket exclusively for writing or readingGravatar Enrico Tassi2015-10-08
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-02
|\|
| * Prevent States.intern_state and System.extern_intern from looking up files in...Gravatar Guillaume Melquiond2015-09-29
| * Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
| * Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-09-25
|\|
| * The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-08-05
|\|
| * For convenience, making yes and on, and no and off synonymous inGravatar Hugo Herbelin2015-08-02
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-07-18
|\|
| * Option -type-in-type: added support in checker and making it contaminatingGravatar Hugo Herbelin2015-07-10
| * Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-06-24
|\|
| * when OCAML_GC_STATS points to a filepath, write Gc stats into itGravatar Gabriel Scherer2015-06-24
* | Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-23