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