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

1 files changed, 3 insertions, 3 deletions

diff --git a/test-suite/typeclasses/unification_delta.v b/test-suite/typeclasses/unification_delta.v
index b8789f26e..663a837f3 100644
--- a/test-suite/typeclasses/unification_delta.v
+++ b/test-suite/typeclasses/unification_delta.v
@@ -7,15 +7,15 @@ Lemma bla : forall [ ! Equivalence A (eqA : relation A) ] x y, eqA x y -> eqA y
 Proof.
   intros.
   rewrite H0.
-  refl.
+  reflexivity.
 Defined.
 
 Lemma bla' : forall [ ! Equivalence A (eqA : relation A) ] x y, eqA x y -> eqA y x.
 Proof.
   intros.
-  (* Need delta no [relation] to unify with the right lemmas. *)
+  (* Need delta on [relation] to unify with the right lemmas. *)
   rewrite <- H0.
-  refl.
+  reflexivity.
 Qed.
 
 Axiom euclid : nat -> { x : nat | x > 0 } -> nat.