aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Expand)AuthorAge
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* Fixed parsing of -no-native-compiler flag.Gravatar mdenes2013-01-24
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Using library string functions.Gravatar ppedrot2012-12-13
* Ensure that a function declared with a label is used with itGravatar letouzey2012-12-08
* Restoring flush of Welcome message lost in r15148Gravatar herbelin2012-12-06
* Monomorphization (toplevel)Gravatar ppedrot2012-11-26
* Another GC testGravatar ppedrot2012-11-13
* Removed the modification of the GC pressure coefficient, in orderGravatar ppedrot2012-11-12
* Coq is a heavy user of persistent data structures and symbolic ASTs, so theGravatar ppedrot2012-11-06
* Fix test-suite output/* in benchGravatar pboutill2012-10-17
* coqtop -time : display per-command timingsGravatar letouzey2012-10-05
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Made Pp.std_ppcmds opaque.Gravatar ppedrot2012-09-13
* Avoid [Loading ML file ...] messages when launching coqtopGravatar letouzey2012-09-07
* Use fully-qualified Coq.Init.Prelude when starting coqtopGravatar letouzey2012-08-24
* No more states/initial.coq, instead coqtop now requires Prelude.voGravatar letouzey2012-08-23
* Updating headers.Gravatar herbelin2012-08-08
* verbose compat notations : nicer option nameGravatar letouzey2012-07-08
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* Colorization of coqtop messages is turned *off* by defaultGravatar letouzey2012-06-07
* Replacing some str with strbrkGravatar ppedrot2012-06-04
* Added a color output to Coqtop.Gravatar ppedrot2012-06-04
* Fixed printing error problem... A line had disappeared in a previous patch.Gravatar ppedrot2012-06-02
* Flushing formatters before program exit.Gravatar ppedrot2012-06-02
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* Avoid Dumpglob dependency on LexerGravatar letouzey2012-05-29
* Remove print call that do not use the pp mechanismGravatar pboutill2012-04-12
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
* A unified backtrack mechanism, with a basic "Show Script" as side-effectGravatar letouzey2012-03-23
* Noise for nothingGravatar pboutill2012-03-02
* Add support for plugin initialization functionGravatar gareuselesinge2012-01-26
* Bug 739: forbid dumpglob while using Coqtop in interactive modeGravatar pboutill2012-01-23
* -user option removalGravatar pboutill2011-11-21
* Remove code concerning the obsolete Set/Unset UndoGravatar letouzey2011-09-05
* Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...Gravatar aspiwack2011-08-09
* Add compatibility option "-compat 8.3".Gravatar herbelin2011-06-20
* Made the emacs-U option deprecated. Also removed the old codeGravatar courtieu2011-05-24
* A new mechanism to handle errors.Gravatar aspiwack2011-05-13
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Ide: stronger separation from coqtopGravatar letouzey2011-03-23
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Restored checking that _all_ arguments of the command line are meaningfulGravatar herbelin2010-11-01
* CoqIDE argv parsing delegated to coqtopGravatar vgross2010-09-14
* * toplevel/Coqtop: Reactivate -dont-load-proofs option.Gravatar regisgia2010-08-27