| Age | Commit message (Expand) | Author |
| 2018-01-16 | Merge PR #6551: Bracket with goal selector | Maxime Dénès |
| 2018-01-05 | Documentation and CHANGES for bracket with goal selector. | Théo Zimmermann |
| 2018-01-03 | add optimize_heap tactic for #6488 | Paul Steckler |
| 2017-12-14 | Add optindex for Set Bullet Behavior. | Gaëtan Gilbert |
| 2017-09-22 | Avoid generated names for html pages of the reference manual (bug #4742). | Guillaume Melquiond |
| 2017-08-17 | Adding documentation for Printing Focused option. | Pierre Courtieu |
| 2017-07-04 | Merge branch 'v8.6' | Pierre-Marie Pédrot |
| 2017-06-13 | Document Show ident. | Théo Zimmermann |
| 2017-06-12 | Remove commented documentation for Show Tree. | Théo Zimmermann |
| 2017-05-23 | [vernac] Remove `Save thm id.` command. | Emilio Jesus Gallego Arias |
| 2017-05-23 | [vernac] Remove `Save.` command. | Emilio Jesus Gallego Arias |
| 2017-05-17 | Merge branch 'v8.6' | Pierre-Marie Pédrot |
| 2017-05-03 | Fix outdated description in RefMan. | Théo Zimmermann |
| 2017-03-17 | Document Show Match, add ref to that in match variants/extensions | Paul Steckler |
| 2017-02-20 | Fix V7 syntax in refman. | Théo Zimmermann |
| 2016-01-20 | Documenting Set Bullet Behavior. | Hugo Herbelin |
| 2015-12-15 | Proof using: do not clear unused section hyps automatically | Enrico Tassi |
| 2015-10-10 | Fix a few latex errors in documentation of Proof Using (e.g. \tt*). | Guillaume Melquiond |
| 2015-10-08 | Proof using: let-in policy, optional auto-clear, forward closure* | Enrico Tassi |
| 2015-07-22 | Refman: document Show Universes. | Matthieu Sozeau |
| 2015-02-17 | Separate index for vernacular options. | Maxime Dénès |
| 2015-02-17 | Remove documentation of non-existing Show Implicits command. | Maxime Dénès |
| 2015-01-29 | Fix some broken Coq scripts in the reference manual. | Guillaume Melquiond |
| 2015-01-24 | Reference Manual: Documenting new printing of evars and new effect of | Hugo Herbelin |
| 2015-01-08 | Fixed and extend bullet related info/error messages. + doc. | Pierre Courtieu |
| 2015-01-05 | Added more informative messages about bullets. | Pierre Courtieu |
| 2015-01-05 | Updating documentation about bullets. | Pierre Courtieu |
| 2014-12-19 | Better doc and a few fixes for Proof using. | Enrico Tassi |
| 2014-12-18 | Proof using: New vernacular to name sets of section variables | Enrico Tassi |
| 2014-11-12 | Document (some) Proof using syntax + the new Optimize commands | Enrico Tassi |
| 2014-10-03 | Removing deactivated command Show Tree. | Hugo Herbelin |
| 2014-09-09 | Documenting the new Undo semantics | Enrico Tassi |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-05 | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin |
| 2014-08-05 | Making references to Proof General and CoqIDE uniform in Reference Manual. | Hugo Herbelin |
| 2013-02-21 | Added missing documentation of Set Printing Existential Instances. | herbelin |
| 2012-08-11 | Improving rendering of ldots in doc (partially done, there are too | herbelin |
| 2012-08-07 | Typo in r15654 | herbelin |
| 2012-07-25 | documentation of bullets (forward port from v8.4). | courtieu |
| 2012-05-10 | Addedum to documentation of bullets: I now use the dedicated coq_example | aspiwack |
| 2012-05-10 | Documentation for Unfocused, braces and bullets. | aspiwack |
| 2012-03-23 | Remove old proof-managment commands Suspend/Resume | letouzey |
| 2012-02-07 | Documentation for Grab Existential Variables. | aspiwack |
| 2011-12-12 | Proof using ... | gareuselesinge |
| 2011-09-05 | Remove code concerning the obsolete Set/Unset Undo | letouzey |
| 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 |
| 2008-01-29 | Added full documentation for mathematical mode (draft version) | corbinea |
| 2008-01-05 | Standardisation du format des références croisées vers Figure, Section, Ch... | herbelin |
| 2007-08-20 | Erreur de copier/coller dans la section Guarded | notin |