aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqinit.ml
Commit message (Expand)AuthorAge
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* Fix #4793: Coq 8.6 should accept -compat 8.6Gravatar Maxime Dénès2016-07-06
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* coqtop: Add ltac/ to search path.Gravatar Matthieu Sozeau2016-06-02
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Accept option -compat 8.5. (Fix bug #4393)Gravatar Guillaume Melquiond2015-10-29
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-05-05
|\|
| * Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
| * No longer add dev/ to the LoadPath, only to the ML path.Gravatar Guillaume Melquiond2015-04-17
* | Merge branch 'v8.5' into trunkGravatar Pierre Letouzey2015-04-09
|\|
| * Remove Mltop.add_path as it is no longer possible to import files from subdir...Gravatar Guillaume Melquiond2015-04-02
| * Fixing inclusion of user contrib directory in the loadpath.Gravatar Pierre-Marie Pédrot2015-04-01
* | Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-02-27
| * 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
|/
* Update headers.Gravatar Maxime Dénès2015-01-12
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Fix ML paths (thanks Jean-Marc Notin for bisecting it)Gravatar Enrico Tassi2014-10-14
* Coqinit: look in toploop/ even if configured with -localGravatar Enrico Tassi2014-10-13
* Prerequisite to fix stm test-suite when not in -localGravatar Pierre Boutillier2014-08-25
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* cut toploop(s) out of coqtop: now they are loaded dynamicallyGravatar Enrico Tassi2014-06-25
* Add an option -Q (tentative name).Gravatar Guillaume Melquiond2014-04-08
* Change handling of loadpath and mlpath.Gravatar Guillaume Melquiond2014-04-06
* Lets coqtop use a slashGravatar Virgile Prevosto2014-03-06
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Updating the backtrace handling mechanism to accomodate the newGravatar ppedrot2013-02-18
* Actually adding backtrace handling.Gravatar ppedrot2013-01-28
* Added backtrace information to anomaliesGravatar ppedrot2013-01-28
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Ensure that a function declared with a label is used with itGravatar letouzey2012-12-08
* Monomorphization (toplevel)Gravatar ppedrot2012-11-26
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
* Updating headers.Gravatar herbelin2012-08-08
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
* /home/pirbo/.coqrc* are read againGravatar pboutill2011-11-21
* -user option removalGravatar pboutill2011-11-21