coq - The formal proof system

Age	Commit message (Expand)	Author
2012-07-08	verbose compat notations : nicer option name	letouzey
2012-07-05	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey
2012-06-07	Colorization of coqtop messages is turned off by default	letouzey
2012-06-04	Replacing some str with strbrk	ppedrot
2012-06-04	Added a color output to Coqtop.	ppedrot
2012-06-02	Fixed printing error problem... A line had disappeared in a previous patch.	ppedrot
2012-06-02	Flushing formatters before program exit.	ppedrot
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot
2012-05-30	More uniformisation in Pp.warn functions.	ppedrot
2012-05-29	Avoid Dumpglob dependency on Lexer	letouzey
2012-04-12	Remove print call that do not use the pp mechanism	pboutill
2012-04-12	lib directory is cut in 2 cma.	pboutill
2012-03-23	A unified backtrack mechanism, with a basic "Show Script" as side-effect	letouzey
2012-03-02	Noise for nothing	pboutill
2012-01-26	Add support for plugin initialization function	gareuselesinge
2012-01-23	Bug 739: forbid dumpglob while using Coqtop in interactive mode	pboutill
2011-11-21	-user option removal	pboutill
2011-09-05	Remove code concerning the obsolete Set/Unset Undo	letouzey
2011-08-09	Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...	aspiwack
2011-06-20	Add compatibility option "-compat 8.3".	herbelin
2011-05-24	Made the emacs-U option deprecated. Also removed the old code	courtieu
2011-05-13	A new mechanism to handle errors.	aspiwack
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-03-23	Ide: stronger separation from coqtop	letouzey
2011-01-28	Remove the "Boxed" syntaxes and the const_entry_boxed field	letouzey
2010-11-01	Restored checking that _all_ arguments of the command line are meaningful	herbelin
2010-09-14	CoqIDE argv parsing delegated to coqtop	vgross
2010-08-27	* toplevel/Coqtop: Reactivate -dont-load-proofs option.	regisgia
2010-08-27	* lib/Flags: Replace dont_load_proofs by load_proofs since not loading	regisgia
2010-07-29	Rather quick hack to make basic unicode notations available by	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-05-31	CoqIDE goes multiprocess	vgross
2010-05-31	deporting Coq specific code from ide to toplevel.	vgross
2010-05-31	Modifying startup sequence	vgross
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-10-16	note for later : when the tag table is shared, never, ever create two	vgross
2009-10-04	Changed the way to support compatibility with previous versions.	herbelin
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-02	Improved parameterization of Coq:	herbelin
2009-07-01	Support for binding Coq root read-only in -R option	herbelin
2009-04-08	Some dead code removal + cleanups	letouzey
2009-03-14	Better mechanism for loading initial plugins	letouzey
2009-02-11	Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk	notin
2008-12-26	- Suppression date dans configure du trunk	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-12-19	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin
2008-12-17	Sequel of 11697: repair coqtop.byte when contribs are statically linked (+min...	letouzey
2008-12-16	Take advantage of natdynlink when available: almost all contribs become loada...	letouzey
2008-11-22	Fixed bug in VernacExtend printing + missing vernacular printing rules +	herbelin
2008-11-13	Tentative d'amélioration de la robustesse des Makefile générés par	notin