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

2 files changed, 27 insertions, 1 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c18b0e0450..47be844600 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 =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c06006ad05..dba60234bc 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -65,6 +65,14 @@ val is_class : inductive -> bool
 val class_of_constr : constr -> typeclass option
 
 val resolve_typeclass : env -> evar -> evar_info -> evar_defs * bool -> evar_defs * bool
+
+(* Use evar_extra for marking resolvable evars. *)
+val bool_in : bool -> Dyn.t
+val bool_out : Dyn.t -> bool
+
+val is_resolvable : evar_info -> bool
+val mark_unresolvable : evar_info -> evar_info
+
 val resolve_typeclasses : ?onlyargs:bool -> ?all:bool -> env -> evar_map -> evar_defs -> evar_defs
 
 val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref