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

4 files changed, 19 insertions, 15 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c14f107ec..6da662422 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)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c8f41841a..028e393f2 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -78,7 +78,7 @@ val is_implicit_arg : Evar_kinds.t -> bool
 val instance_constructor : typeclass -> constr list -> constr option * types
 
 (** Filter which evars to consider for resolution. *)
-type evar_filter = Evar_kinds.t -> bool
+type evar_filter = existential_key -> Evar_kinds.t -> bool
 val all_evars : evar_filter
 val all_goals : evar_filter
 val no_goals : evar_filter
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 84149bead..fb41c2e15 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -677,7 +677,7 @@ let resolve_all_evars debug m env p oevd do_split fail =
 
 let initial_select_evars filter =
   fun evd ev evi ->
-    filter (snd evi.Evd.evar_source) &&
+    filter ev (snd evi.Evd.evar_source) &&
     Typeclasses.is_class_evar evd evi
 
 let resolve_typeclass_evars debug m env evd filter split fail =
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 50f751a1d..e21ee7f23 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -304,7 +304,7 @@ let rewrite_unif_flags = {
   Unification.modulo_delta_types = full_transparent_state;
   Unification.modulo_delta_in_merge = None;
   Unification.check_applied_meta_types = true;
-  Unification.resolve_evars = true;
+  Unification.resolve_evars = false;
   Unification.use_pattern_unification = true;
   Unification.use_meta_bound_pattern_unification = true;
   Unification.frozen_evars = ExistentialSet.empty;
@@ -321,7 +321,7 @@ let rewrite2_unif_flags =
      Unification.modulo_delta_types = conv_transparent_state;
      Unification.modulo_delta_in_merge = None;
      Unification.check_applied_meta_types = true;
-     Unification.resolve_evars = true;
+     Unification.resolve_evars = false;
      Unification.use_pattern_unification = true;
      Unification.use_meta_bound_pattern_unification = true;
      Unification.frozen_evars = ExistentialSet.empty;
@@ -339,7 +339,7 @@ let general_rewrite_unif_flags () =
        Unification.modulo_delta_types = ts;
        Unification.modulo_delta_in_merge = None;
        Unification.check_applied_meta_types = true;
-       Unification.resolve_evars = true;
+       Unification.resolve_evars = false;
        Unification.use_pattern_unification = true;
        Unification.use_meta_bound_pattern_unification = true;
        Unification.frozen_evars = ExistentialSet.empty;
@@ -378,7 +378,10 @@ let extend_evd sigma ext sigma' =
     Evd.add acc i (Evd.find sigma' i))
     ext sigma
 
-let unify_eqn env sigma hypinfo by t =
+let no_constraints cstrs = 
+  fun ev _ -> not (Int.Set.mem ev cstrs)
+
+let unify_eqn env (sigma, cstrs) hypinfo by t =
   if isEvar t then None
   else try
     let {cl=cl; ext=ext; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = 
@@ -395,7 +398,8 @@ let unify_eqn env sigma hypinfo by t =
       | None ->
 	  let env' = clenv_unify ~flags:!hypinfo.flags CONV left t cl in
 	  let env' = Clenvtac.clenv_pose_dependent_evars true env' in
-	  let evd' = Typeclasses.resolve_typeclasses ~fail:true env'.env env'.evd in
+	  let evd' = Typeclasses.resolve_typeclasses ~filter:(no_constraints cstrs)
+	    ~fail:true env'.env env'.evd in
 	  let env' = { env' with evd = evd' } in
 	  let env', prf = solve_remaining_by by env' (Clenv.clenv_value env') in	   
 	  let nf c = Evarutil.nf_evar env'.evd (Clenv.clenv_nf_meta env' c) in
@@ -635,7 +639,7 @@ let apply_rule hypinfo by loccs : strategy =
     fun env avoid t ty cstr evars ->
       if not (eq_env !hypinfo.cl.env env) then
 	hypinfo := refresh_hypinfo env (goalevars evars) !hypinfo;
-      let unif = unify_eqn env (goalevars evars) hypinfo by t in
+      let unif = unify_eqn env evars hypinfo by t in
 	if not (Option.is_empty unif) then incr occ;
 	match unif with
 	| Some (evd', (prf, (car, rel, c1, c2))) when is_occ !occ ->