| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2007-08-09 | Modification de control_only_guard, qui utilise maintenant | notin |
| 2007-04-26 | Documentation de Existential et de Show Existential (fixes bug #1294) | notin |
| 2007-04-17 | Changed many refman/*.tex files. Put \label and \index commands that immediat... | emakarov |
| 2006-10-26 | added doc for declarative language | corbinea |
| 2006-07-07 | Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé... | herbelin |
| 2006-02-24 | Modification des propriétés des fichiers .tex (svn:executable) | notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty |
| 2006-02-23 | Nettoyage de l'archive doc et restructuration avant intégration à l'archive | herbelin |
