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