coq - The formal proof system

Age	Commit message (Expand)	Author
2015-10-18	Reference Manual: Applying standard style recommendation about not	Hugo Herbelin
2015-10-11	Documenting matching under binders.	Hugo Herbelin
2015-03-22	Qed export -> Qed exporting	Enrico Tassi
2015-02-23	Fixed doc of fresh (was already outdated before fixing #3233).	Pierre Courtieu
2015-02-17	Separate index for vernacular options.	Maxime Dénès
2015-02-14	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi
2015-01-29	Fix index of reference manual.	Guillaume Melquiond
2015-01-21	Reference manual: fix typo in doc of [tryif/then/else].	Arnaud Spiwack
2015-01-14	Reference manual: I had previously omitted the syntax entry for [> t1\|…\|tn].	Arnaud Spiwack
2015-01-14	Reference manual: document tryif/then/else.	Arnaud Spiwack
2015-01-14	Reference manual: document multimatch.	Arnaud Spiwack
2015-01-14	Reference manual: try and improve documentation for Ltac's match.	Arnaud Spiwack
2015-01-14	Reference manual: try and improve the documentation of lazymatch.	Arnaud Spiwack
2015-01-14	Reference manual: document gfail.	Arnaud Spiwack
2014-12-30	Document the new behavior of lazymatch.	Guillaume Melquiond
2014-11-01	Document [Info] command.	Arnaud Spiwack
2014-10-24	Fix typo in documentation of the [repeat] tactical.	Arnaud Spiwack
2014-09-11	Removing remaining documentation of the XML plugin.	Pierre-Marie Pédrot
2014-09-03	sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex	Pierre Boutillier
2014-08-25	"allows to", like "allowing to", is improper	Jason Gross
2014-08-05	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-01	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-07-29	Document untyped terms in tactics.	Arnaud Spiwack
2014-07-25	Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-...	Arnaud Spiwack
2014-07-13	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin
2014-04-02	Fix Bug 3131 + Really drop mentions of info in refman.	Pierre Boutillier
2014-01-01	Reference the 'external' tactic.	Guillaume Melquiond
2013-12-03	Silence some warning about references in documentation.	Guillaume Melquiond
2013-11-04	Fix ltac's progress tactical: requires progress in each goal.	aspiwack
2013-11-02	Documentation for the backtracking features.	aspiwack
2013-08-08	Manual fixed w.r.t. STM	gareuselesinge
2013-05-29	Documenting the "appcontext" by default.	ppedrot
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2012-01-20	Added documentation for "r foo" in Ltac debugger.	herbelin
2011-11-29	Documentation of appcontext	letouzey
2011-03-21	Documentation of the timeout tactical (cf r13917)	letouzey
2010-10-05	(Hopefully) clearer explanation of Ltac's context patterns	glondu
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