aboutsummaryrefslogtreecommitdiff
path: root/toplevel/coqinit.ml
AgeCommit message (Expand)Author
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
2017-10-11[stm] [toplevel] Move delicate state initialization to the STM (BZ#5556)Emilio Jesus Gallego Arias
2017-10-06[stm] Switch to a functional APIEmilio Jesus Gallego Arias
2017-10-06[stm] [flags] Move document mode flags to the STM.Emilio Jesus Gallego Arias
2017-10-06[coqtop] Don't reset coqinit internal variables after initialization.Emilio Jesus Gallego Arias
2017-07-31[general] Remove spurious dependency of highparsing on toplevel.Emilio Jesus Gallego Arias
2017-07-21Adding a V8.7 compatibility version number.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond
2017-06-14Remove support for Coq 8.3.Guillaume Melquiond
2017-06-14Remove support for Coq 8.2.Guillaume Melquiond
2017-06-14Add a version to be used when parsing compatibility notations mentioning old ...Guillaume Melquiond
2017-06-12Add support for "-bypass-API" argument of "coq_makefile"Matej Košík
2017-05-23Put the list of Coq sources subdirectories in one placeEnrico Tassi
2017-04-12[stm] Port the toplevel to the STM.Emilio Jesus Gallego Arias
2017-04-07Fixes for Drop. to work (decl_mode removal and toplevel -> vernac)Matthieu Sozeau
2016-09-27Merge remote-tracking branch 'github/pr/290' into trunkMaxime Dénès
2016-09-27Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-268.7 now points to Current and 8.6 points to V8_6.Théo Zimmermann
2016-09-25The coqtop options -Q and -R do not affect the ML loadpath anymore.Pierre-Marie Pédrot
2016-09-14Merge branch 'v8.6'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-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
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