aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
* Reinstall Set Printing Universes option overwritten by Maxime!Gravatar Matthieu Sozeau2015-06-28
* Fix bug #4254 with the help of J.H. JourdanGravatar Matthieu Sozeau2015-06-26
* Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"Gravatar Lionel Rieg2015-06-26
* Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.Gravatar Thomas Sibut-Pinote2015-06-25
* improve --help documentation: the -m|--memory option was missingGravatar Gabriel Scherer2015-06-24
* when OCAML_GC_STATS points to a filepath, write Gc stats into itGravatar Gabriel Scherer2015-06-24
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* obligations: wrap Ephemeron.get to make error more informativeGravatar Enrico Tassi2015-06-23
* Wrap the program_info type up in the ephemeron mechanismGravatar Alec Faithfull2015-06-23
* Add a Set Dump Bytecode command for debugging purposes.Gravatar Maxime Dénès2015-06-23
* Warning are enabled by default in interactive mode.Gravatar Pierre-Marie Pédrot2015-06-23
* Remove uses of polymorphic equality from prev. commitGravatar Clément Pit--Claudel2015-06-22
* Replace 'try ... with Failure "List.last"' with 'if l <> []'Gravatar Clément Pit--Claudel2015-06-22
* Guard the List.hd call in [Show Intros]Gravatar Clément Pit--Claudel2015-06-22
* coqtop: reset the current file name after a load-vernac-sourceGravatar Enrico Tassi2015-05-29
* Flag -test-mode intended to be used for ad-hoc prints in test-suiteGravatar Enrico Tassi2015-05-29
* make Unset Silent work in coqcGravatar Enrico Tassi2015-05-29
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Uncaught exception termination exits coqtop with the anomaly errno.Gravatar Pierre-Marie Pédrot2015-05-18
* The Fail command does not catch uncaught exception anomalies anymore.Gravatar Pierre-Marie Pédrot2015-05-18
* Disabling colors when tERM variable is "dumb".Gravatar Pierre Courtieu2015-05-18
* Fix usage about -color.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
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Better error message for non-existent required libraries with a From prefix.Gravatar Pierre-Marie Pédrot2015-05-13
* STM: process_error_hook set in Vernac where fname is known (fix #4229)Gravatar Enrico Tassi2015-05-12
* Adding a test to check whether two tactic notations conflict.Gravatar Pierre-Marie Pédrot2015-05-11
* Add a [Redirect] vernacular commandGravatar Clément Pit--Claudel2015-05-04
* Fixing computation of implicit arguments by position in fixpoints (#4217).Gravatar Hugo Herbelin2015-05-01
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* No longer add dev/ to the LoadPath, only to the ML path.Gravatar Guillaume Melquiond2015-04-17
* Fixing bug #4190.Gravatar Pierre-Marie Pédrot2015-04-16
* Program: Do not reduce obligation types preemptively, only atGravatar Matthieu Sozeau2015-04-13
* Fix declarations of instances to perform restriction of universeGravatar Matthieu Sozeau2015-04-09
* Remove Mltop.add_path as it is no longer possible to import files from subdir...Gravatar Guillaume Melquiond2015-04-02
* Make "Add LoadPath" behave accordingly to its documentation.Gravatar Guillaume Melquiond2015-04-02
* Display the proper error message when Require fails to find a library.Gravatar Guillaume Melquiond2015-04-02
* From X Require Y looks for X with absolute path, disregarding -R.Gravatar Pierre-Marie Pédrot2015-04-01
* Fixing inclusion of user contrib directory in the loadpath.Gravatar Pierre-Marie Pédrot2015-04-01
* Removing references to deprecated syntax -I/-R -as.Gravatar Pierre-Marie Pédrot2015-03-31
* Removing the unused root flag from loadpaths.Gravatar Pierre-Marie Pédrot2015-03-31
* Putting the From parameter of the Require command into the AST.Gravatar Pierre-Marie Pédrot2015-03-27
* coqc: fix --helpGravatar Enrico Tassi2015-03-25
* Revert "Useless check when loading notations through import."Gravatar Pierre-Marie Pédrot2015-03-24
* Load: don't give anomaly on aborted proofs (Close: #3882)Gravatar Enrico Tassi2015-03-23
* add -type-in-type to the usage messageGravatar Daniel R. Grayson2015-03-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-12 07:43:11 +0000