| Age | Commit message (Expand) | Author |
| 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 |
| 2007-04-17 | Changed many refman/*.tex files. Put \label and \index commands that immediat... | emakarov |
| 2007-04-12 | Cleaned doc/common/title.tex file. Increased the space under headers | emakarov |
| 2007-02-07 | Meilleur anglais (cf 9619) | herbelin |
| 2007-02-07 | Relecture/nettoyage chapitre Gallina; déplacement section Function | herbelin |
| 2006-10-28 | Documentation de "Set Printing Universes", "Print Universes" (anciennement | herbelin |
| 2006-07-07 | Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé... | herbelin |
| 2006-07-04 | Documentation or-pattern | herbelin |