| Age | Commit message (Expand) | Author |
|---|
| 2018-04-13 | [Sphinx] Move chapter 1 to new infrastructure | Maxime Dénès |
| 2017-10-24 | Documentation: Add various basic constructs to the index. | Johannes Kloos |
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond |
| 2017-07-31 | Fix incorrect use of "At the end". | Sam Pablo Kuper |
| 2017-07-01 | RefMan-gal: improve grammar | William Lawvere |
| 2016-12-06 | Update documentation (bugs #5246 and #5251). | Guillaume Melquiond |
| 2016-06-27 | Adding ability to put any pattern in binders, prefixed by a quote. | Daniel de Rauglaudre |
| 2015-12-14 | Remove a mention of Set Virtual Machine in doc. | Maxime Dénès |
| 2015-12-10 | TYPOGRAPHY: 'non dependent product', just like 'dependent product' is now emp... | Matej Kosik |
| 2015-12-10 | RefMan, ch. 4: Reference Manual: more on the "in pattern" clause and | Hugo Herbelin |
| 2015-12-06 | RefMan, ch. 1 and 2: avoiding using the name "constant" when | Hugo Herbelin |
| 2015-07-30 | Fix some broken Coq scripts in the documentation. | Guillaume Melquiond |
| 2015-03-05 | Preprend Fail to all the expected failures in the documentation. | Guillaume Melquiond |
| 2015-01-29 | Fix some broken Coq scripts in the reference manual. | Guillaume Melquiond |
| 2015-01-13 | More documentation of the Local Definitions and Axioms. | Pierre-Marie Pédrot |
| 2014-09-04 | Documenting the [Variant] type definition and the [Nonrecursive Elimination S... | Arnaud Spiwack |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2013-12-03 | Silence some warning about references in documentation. | Guillaume Melquiond |
| 2013-03-25 | Typo in refman (fix #2962) | letouzey |
| 2013-03-11 | Allowing (Co)Fixpoint to be defined local and Let-style. | ppedrot |
| 2013-03-11 | Documentation of the "Local Definition" command. | ppedrot |
| 2012-08-11 | Improving rendering of ldots in doc (partially done, there are too | herbelin |
| 2012-08-11 | Improving rendering of ...-separated lists and sequences in reference | herbelin |
| 2012-07-05 | ZArith + other : favor the use of modern names instead of compat notations | letouzey |
| 2012-04-13 | Uniformisation in the documentation: remove the use of 'coinductive' in | aspiwack |
| 2012-02-29 | RefMan update about match syntax. | pboutill |
| 2012-02-01 | Corrected a careless cut-and-paste in Gallina description which dated back to... | ppedrot |
| 2011-10-07 | Remove 'status' of Program and explain the :> better, as well as referencing ... | msozeau |
| 2011-09-01 | Bug 2583: Update of the syntax of terms in the reference manual | pboutill |
| 2010-06-08 | Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction". | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2009-09-11 | Add doc of [Context] vernacular. | msozeau |
| 2009-01-27 | - Fixed various Overfull in documentation. | herbelin |
| 2009-01-18 | Backporting from v8.2 to trunk: | herbelin |
| 2008-11-22 | - Fixed minor bug #1994 in the tactic chapter of the manual [doc] | herbelin |
| 2008-04-25 | Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve | herbelin |
| 2008-01-05 | Standardisation du format des références croisées vers Figure, Section, Ch... | herbelin |
| 2007-07-07 | If a fixpoint is not written with an explicit { struct ... }, then | letouzey |
| 2007-04-17 | Changed many refman/*.tex files. Put \label and \index commands that immediat... | emakarov |
| 2007-04-10 | Eliminated warning messages from Hevea. Most warning messages were | emakarov |
| 2007-02-07 | Relecture/nettoyage chapitre Gallina; déplacement section Function | herbelin |
| 2006-09-07 | Updating the doc about Function and co | courtieu |
| 2006-07-17 | MAJ | jforest |
| 2006-07-11 | MAJ doc/refman | notin |
| 2006-07-07 | MAJ du manuel de référence (modules+fixpoints+pose proof) | notin |
| 2006-07-05 | Précisions sur l'Unicode reconnu; typo; ajout Example, Proposition, Corollary. | herbelin |
| 2006-07-04 | Documentation or-pattern | herbelin |
| 2006-06-07 | petites corrections dans la doc de functional xxx. | courtieu |
| 2006-06-07 | mise en texttt d'une commande. | courtieu |
| 2006-06-07 | Changements sur Functional xxx. Plus précis et plus exact. | courtieu |
