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

1 files changed, 29 insertions, 16 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