aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-pro.tex
Commit message (Expand)AuthorAge
* 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
* Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé...Gravatar herbelin2006-07-07
* Modification des propriétés des fichiers .tex (svn:executable)Gravatar notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty2006-02-24
* Nettoyage de l'archive doc et restructuration avant intégration à l'archiveGravatar herbelin2006-02-23