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

2 files changed, 11 insertions, 7 deletions

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 ->