coq - The formal proof system

Age	Commit message (Expand)	Author
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-04-08	Add an option -Q (tentative name).	Guillaume Melquiond
2014-04-06	Change handling of loadpath and mlpath.	Guillaume Melquiond
2013-12-22	Adding a finer-grained -bt flag to coqtop only triggering backtraces.	Pierre-Marie Pédrot
2013-11-27	New option --help-XML-protocol to document the XML procol used by -ideslave	Enrico Tassi
2013-08-22	Misc changes around coqtop.ml :	letouzey
2012-12-08	Ensure that a function declared with a label is used with it	letouzey
2012-10-05	coqtop -time : display per-command timings	letouzey
2012-08-23	No more states/initial.coq, instead coqtop now requires Prelude.vo	letouzey
2012-08-08	Updating headers.	herbelin
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-15	Partialy revert "coq_makefile fixup" because old Makefiles still need CAMLP4BIN	pboutill
2012-06-14	coq_makefile fixup	pboutill
2012-06-12	New step in purpose to get both camlp4 and camlp5 compatible coq_makefiles	pboutill
2012-04-12	lib directory is cut in 2 cma.	pboutill
2011-11-21	-user option removal	pboutill
2011-09-27	In Coq_config: get rid of coqsrc and make coqlib optional	glondu
2011-04-28	coqtop -config returns coq returns coq environments at exection time	pboutill
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2011-03-28	Ide_slave: a more robust current_status () function	letouzey
2010-09-14	CoqIDE argv parsing delegated to coqtop	vgross
2010-09-13	Fix unescaped end-of-lines (OCaml warning 29)	glondu
2010-08-31	* By default, load proof terms.	regisgia
2010-08-27	* scripts/Coqc toplevel/Usage:	regisgia
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-08-02	Improved parameterization of Coq:	herbelin
2009-06-13	Correct typo: -noglob takes no argument.	msozeau
2009-02-11	Fix de divers petits problèmes d'installation	notin
2009-02-11	Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk	notin
2009-01-06	Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...	notin
2008-12-26	- Suppression date dans configure du trunk	herbelin
2008-12-19	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin
2008-11-13	Tentative d'amélioration de la robustesse des Makefile générés par	notin
2008-07-18	Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...	notin
2008-06-29	Lissage de la gestion des chemins de chargement de fichiers :	herbelin
2008-06-24	Suppression de l'option -dump-glob et ajout d'une option -no-glob	notin
2006-06-09	Ajout d'une option -with-geoproof à la configuration et à l'exécution	notin
2004-09-03	MAJ options coqtop et coqc	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-01-15	Ajout nouvelles options	herbelin
2002-11-05	Intégration des modifs de la branche mowgli :	herbelin
2002-04-10	backtrack dans l'algo d'unification	barras
2002-03-07	raccourci -l en plus de -load-vernac-source	letouzey
2002-02-27	-dump-glob dans le usage	filliatr
2001-09-18	Ajout d'une option et d'une fonction compile pour fabriquer les .vo	herbelin
2001-04-19	* empty log message *	courant
2001-04-06	bug Print Proof; usage coqtop/coqc	filliatr