coq - The formal proof system

Age	Commit message (Expand)	Author
2014-12-09	refman: switch all source files to utf8	Pierre Letouzey
2014-10-22	Move 'Arguments: clear implicits' to 2.7.4 (Close 2891)	Enrico Tassi
2014-09-29	typo	Enrico Tassi
2014-09-18	seems to fix a looping coq-tex (when compiled with camlp4)	Pierre Boutillier
2014-09-04	Documenting the [Variant] type definition and the [Nonrecursive Elimination S...	Arnaud Spiwack
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-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