aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
Commit message (Expand)AuthorAge
* 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
* * lib/Flags: Replace dont_load_proofs by load_proofs since not loadingGravatar regisgia2010-08-27
* Rather quick hack to make basic unicode notations available byGravatar herbelin2010-07-29
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* CoqIDE goes multiprocessGravatar vgross2010-05-31
* deporting Coq specific code from ide to toplevel.Gravatar vgross2010-05-31
* Modifying startup sequenceGravatar vgross2010-05-31
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* note for later : when the tag table is shared, never, ever create twoGravatar vgross2009-10-16
* Changed the way to support compatibility with previous versions.Gravatar herbelin2009-10-04
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17