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

5 files changed, 37 insertions, 22 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
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v
index 7d795cf50e..5d6ed9abed 100644
--- a/theories/Numbers/Cyclic/Int31/Cyclic31.v
+++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v
@@ -2029,7 +2029,7 @@ Section Int31_Spec.
         (1 * 2 + (([|j|] - 2) + [|i|] / [|j|])); try ring.
  rewrite Z_div_plus_full_l; auto with zarith.
  assert (0 <= [|i|]/ [|j|]) by (apply Z_div_pos; auto with zarith).
- assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / [|2|]) ; auto with zarith.
+ assert (0 <= ([|j|] - 2 + [|i|] / [|j|]) / 2) ; auto with zarith.
  rewrite <- Hj1, Zdiv_1_r.
  replace (1 + [|i|])%Z with (1 * 2 + ([|i|] - 1))%Z; try ring.
  rewrite Z_div_plus_full_l; auto with zarith.
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index efe76d9166..046dd2dfdd 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -1193,7 +1193,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite strong_spec_red.
  symmetry; apply (Qred_complete (x+(-y)%Qc)%Q).
  rewrite spec_sub_norm, ! strong_spec_of_Qc.
- unfold Qcopp, Q2Qc; rewrite Qred_correct; auto with qarith.
+ unfold Qcopp, Q2Qc, this. rewrite Qred_correct ; auto with qarith.
  Qed.
 
  Theorem spec_mulc x y:
@@ -1294,7 +1294,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType.
  rewrite strong_spec_red.
  symmetry; apply (Qred_complete (x*(/y)%Qc)%Q).
  rewrite spec_div_norm, ! strong_spec_of_Qc.
- unfold Qcinv, Q2Qc; rewrite Qred_correct; auto with qarith.
+ unfold Qcinv, Q2Qc, this; rewrite Qred_correct; auto with qarith.
  Qed.
 
  Theorem spec_squarec x: [[square x]] =  [[x]]^2.
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v
index 57bc050a90..a4feed8f3e 100644
--- a/theories/Reals/Rpower.v
+++ b/theories/Reals/Rpower.v
@@ -470,7 +470,7 @@ Proof.
   apply Rmult_eq_reg_l with (INR 2).
   apply exp_inv.
   fold Rpower in |- *.
-  cut ((x ^R (/ 2)) ^R INR 2 = sqrt x ^R INR 2).
+  cut ((x ^R (/ INR 2)) ^R INR 2 = sqrt x ^R INR 2).
   unfold Rpower in |- *; auto.
   rewrite Rpower_mult.
   rewrite Rinv_l.