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