aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
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-30Merge branch 'v8.5' into trunkEnrico Tassi
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-23Merge branch 'v8.5'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-11Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-08Fixing bug #2951.Pierre-Marie Pédrot
2015-03-06Merge branch 'v8.5' into trunkPierre Letouzey
2015-03-05Do not prepend a "Error:" header when the error is expected by the user.Guillaume Melquiond
2015-02-28Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-27Fixing OCaml 3.12 compilation.Pierre-Marie Pédrot
2015-02-27Fixing bug #3249.Pierre-Marie Pédrot
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
2015-02-26Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-24Univs: Fix Check calling the kernel to retype in the wrong environment.Matthieu Sozeau
2015-02-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-19Adding a possible DEPRECATED flag to VERNAC EXTEND statements.Pierre-Marie Pédrot
2015-02-18Merge branch 'v8.5'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-16Using same code for browsing physical directories in coqtop and coqdep.Hugo Herbelin
2015-02-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
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-11Merge branch 'v8.5'Pierre-Marie Pédrot
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-10Merge branch 'v8.5'Pierre-Marie Pédrot
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-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-01-29Prevent spurious warnings about Arguments.Guillaume Melquiond