Fix anomaly when using typeclass resolution with filtered hyps in evars.

Make setoid_rewrite-through-rewrite's selection of occurences more
robust: do not try unification with reduction if not needed.
This changes a few scripts that were using reduction in a far from
obvious way and could break more.


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

2 files changed, 33 insertions, 18 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index bd632b59ad..f89528487a 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -65,14 +65,20 @@ let valid goals p res_sigma l =
       !res_sigma goals l
   in raise (Found evm)
 
+let evar_filter evi =
+  let hyps' = evar_filtered_context evi in
+    { evi with 
+      evar_hyps = Environ.val_of_named_context hyps';
+      evar_filter = List.map (fun _ -> true) hyps' }
+      
 let evars_to_goals p evm =
   let goals, evm' =
     Evd.fold
       (fun ev evi (gls, evm') ->
 	if evi.evar_body = Evar_empty then
 	  let evi', goal = p evm ev evi in
-	    if goal then 
-	      ((ev,evi) :: gls, Evd.add evm' ev evi')
+	    if goal then
+	      ((ev, evi') :: gls, Evd.add evm' ev evi')
 	    else (gls, Evd.add evm' ev evi')
 	else (gls, Evd.add evm' ev evi))
       evm ([], Evd.empty)
@@ -252,8 +258,11 @@ let make_resolve_hyp env sigma st flags only_classes pri (id, _, cty) =
 	[make_exact_entry pri; make_apply_entry env sigma flags pri]
     else []
 
+let pf_filtered_hyps gls = 
+  evar_filtered_context (sig_it gls)
+
 let make_autogoal_hints only_classes ?(st=full_transparent_state) g =
-  let sign = pf_hyps g in
+  let sign = pf_filtered_hyps g in
   let hintlist = list_map_append (pf_apply make_resolve_hyp g st (true,false,false) only_classes None) sign in
     Hint_db.add_list hintlist (Hint_db.empty st true)
   
@@ -549,20 +558,24 @@ let resolve_all_evars debug m env p oevd do_split fail =
   let split = if do_split then split_evars oevd else [Intset.empty] in
   let p = if do_split then
     fun comp evd ev evi -> 
-      (try let oevi = Evd.find oevd ev in
-	     if Typeclasses.is_resolvable oevi then
-	       Typeclasses.mark_unresolvable evi, (Intset.mem ev comp &&
-						      p evd ev evi)
-	     else evi, false
-	with Not_found ->
-	  Typeclasses.mark_unresolvable evi, p evd ev evi)
+      if evi.evar_body = Evar_empty then
+	(try let oevi = Evd.find oevd ev in
+	       if Typeclasses.is_resolvable oevi then
+		 Typeclasses.mark_unresolvable evi, (Intset.mem ev comp &&
+							p evd ev evi)
+	       else evi, false
+	  with Not_found ->
+	    Typeclasses.mark_unresolvable evi, p evd ev evi)
+      else evi, false
     else fun _ evd ev evi -> 
-      try let oevi = Evd.find oevd ev in
-	    if Typeclasses.is_resolvable oevi then
-	      Typeclasses.mark_unresolvable evi, p evd ev evi
-	    else evi, false
-      with Not_found ->
-	Typeclasses.mark_unresolvable evi, p evd ev evi
+      if evi.evar_body = Evar_empty then
+	try let oevi = Evd.find oevd ev in
+	      if Typeclasses.is_resolvable oevi then
+		Typeclasses.mark_unresolvable evi, p evd ev evi
+	      else evi, false
+	with Not_found ->
+	  Typeclasses.mark_unresolvable evi, p evd ev evi
+      else evi, false
   in
   let rec aux p evd =
     let evd' = resolve_all_evars_once debug m p evd in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 1ba25fc609..15ef2db2dc 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -334,7 +334,7 @@ let unify_eqn env sigma hypinfo t =
     let env', prf, c1, c2, car, rel =
       match abs with
       | Some (absprf, absprfty) ->
-	  let env' = clenv_unify allowK ~flags:rewrite2_unif_flags CONV left t cl in
+	  let env' = clenv_unify allowK ~flags:rewrite_unif_flags CONV left t cl in
 	    env', prf, c1, c2, car, rel
       | None ->
 	  let env' =
@@ -1370,7 +1370,9 @@ let unification_rewrite l2r c1 c2 cl car rel but gl =
       clenv_pose_metas_as_evars cl' mvs
   in
   let nf c = Evarutil.nf_evar ( cl'.evd) (Clenv.clenv_nf_meta cl' c) in
-  let c1 = nf c1 and c2 = nf c2 and car = nf car and rel = nf rel in
+  let c1 = if l2r then nf c' else nf c1
+  and c2 = if l2r then nf c2 else nf c'
+  and car = nf car and rel = nf rel in
   check_evar_map_of_evars_defs cl'.evd;
   let prf = nf (Clenv.clenv_value cl') and prfty = nf (Clenv.clenv_type cl') in
   let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in