One more fix for rewrite: disallow resolving of the (partial) constraints

happening silently in w_unify and handle this explicitely. Class resolution
filters now can test the existential key. Fixes Ergo contrib.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16571 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 7 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c14f107ec6..6da6624228 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -481,19 +481,19 @@ let mark_unresolvable evi = mark_resolvability false evi
 let mark_resolvable evi = mark_resolvability true evi
 
 open Evar_kinds
-type evar_filter = Evar_kinds.t -> bool
+type evar_filter = existential_key -> Evar_kinds.t -> bool
 
-let all_evars _ = true
-let all_goals = function GoalEvar -> true | _ -> false
-let no_goals evi = not (all_goals evi)
-let no_goals_or_obligations = function
+let all_evars _ _ = true
+let all_goals _ = function GoalEvar -> true | _ -> false
+let no_goals ev evi = not (all_goals ev evi)
+let no_goals_or_obligations _ = function
   | GoalEvar | QuestionMark _ -> false
   | _ -> true
 
 let mark_resolvability filter b sigma =
   Evd.fold_undefined 
     (fun ev evi evs ->
-     if filter (snd evi.evar_source) then
+     if filter ev (snd evi.evar_source) then
        Evd.add evs ev (mark_resolvability_undef b evi)
      else Evd.add evs ev evi)
   sigma (Evd.defined_evars sigma)
@@ -503,7 +503,7 @@ let mark_resolvables sigma = mark_resolvability all_evars true sigma
 
 let has_typeclasses filter evd =
   Evd.fold_undefined (fun ev evi has -> has ||
-    (filter (snd evi.evar_source) && is_class_evar evd evi && is_resolvable evi))
+    (filter ev (snd evi.evar_source) && is_class_evar evd evi && is_resolvable evi))
     evd false
 
 let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)