coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Small improvements suggested in comments to PR #8086.	Zeimer	2018-07-20
\|
*	Improved chapter 'The tactic language' of the Reference Manual.	Zeimer	2018-07-20
\|
*	fixed typo for assert_suceed	charguer	2018-07-10
\|
*	[doc] Allow more than one signature and name per Sphinx object	Clément Pit-Claudel	2018-05-25
\| \| \| \|	As discussed in GH-7556.
*	[sphinx] Fix new warnings related to tacn, cmd, opt...	Théo Zimmermann	2018-05-09
\|
*	[sphinx] Add indices for only, all and par.	Théo Zimmermann	2018-05-05
\|
*	Clean-up around cmd documentation.	Théo Zimmermann	2018-05-05
\| \| \| \|	In particular, remove trailing dots.
*	[sphinx] Replace remaining `@natural` by `@num`.	Théo Zimmermann	2018-05-05
\|
*	[sphinx] Use references for command Info.	Théo Zimmermann	2018-05-05
\|
*	Fix error messages and make them consistent.	Théo Zimmermann	2018-05-05
\| \| \| \|	All the error messages start with a capitalized letter and end with a dot.
*	Clean-up around options.	Théo Zimmermann	2018-05-05
\| \| \| \| \| \|	- Remove all trailing dots. - There is only one Bullet Behavior option. - Replaces `@natural` and `@integer` by `@num`.
*	[sphinx] Fix some references.	Théo Zimmermann	2018-05-05
\|
*	Strict focusing using Default Goal Selector.	Gaëtan Gilbert	2018-04-29
\| \| \| \| \| \| \| \| \| \| \| \|	We add a [SelectAlreadyFocused] constructor to [goal_selector] (read "!") which causes a failure when there's not exactly 1 goal and otherwise is a noop. Then [Set Default Goal Selector "!".] puts us in "strict focusing" mode where we can only run tactics if we have only one goal or use a selector. Closes #6689.
*	[Sphinx] Clean-up indices	Maxime Dénès	2018-04-16
\|
*	[Sphinx] Fix all remaining warnings.	Maxime Dénès	2018-04-14
\|
*	[Sphinx] Add chapter 9.	Théo Zimmermann	2018-04-14
\| \| \| \|	Chapter ported by Théo Zimmermann and Maxime Dénès.
*	[Sphinx] Move chapter 9 to new infrastructure.	Théo Zimmermann	2018-04-14