coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)	Enrico Tassi	2014-10-22
*	typo	Enrico Tassi	2014-09-29
*	seems to fix a looping coq-tex (when compiled with camlp4)	Pierre Boutillier	2014-09-18
*	Documenting the [Variant] type definition and the [Nonrecursive Elimination S...	Arnaud Spiwack	2014-09-04
*	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-09-03
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Documenting old but useful command "Print Tables".	Hugo Herbelin	2014-01-13
*	Documenting the tactic-in-term construction.	Pierre-Marie Pédrot	2013-12-11
*	Silence some warning about references in documentation.	Guillaume Melquiond	2013-12-03
*	First stab at documenting Canonical Structures	Enrico Tassi	2013-11-29
*	Manual fixed w.r.t. STM	gareuselesinge	2013-08-08
*	Documentation of the "Local Definition" command.	ppedrot	2013-03-11
*	Added missing documentation of Set Printing Existential Instances.	herbelin	2013-02-21
*	Improving rendering of ...-separated lists and sequences in reference	herbelin	2012-08-11
*	Documentation of records defined with the keywords Inductive and	aspiwack	2012-04-13
*	Added documentation for "Set Parsing Explicit" + fixed mistakenly	herbelin	2012-01-20
*	Fixed a Not_found bug when declaring in a section some implicit	herbelin	2011-12-18
*	Command Arguments: standardizing format of error messages and American spelling.	herbelin	2011-12-17
*	Documentation of Arguments + implicits	gareuselesinge	2011-12-06
*	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-07-16
*	@ in index of refman (last request of bug 2494)	pboutill	2011-04-08
*	Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)	herbelin	2011-04-06
*	Fix formatting issue in refman	glondu	2011-01-12
*	Add "Print Sorted Universes"	glondu	2011-01-11
*	Document DOT output of universe graph	glondu	2010-11-02
*	Added multiple implicit arguments rules per name.	herbelin	2010-10-03
*	Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".	herbelin	2010-06-08
*	Correction in Function documentation	jforest	2010-05-06
*	Applying François Garillot's patch (#2261 in bug tracker) for extended	herbelin	2010-04-22
*	Document Generalizable Variables, and change syntax to	msozeau	2009-11-15
*	Fixed record syntax "{\|x=...; y=...\|}" so that it works with qualified names.	gmelquio	2009-11-04
*	Fixed some typos in the reference manual.	gmelquio	2009-10-29
*	- Fixed various Overfull in documentation.	herbelin	2009-01-27
*	Last changes in type class syntax:	msozeau	2009-01-18
*	- Standardized prefix use of "Local"/"Global" modifiers as decided in	herbelin	2009-01-13
*	Lissage de la gestion des chemins de chargement de fichiers :	herbelin	2008-06-29
*	Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour	herbelin	2008-04-26
*	- Un peu de doc, préparation du CHANGES pour la release.	herbelin	2008-04-15
*	Fix examples in Program documentation and add comindexes for the various	msozeau	2008-03-23
*	Fix the clrewrite tactic, change Relations.v to work on relations in Prop	msozeau	2008-02-09
*	Documentation of CHANGES and refman doc for the implicit argument binder	msozeau	2008-02-08
*	- Documentation des nouvelles options d'implicites (Set Strongly Strict	herbelin	2008-02-06
*	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin	2008-02-01
*	Finish let\| implementation and document it	msozeau	2008-01-31
*	Standardisation du format des références croisées vers Figure, Section, Ch...	herbelin	2008-01-05
*	Ajout possibilité d'options à trois mots.	herbelin	2007-04-29
*	Fixed some typos.	glondu	2007-04-18
*	Changed many refman/*.tex files. Put \label and \index commands that immediat...	emakarov	2007-04-17