coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Document [Info] command.	Arnaud Spiwack	2014-11-01
*	Fix typo in documentation of the [repeat] tactical.	Arnaud Spiwack	2014-10-24
*	Removing remaining documentation of the XML plugin.	Pierre-Marie Pédrot	2014-09-11
*	sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex	Pierre Boutillier	2014-09-03
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Documentation: a simple example for [numgoals].	Arnaud Spiwack	2014-08-05
*	Documentation of [uconstr]: typesetting.	Arnaud Spiwack	2014-08-05
*	Documentation: refine accept uconstr arguments.	Arnaud Spiwack	2014-08-05
*	Document [> … ].	Arnaud Spiwack	2014-08-01
*	Fix English spelling -> American spelling in doc.	Arnaud Spiwack	2014-08-01
*	Document [numgoals] and [guard].	Arnaud Spiwack	2014-08-01
*	Document untyped terms in tactics.	Arnaud Spiwack	2014-07-29
*	Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-...	Arnaud Spiwack	2014-07-25
*	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin	2014-07-13
*	Fix Bug 3131 + Really drop mentions of info in refman.	Pierre Boutillier	2014-04-02
*	Reference the 'external' tactic.	Guillaume Melquiond	2014-01-01
*	Silence some warning about references in documentation.	Guillaume Melquiond	2013-12-03
*	Fix ltac's progress tactical: requires progress in each goal.	aspiwack	2013-11-04
*	Documentation for the backtracking features.	aspiwack	2013-11-02
*	Manual fixed w.r.t. STM	gareuselesinge	2013-08-08
*	Documenting the "appcontext" by default.	ppedrot	2013-05-29
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Added documentation for "r foo" in Ltac debugger.	herbelin	2012-01-20
*	Documentation of appcontext	letouzey	2011-11-29
*	Documentation of the timeout tactical (cf r13917)	letouzey	2011-03-21
*	(Hopefully) clearer explanation of Ltac's context patterns	glondu	2010-10-05
*	Report de la révision #12208 de la v8.2 (correction du bug #2126)	notin	2009-11-03
*	New cleaning phase of the Local/Global option management	herbelin	2009-10-26
*	Ltac doc: only variables are accepted as message_token	glondu	2009-09-23
*	Clarify documentation of ltac repeat	glondu	2009-09-17
*	Report de la révision #12200 (bug #2125)	notin	2009-06-22
*	- Fixed various Overfull in documentation.	herbelin	2009-01-27
*	Backporting from v8.2 to trunk:	herbelin	2009-01-18
*	- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to	msozeau	2008-05-12
*	- Cleanup parsing of binders, reducing to a single production for all	msozeau	2008-05-11
*	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin	2008-02-01
*	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	2008-01-05
*	Changed many refman/*.tex files. Put \label and \index commands that immediat...	emakarov	2007-04-17
*	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-22
*	Réintroduction de l'entrée "integer" dans ltac (apparemment disparue lors	herbelin	2007-02-15
*	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin	2007-02-13
*	MAJ crédits, fresh; documentation apply in	herbelin	2006-10-26
*	Documentation de lazymatch et des extensions de idtac et fail	herbelin	2006-07-11
*	Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé...	herbelin	2006-07-07
*	Documentation Print Ltac qualid; documentation du debugger de ltac.	herbelin	2006-07-05
*	Documentation 'external'	herbelin	2006-07-05
*	Correction comportement clause _ du match goal	herbelin	2006-05-05
*	Nettoyage de l'archive doc et restructuration avant intégration à l'archive	herbelin	2006-02-23