coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Tentative fix of test-suite file to avoid loop	Matthieu Sozeau	2016-06-16
\| \| \| \| \|	Looping on jenkins only, couldn't reproduce locally. To be investigated further.
*	Cleanup and refactoring	Matthieu Sozeau	2016-06-16
\|
*	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
\| \| \| \| \|	As noticed by C. Cohen it was confusingly different from standard notation.
*	Example given at DeepSpec workshop	Matthieu Sozeau	2016-06-16
\|
*	Purely refactoring and code/API cleanup.	Matthieu Sozeau	2016-06-16
\| \| \| \|	Fix test-suite files
*	bteauto: a Proofview.tactic for multiple goals	Matthieu Sozeau	2016-06-16
	Add an option to force backtracking at toplevel, which is used by default when calling typeclasses eauto on a set of goals. They might be depended on by other subgoals, so the tactic should be backtracking by default, a once can make it not backtrack.