coq - The formal proof system

Age	Commit message (Expand)	Author
2014-12-25	Document 6d5b56d971 (forbid Require inside modules).	Maxime Dénès
2014-12-12	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu
2014-12-09	refman: avoid label names with whitespace (unsupported in html)	Pierre Letouzey
2014-09-03	sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex	Pierre Boutillier
2014-09-03	Update RefMan with respect to new loadpath management	Pierre Boutillier
2014-08-25	"allows to", like "allowing to", is improper	Jason Gross
2014-08-16	Removing documentation related to the deprecated State machinery.	Pierre-Marie Pédrot
2014-07-21	Documenting the changes of Locate semantics.	Pierre-Marie Pédrot
2014-06-21	Fixing grammar in doc of Opaque as proposed by Jason (#3389).	Hugo Herbelin
2014-03-20	Documenting the Print Strategy command.	Pierre-Marie Pédrot
2014-02-02	Removing the [Require "file"] syntax.	Pierre-Marie Pédrot
2014-01-13	Fixing typo in reference manual from previous commit	Hugo Herbelin
2014-01-13	Documenting old but useful command "Print Tables".	Hugo Herbelin
2013-04-17	Renaming SearchAbout into Search and Search into SearchHead.	herbelin
2012-10-30	Documenting the 'Printing Transparent/All Dependencies' command.	ppedrot
2012-08-11	Improving rendering of ldots in doc (partially done, there are too	herbelin
2012-08-03	Document the command Add/Remove Search Blacklist	letouzey
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2012-03-23	Documentation of last commit concerning Backtracking	letouzey
2012-03-23	Remove old proof-managment commands Suspend/Resume	letouzey
2011-09-01	Bug 2583: Update of the syntax of terms in the reference manual	pboutill
2011-04-12	remove old traces of SearchIsos (never ported to 7.x nor 8.x)	letouzey
2011-03-17	An option "Set Default Timeout n."	letouzey
2010-11-19	SearchAbout: who has never been annoyed by the [ ] syntax ?	letouzey
2010-10-06	Remove Explain* vernacs	glondu
2010-10-06	Remove VernacGo	glondu
2010-09-23	Added a section in the documentation of Vernacular commands about Set/Unset/T...	aspiwack
2010-06-08	Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".	herbelin
2010-06-04	A new command Compute foo, shortcut for Eval vm_compute in foo	letouzey
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-03-11	Update manual on search commands	puech
2010-01-28	New command Declare Reduction <id> := <conv_expr>.	letouzey
2010-01-14	Document Local Declare ML Module	glondu
2009-10-27	Documentation of the Local and Global modifiers.	herbelin
2009-06-26	Add doc for [Print Opaque Dependencies] and a better explanation for the	msozeau
2009-04-28	Backporting 12112 from v8.2 branch to trunk (fixing documentation bugs	herbelin
2009-03-14	RefMan: a label defined twice	letouzey
2009-03-04	doc et CHANGES pour la commande Timeout	barras
2009-01-01	- Fixed bug #2021 (uncaught exception with injection/discriminate when	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-10-29	Document native "Declare ML Module"	glondu
2008-10-19	- Export de pattern_ident vers les ARGUMENT EXTEND and co.	herbelin
2008-10-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin
2008-06-29	Lissage de la gestion des chemins de chargement de fichiers :	herbelin
2008-06-09	- Documentation de admit et Print Assumptions.	herbelin
2008-05-22	Strategy commands are now exported	barras
2008-05-21	refined the conversion oracle	barras
2008-04-13	Bugs, nettoyage, et améliorations diverses	herbelin
2008-04-03	Chgts mineurs:	herbelin