aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Expand)AuthorAge
* Revert "Rename Lexer -> CLexer."Gravatar Pierre-Marie Pédrot2016-05-31
* Rename Lexer -> CLexer.Gravatar Pierre-Marie Pédrot2016-05-09
* Fix bug #4705: coqtop accepts both -emacs and -ideslave.Gravatar Pierre-Marie Pédrot2016-05-03
* Restore warnings produced by the interpretation of the command lineGravatar Hugo Herbelin2016-01-22
* 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
* Flag -compat 8.4 now loads Coq.Compat.Coq84.Gravatar Maxime Dénès2015-12-14
* Remove -vm flag of coqtop.Gravatar Maxime Dénès2015-10-14
* Code cleaning in VM (with Benjamin).Gravatar Maxime Dénès2015-10-09
* Spawn: use each socket exclusively for writing or readingGravatar Enrico Tassi2015-10-08
* 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
* The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
* For convenience, making yes and on, and no and off synonymous inGravatar Hugo Herbelin2015-08-02
* 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
* when OCAML_GC_STATS points to a filepath, write Gc stats into itGravatar Gabriel Scherer2015-06-24
* Warning are enabled by default in interactive mode.Gravatar Pierre-Marie Pédrot2015-06-23
* Flag -test-mode intended to be used for ad-hoc prints in test-suiteGravatar Enrico Tassi2015-05-29
* Uncaught exception termination exits coqtop with the anomaly errno.Gravatar Pierre-Marie Pédrot2015-05-18
* Disabling colors when tERM variable is "dumb".Gravatar Pierre Courtieu2015-05-18
* The -list-tag options now prints the corresponding COQ_COLORS value.Gravatar Pierre-Marie Pédrot2015-05-14
* Adding an option -w to control Coq warning output.Gravatar Pierre-Marie Pédrot2015-05-14
* Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Remove Mltop.add_path as it is no longer possible to import files from subdir...Gravatar Guillaume Melquiond2015-04-02
* Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
* Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
* Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
* spit module path using / as directory separatorGravatar Enrico Tassi2015-02-03
* Make -print-mod-uid accept a list of files.Gravatar Maxime Dénès2015-01-15
* Made -print-mod-uid more silent and robust.Gravatar Maxime Dénès2015-01-13
* Update headers.Gravatar Maxime Dénès2015-01-12
* rename: vi -> vioGravatar Enrico Tassi2015-01-06
* STM: rename and simplify flagsGravatar Enrico Tassi2014-12-17
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* async_queries_* merged with async_proofs_*Gravatar Enrico Tassi2014-11-27
* Feedback: API cleaned up, documented and made user extensibleGravatar Enrico Tassi2014-11-27
* Plugging console highlighting in for toplevel and compilation error messages.Gravatar Pierre-Marie Pédrot2014-11-24
* For consistency with other coqtop flags, use -help rather than --help in usage.Gravatar Hugo Herbelin2014-11-16
* Adding a command line option to print out accepted color tags.Gravatar Pierre-Marie Pédrot2014-11-15
* Reworking the -color flag of coqtop.Gravatar Pierre-Marie Pédrot2014-11-15
* Plugging the color initialization in the Coqtop loop.Gravatar Pierre-Marie Pédrot2014-11-15
* Exit with code 129 when an anomaly occurs.Gravatar Xavier Clerc2014-11-14
* STM: new worker for queriesGravatar Enrico Tassi2014-10-31
* Undo prints only if coqtop || emacsGravatar Enrico Tassi2014-09-16
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
* Load Prelude.vi if not Prelude.vo is found (Close: 3595)Gravatar Enrico Tassi2014-09-09
* toploop plugins taken into account when printing --help (close: 3535)Gravatar Enrico Tassi2014-09-09