coq - The formal proof system

Age	Commit message (Expand)	Author
2014-01-13	Documenting old but useful command "Print Tables".	Hugo Herbelin
2013-12-11	Documenting the tactic-in-term construction.	Pierre-Marie Pédrot
2013-12-03	Silence some warning about references in documentation.	Guillaume Melquiond
2013-11-29	First stab at documenting Canonical Structures	Enrico Tassi
2013-08-08	Manual fixed w.r.t. STM	gareuselesinge
2013-03-11	Documentation of the "Local Definition" command.	ppedrot
2013-02-21	Added missing documentation of Set Printing Existential Instances.	herbelin
2012-08-11	Improving rendering of ...-separated lists and sequences in reference	herbelin
2012-04-13	Documentation of records defined with the keywords Inductive and	aspiwack
2012-01-20	Added documentation for "Set Parsing Explicit" + fixed mistakenly	herbelin
2011-12-18	Fixed a Not_found bug when declaring in a section some implicit	herbelin
2011-12-17	Command Arguments: standardizing format of error messages and American spelling.	herbelin
2011-12-06	Documentation of Arguments + implicits	gareuselesinge
2011-07-16	This adds two option tables 'Printing Record' and 'Printing Constructor'	herbelin
2011-07-16	This option disables the use of the '{\| field := ... \|}' notation	herbelin
2011-04-08	@ in index of refman (last request of bug 2494)	pboutill
2011-04-06	Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)	herbelin
2011-01-12	Fix formatting issue in refman	glondu
2011-01-11	Add "Print Sorted Universes"	glondu
2010-11-02	Document DOT output of universe graph	glondu
2010-10-03	Added multiple implicit arguments rules per name.	herbelin
2010-06-08	Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".	herbelin
2010-05-06	Correction in Function documentation	jforest
2010-04-22	Applying François Garillot's patch (#2261 in bug tracker) for extended	herbelin
2009-11-15	Document Generalizable Variables, and change syntax to	msozeau
2009-11-04	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio
2009-10-29	Fixed some typos in the reference manual.	gmelquio
2009-01-27	- Fixed various Overfull in documentation.	herbelin
2009-01-18	Last changes in type class syntax:	msozeau
2009-01-13	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin
2008-06-29	Lissage de la gestion des chemins de chargement de fichiers :	herbelin
2008-04-26	Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour	herbelin
2008-04-15	- Un peu de doc, préparation du CHANGES pour la release.	herbelin
2008-03-23	Fix examples in Program documentation and add comindexes for the various	msozeau
2008-02-09	Fix the clrewrite tactic, change Relations.v to work on relations in Prop	msozeau
2008-02-08	Documentation of CHANGES and refman doc for the implicit argument binder	msozeau
2008-02-06	- Documentation des nouvelles options d'implicites (Set Strongly Strict	herbelin
2008-02-01	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin
2008-01-31	Finish let\| implementation and document it	msozeau
2008-01-05	Standardisation du format des références croisées vers Figure, Section, Ch...	herbelin
2007-04-29	Ajout possibilité d'options à trois mots.	herbelin
2007-04-18	Fixed some typos.	glondu
2007-04-17	Changed many refman/*.tex files. Put \label and \index commands that immediat...	emakarov
2007-04-12	Cleaned doc/common/title.tex file. Increased the space under headers	emakarov
2007-02-07	Meilleur anglais (cf 9619)	herbelin
2007-02-07	Relecture/nettoyage chapitre Gallina; déplacement section Function	herbelin
2006-10-28	Documentation de "Set Printing Universes", "Print Universes" (anciennement	herbelin
2006-07-07	Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé...	herbelin
2006-07-04	Documentation or-pattern	herbelin
2006-02-23	Nettoyage de l'archive doc et restructuration avant intégration à l'archive	herbelin