coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[Sphinx] Move chapter 7 to new infrastructure	Maxime Dénès	2018-04-09
*	Deprecate Focus and Unfocus.	Théo Zimmermann	2018-03-05
*	Fix typos.	Théo Zimmermann	2018-03-04
*	Merge PR #6551: Bracket with goal selector	Maxime Dénès	2018-01-16
\|\
\| *	Documentation and CHANGES for bracket with goal selector.	Théo Zimmermann	2018-01-05
* \|	add optimize_heap tactic for #6488	Paul Steckler	2018-01-03
\|/
*	Add optindex for Set Bullet Behavior.	Gaëtan Gilbert	2017-12-14
*	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