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, 19 insertions, 1 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c18b0e045..47be84460 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -341,9 +341,27 @@ let class_of_constr c =
 	App (c, _) -> extract_ind c
       | _ -> extract_ind c
 
+(* To embed a boolean for resolvability status.
+   This is essentially a hack to mark which evars correspond to 
+   goals and do not need to be resolved when we have nested [resolve_all_evars] 
+   calls (e.g. when doing apply in an External hint in typeclass_instances).
+   Would be solved by having real evars-as-goals. *)
+
+let ((bool_in : bool -> Dyn.t),
+    (bool_out : Dyn.t -> bool)) = Dyn.create "bool"
+  
+let is_resolvable evi =
+  match evi.evar_extra with
+      Some t -> if Dyn.tag t = "bool" then bool_out t else true
+    | None -> true
+	
+let mark_unresolvable evi = 
+  { evi with evar_extra = Some (bool_in false) }
+
 let has_typeclasses evd =
   Evd.fold (fun ev evi has -> has || 
-    (evi.evar_body = Evar_empty && class_of_constr evi.evar_concl <> None))
+    (evi.evar_body = Evar_empty && class_of_constr evi.evar_concl <> None 
+	&& is_resolvable evi))
     evd false
 
 let resolve_typeclasses ?(onlyargs=false) ?(all=true) env sigma evd =