coq - The formal proof system

Age	Commit message (Expand)	Author
2009-11-03	Report de la révision #12208 de la v8.2 (correction du bug #2126)	notin
2009-10-26	New cleaning phase of the Local/Global option management	herbelin
2009-09-23	Ltac doc: only variables are accepted as message_token	glondu
2009-09-17	Clarify documentation of ltac repeat	glondu
2009-06-22	Report de la révision #12200 (bug #2125)	notin
2009-01-27	- Fixed various Overfull in documentation.	herbelin
2009-01-18	Backporting from v8.2 to trunk:	herbelin
2008-05-12	- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to	msozeau
2008-05-11	- Cleanup parsing of binders, reducing to a single production for all	msozeau
2008-02-01	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin
2008-01-05	Added a note about the ambiguity of the syntax "qualid" in "tacarg"	herbelin
2008-01-05	Standardisation du format des références croisées vers Figure, Section, Ch...	herbelin
2007-04-17	Changed many refman/*.tex files. Put \label and \index commands that immediat...	emakarov
2007-02-22	doc: typo/english: "is left associating" -> "is left-associative".	lmamane
2007-02-22	Documentation of tactical "t1 \|\| t2": t2 is executed if t1 fails to	lmamane
2007-02-15	Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors	herbelin
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2006-10-26	MAJ crédits, fresh; documentation apply in	herbelin
2006-07-11	Documentation de lazymatch et des extensions de idtac et fail	herbelin
2006-07-07	Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé...	herbelin
2006-07-05	Documentation Print Ltac qualid; documentation du debugger de ltac.	herbelin
2006-07-05	Documentation 'external'	herbelin
2006-05-05	Correction comportement clause _ du match goal	herbelin
2006-02-23	Nettoyage de l'archive doc et restructuration avant intégration à l'archive	herbelin