aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqinit.ml
AgeCommit message (Expand)Author
2016-09-25The coqtop options -Q and -R do not affect the ML loadpath anymore.Pierre-Marie Pédrot
2016-09-10Avoid putting a useless "toploop" directory in the ML search path if it does ...Guillaume Melquiond
2016-09-09Make it explicit when paths are added to the ML search paths.Guillaume Melquiond
2016-07-06Fix #4793: Coq 8.6 should accept -compat 8.6Maxime Dénès
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-02coqtop: Add ltac/ to search path.Matthieu Sozeau
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-10-29Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-29Accept option -compat 8.5. (Fix bug #4393)Guillaume Melquiond
2015-05-05Merge branch 'v8.5'Pierre-Marie Pédrot
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-17No longer add dev/ to the LoadPath, only to the ML path.Guillaume Melquiond
2015-04-09Merge branch 'v8.5' into trunkPierre Letouzey
2015-04-02Remove Mltop.add_path as it is no longer possible to import files from subdir...Guillaume Melquiond
2015-04-01Fixing inclusion of user contrib directory in the loadpath.Pierre-Marie Pédrot
2015-02-27Adding a new folder corresponding to the low-level part of the pretyperPierre-Marie Pédrot
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-01-12Update headers.Maxime Dénès
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-10-14Fix ML paths (thanks Jean-Marc Notin for bisecting it)Enrico Tassi
2014-10-13Coqinit: look in toploop/ even if configured with -localEnrico Tassi
2014-08-25Prerequisite to fix stm test-suite when not in -localPierre Boutillier
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-06-25all coqide specific files moved into ide/Enrico Tassi
2014-06-25cut toploop(s) out of coqtop: now they are loaded dynamicallyEnrico Tassi
2014-04-08Add an option -Q (tentative name).Guillaume Melquiond
2014-04-06Change handling of loadpath and mlpath.Guillaume Melquiond
2014-03-06Lets coqtop use a slashVirgile Prevosto
2013-08-22Misc changes around coqtop.ml :letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Updating the backtrace handling mechanism to accomodate the newppedrot
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Added backtrace information to anomaliesppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-08Ensure that a function declared with a label is used with itletouzey
2012-11-26Monomorphization (toplevel)ppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-23No more states/initial.coq, instead coqtop now requires Prelude.voletouzey
2012-08-08Updating headers.herbelin
2012-07-05Notation: a new annotation "compat 8.x" extending "only parsing"letouzey
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-29place all pretty-printing files in new dir printing/letouzey
2012-04-12lib directory is cut in 2 cma.pboutill
2011-11-21/home/pirbo/.coqrc* are read againpboutill
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 20:29:12 +0000