aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2015-05-12STM: process_error_hook set in Vernac where fname is known (fix #4229)Enrico Tassi
2015-05-11Adding a test to check whether two tactic notations conflict.Pierre-Marie Pédrot
2015-05-04Add a [Redirect] vernacular commandClément Pit--Claudel
2015-05-01Fixing computation of implicit arguments by position in fixpoints (#4217).Hugo Herbelin
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-23Using tclZEROMSG instead of tclZERO in several places.Pierre-Marie Pédrot
2015-04-17No longer add dev/ to the LoadPath, only to the ML path.Guillaume Melquiond
2015-04-16Fixing bug #4190.Pierre-Marie Pédrot
2015-04-13Program: Do not reduce obligation types preemptively, only atMatthieu Sozeau
2015-04-09Fix declarations of instances to perform restriction of universeMatthieu Sozeau
2015-04-02Remove Mltop.add_path as it is no longer possible to import files from subdir...Guillaume Melquiond
2015-04-02Make "Add LoadPath" behave accordingly to its documentation.Guillaume Melquiond
2015-04-02Display the proper error message when Require fails to find a library.Guillaume Melquiond
2015-04-01From X Require Y looks for X with absolute path, disregarding -R.Pierre-Marie Pédrot
2015-04-01Fixing inclusion of user contrib directory in the loadpath.Pierre-Marie Pédrot
2015-03-31Removing references to deprecated syntax -I/-R -as.Pierre-Marie Pédrot
2015-03-31Removing the unused root flag from loadpaths.Pierre-Marie Pédrot
2015-03-27Putting the From parameter of the Require command into the AST.Pierre-Marie Pédrot
2015-03-25coqc: fix --helpEnrico Tassi
2015-03-24Revert "Useless check when loading notations through import."Pierre-Marie Pédrot
2015-03-23Load: don't give anomaly on aborted proofs (Close: #3882)Enrico Tassi
2015-03-18add -type-in-type to the usage messageDaniel R. Grayson
2015-03-08Fixing bug #2951.Pierre-Marie Pédrot
2015-03-05Do not prepend a "Error:" header when the error is expected by the user.Guillaume Melquiond
2015-02-27Fixing OCaml 3.12 compilation.Pierre-Marie Pédrot
2015-02-27Fixing bug #3249.Pierre-Marie Pédrot
2015-02-24Univs: Fix Check calling the kernel to retype in the wrong environment.Matthieu Sozeau
2015-02-19Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Pierre-Marie Pédrot
2015-02-18Fix bug #4046.Matthieu Sozeau
2015-02-17Remove Whelp commands.Maxime Dénès
2015-02-16Fix bug #3960: potential evar instance categorized as an unresolvableMatthieu Sozeau
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-13Better error message for nested module application.Maxime Dénès
2015-02-12Fix typos about .vio files (thanks Arthur for spotting them)Enrico Tassi
2015-02-12Revert "Using same code for browsing physical directories in coqtop and coqdep."Hugo Herbelin
2015-02-12Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)Hugo Herbelin
2015-02-12Capital letter in plugins.Hugo Herbelin
2015-02-12Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
2015-02-11Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-02-10Fixing #4017, #3726 (use of implicit arguments was lost in multiple variable ...Hugo Herbelin
2015-02-05Properly set module names in presence of -Q. (Fix for bug #3958)Guillaume Melquiond
2015-02-04Optimized Import/Export the same way as Require Import/Export wasHugo Herbelin
2015-02-04Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-02-03Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"Enrico Tassi
2015-02-03Tactic Notation: use stable unique key for notations (Close: 3970)Enrico Tassi
2015-02-03spit module path using / as directory separatorEnrico Tassi
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-29Prevent spurious warnings about Arguments.Guillaume Melquiond
2015-01-24Equality Schemes options: reverting commit ff9f94634 which isHugo Herbelin
2015-01-24Isolate a function for printing evar sets.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 17:51:52 +0000