coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-11-29	Fixing printing of apply in (continuation of #12246).	Hugo Herbelin

2020-11-16	Avoid exposing an internal names when "intros _ H" fails.	Hugo Herbelin

2019-10-29	`assert_succeeds`&`assert_fails`: multisuccess fix	Jason Gross
	These tactics now work correctly with multisuccess tactics by wrapping the tactic argument in `once`. Fixes #10965
2018-10-04	test-suite: cleaning	Vincent Laporte

2017-10-19	Moving bug numbers to BZ# format in the test-suite.	Théo Zimmermann
	Compared to the original proposition (59a594b in #960), this commit only changes files containing bug numbers that are also PR numbers.
2017-05-17	A fix for #5390 (a useful error on used introduction names was masked).	Hugo Herbelin
	With the "apply in" introduction pattern, and the backtrack possibly done in "apply" over the components of conjunctions (descend_in_conjunctions), the reasons for failing might have different sources. We give priority to the detection of used names over other (unification) errors so that an error there is not masked in the backtracking made by descend_in_conjunctions. Of course, the question of what best unification error to give in the presence of backtracking is still open.
2011-12-17	Bypassing the use of (currently unimplemented) "Show Script" in tests	herbelin
	that used it. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14802 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-04-24	Timide tentative de clarification du statut de l'opérateur de filtrage	herbelin
	PCase dans le type pattern: le type pattern est utilisé essentiellement dans ltac, il est normalement obtenu sans typage, et ce via rawconstr (sauf cas de filtrage ltac non linéaire où il est obtenu de constr). Le cas d'un filtrage sur un "if" doit être traité à part car sans le type, il est impossible de savoir le nombre d'arguments du constructeur puisque par définition du "if", ceux-ci ne sont pas liants et ne laissent pas dans la syntaxe concrète (résolution au passage du bug #1070, dû à un filtrage incomplet dans le passage de pattern à rawconstr permettant l'affichage des pattern). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8728 85f007b7-540e-0410-9357-904b9bb8a0f7
2005-12-23	Test printing of Tactic Notation which was broken until dec 2005	herbelin
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7707 85f007b7-540e-0410-9357-904b9bb8a0f7