From 405a876ec06bc92168c2323b44a621734dff4901 Mon Sep 17 00:00:00 2001 From: msozeau Date: Mon, 17 Mar 2008 18:54:40 +0000 Subject: Add the possibility of specifying constants to unfold for typeclass resolution. Add [relation] and Setoid's [equiv] as such objects. Considerably simplify resolve_all_evars for typeclass resolution, adding a further refinement (and hack): evars get classified as non-resolvable (using the evar_extra dynamic field) if they are turned into a goal. This makes it possible to perform nested typeclass resolution without looping. We take advantage of that in Classes/Morphisms where [subrelation_tac] is added to the [Morphism] search procedure and calls the apply tactic which itself triggers typeclass resolution. Having [subrelation_tac] as a tactic instead of an instance, we can actually force that it is applied only once in each search branch and avoid looping. We could get rid of the hack when we have real goals-as-evars functionality (hint hint). Also fix some test-suite scripts which were still calling [refl] instead of [reflexivity]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10687 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/bugs/closed/shouldsucceed/1704.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'test-suite/bugs') diff --git a/test-suite/bugs/closed/shouldsucceed/1704.v b/test-suite/bugs/closed/shouldsucceed/1704.v index 81b221690..4b02d5f93 100644 --- a/test-suite/bugs/closed/shouldsucceed/1704.v +++ b/test-suite/bugs/closed/shouldsucceed/1704.v @@ -12,6 +12,6 @@ Axiom r : False -> 0 == 1. Goal 0 == 0. Proof. rewrite r. -refl. +reflexivity. admit. Qed. -- cgit v1.2.3