aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* 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
* Fixing bug #2951.Gravatar Pierre-Marie Pédrot2015-03-08
* Do not prepend a "Error:" header when the error is expected by the user.Gravatar Guillaume Melquiond2015-03-05
* Fixing OCaml 3.12 compilation.Gravatar Pierre-Marie Pédrot2015-02-27
* Fixing bug #3249.Gravatar Pierre-Marie Pédrot2015-02-27
* Univs: Fix Check calling the kernel to retype in the wrong environment.Gravatar Matthieu Sozeau2015-02-24
* Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Gravatar Pierre-Marie Pédrot2015-02-19
* Fix bug #4046.Gravatar Matthieu Sozeau2015-02-18
* Remove Whelp commands.Gravatar Maxime Dénès2015-02-17
* Fix bug #3960: potential evar instance categorized as an unresolvableGravatar Matthieu Sozeau2015-02-16
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Better error message for nested module application.Gravatar Maxime Dénès2015-02-13
* Fix typos about .vio files (thanks Arthur for spotting them)Gravatar Enrico Tassi2015-02-12
* Revert "Using same code for browsing physical directories in coqtop and coqdep."Gravatar Hugo Herbelin2015-02-12
* Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Gravatar Hugo Herbelin2015-02-12
* Capital letter in plugins.Gravatar Hugo Herbelin2015-02-12
* Using same code for browsing physical directories in coqtop and coqdep.Gravatar Hugo Herbelin2015-02-12
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-11
* Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ...Gravatar Hugo Herbelin2015-02-10
* Properly set module names in presence of -Q. (Fix for bug #3958)Gravatar Guillaume Melquiond2015-02-05
* Optimized Import/Export the same way as Require Import/Export wasGravatar Hugo Herbelin2015-02-04
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-04
* Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"Gravatar Enrico Tassi2015-02-03
* Tactic Notation: use stable unique key for notations (Close: 3970)Gravatar Enrico Tassi2015-02-03
* spit module path using / as directory separatorGravatar Enrico Tassi2015-02-03
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Prevent spurious warnings about Arguments.Gravatar Guillaume Melquiond2015-01-29
* Equality Schemes options: reverting commit ff9f94634 which isGravatar Hugo Herbelin2015-01-24
* Isolate a function for printing evar sets.Gravatar Hugo Herbelin2015-01-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 03:17:23 +0000