aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-pro.tex
Commit message (Expand)AuthorAge
* Avoid generated names for html pages of the reference manual (bug #4742).Gravatar Guillaume Melquiond2017-09-22
* Adding documentation for Printing Focused option.Gravatar Pierre Courtieu2017-08-17
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
| * Document Show ident.Gravatar Théo Zimmermann2017-06-13
* | Remove commented documentation for Show Tree.Gravatar Théo Zimmermann2017-06-12
* | [vernac] Remove `Save thm id.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
* | [vernac] Remove `Save.` command.Gravatar Emilio Jesus Gallego Arias2017-05-23
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
|\|
| * Fix outdated description in RefMan.Gravatar Théo Zimmermann2017-05-03
* | Document Show Match, add ref to that in match variants/extensionsGravatar Paul Steckler2017-03-17
* | Fix V7 syntax in refman.Gravatar Théo Zimmermann2017-02-20
|/
* Documenting Set Bullet Behavior.Gravatar Hugo Herbelin2016-01-20
* Proof using: do not clear unused section hyps automaticallyGravatar Enrico Tassi2015-12-15
* Fix a few latex errors in documentation of Proof Using (e.g. \tt*).Gravatar Guillaume Melquiond2015-10-10
* Proof using: let-in policy, optional auto-clear, forward closure*Gravatar Enrico Tassi2015-10-08
* Refman: document Show Universes.Gravatar Matthieu Sozeau2015-07-22
* Separate index for vernacular options.Gravatar Maxime Dénès2015-02-17
* Remove documentation of non-existing Show Implicits command.Gravatar Maxime Dénès2015-02-17
* Fix some broken Coq scripts in the reference manual.Gravatar Guillaume Melquiond2015-01-29
* Reference Manual: Documenting new printing of evars and new effect ofGravatar Hugo Herbelin2015-01-24
* Fixed and extend bullet related info/error messages. + doc.Gravatar Pierre Courtieu2015-01-08
* Added more informative messages about bullets.Gravatar Pierre Courtieu2015-01-05
* Updating documentation about bullets.Gravatar Pierre Courtieu2015-01-05
* Better doc and a few fixes for Proof using.Gravatar Enrico Tassi2014-12-19
* Proof using: New vernacular to name sets of section variablesGravatar Enrico Tassi2014-12-18
* Document (some) Proof using syntax + the new Optimize commandsGravatar Enrico Tassi2014-11-12
* Removing deactivated command Show Tree.Gravatar Hugo Herbelin2014-10-03
* Documenting the new Undo semanticsGravatar Enrico Tassi2014-09-09
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Uncountably many bullets (+,-,*,++,--,**,+++,...).Gravatar Hugo Herbelin2014-08-05
* Making references to Proof General and CoqIDE uniform in Reference Manual.Gravatar Hugo Herbelin2014-08-05
* Added missing documentation of Set Printing Existential Instances.Gravatar herbelin2013-02-21
* Improving rendering of ldots in doc (partially done, there are tooGravatar herbelin2012-08-11
* Typo in r15654Gravatar herbelin2012-08-07
* documentation of bullets (forward port from v8.4).Gravatar courtieu2012-07-25
* Addedum to documentation of bullets: I now use the dedicated coq_exampleGravatar aspiwack2012-05-10
* Documentation for Unfocused, braces and bullets.Gravatar aspiwack2012-05-10
* Remove old proof-managment commands Suspend/ResumeGravatar letouzey2012-03-23
* Documentation for Grab Existential Variables.Gravatar aspiwack2012-02-07
* Proof using ...Gravatar gareuselesinge2011-12-12
* Remove code concerning the obsolete Set/Unset UndoGravatar letouzey2011-09-05
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Added full documentation for mathematical mode (draft version)Gravatar corbinea2008-01-29
* Standardisation du format des références croisées vers Figure, Section, Ch...Gravatar herbelin2008-01-05
* Erreur de copier/coller dans la section GuardedGravatar notin2007-08-20
* Modification de control_only_guard, qui utilise maintenantGravatar notin2007-08-09
* Documentation de Existential et de Show Existential (fixes bug #1294)Gravatar notin2007-04-26
* Changed many refman/*.tex files. Put \label and \index commands that immediat...Gravatar emakarov2007-04-17
* added doc for declarative languageGravatar corbinea2006-10-26