Correct handling of existential variables when multiple different

instances of the lemma are rewritten at once. Cleanup dead code and put
the problematic cases in the test-suite. Also fix some test-suite
scripts.


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

4 files changed, 46 insertions, 40 deletions

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index ecc8631bff..8b277e6c2c 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -298,7 +298,7 @@ let refresh_hypinfo env sigma hypinfo =
       match c with
 	| Some c ->
 	    (* Refresh the clausenv to not get the same meta twice in the goal. *)
-	    decompose_applied_relation env cl.evd c l2r;
+	    decompose_applied_relation env sigma c l2r;
 	| _ -> hypinfo
   else hypinfo
 
@@ -307,6 +307,7 @@ let unify_eqn env sigma hypinfo t =
   else try
     let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
     let left = if l2r then c1 else c2 in
+    let cl = { cl with evd = evars_reset_evd sigma cl.evd } in
     let env', prf, c1, c2, car, rel =
       match abs with
       | Some (absprf, absprfty) ->
@@ -332,7 +333,7 @@ let unify_eqn env sigma hypinfo t =
 	  in
 	    if convertible env env'.evd ty1 ty2 then (
 	      if occur_meta prf then
-		hypinfo := refresh_hypinfo env sigma !hypinfo;
+		hypinfo := refresh_hypinfo env env'.evd !hypinfo;
 	      env', prf, c1, c2, car, rel)
 	    else raise Reduction.NotConvertible
     in
@@ -546,10 +547,9 @@ let apply_rule hypinfo loccs : strategy =
 	| _ -> None
 
 let apply_lemma (evm,c) left2right loccs : strategy =
-  fun env sigma ->
-    let evars = Evd.merge sigma evm in
-    let hypinfo = ref (decompose_applied_relation env evars c left2right) in
-      apply_rule hypinfo loccs env sigma
+  fun env sigma t ty cstr evars ->
+    let hypinfo = ref (decompose_applied_relation env (goalevars evars) c left2right) in
+      apply_rule hypinfo loccs env sigma t ty cstr evars
 
 let make_leibniz_proof c ty r =
   let prf = 
@@ -902,10 +902,10 @@ let rewrite_strat flags occs hyp =
   in aux ()
 
 let rewrite_with {it = c; sigma = evm} left2right loccs : strategy =
-  fun env sigma ->
-    let evars = Evd.merge sigma evm in
-    let hypinfo = ref (decompose_applied_relation env evars c left2right) in
-      rewrite_strat default_flags loccs hypinfo env sigma
+  fun env sigma t ty cstr evars ->
+    let gevars = Evd.merge evm (goalevars evars) in
+    let hypinfo = ref (decompose_applied_relation env gevars c left2right) in
+      rewrite_strat default_flags loccs hypinfo env sigma t ty cstr (gevars, cstrevars evars)
 
 let apply_strategy (s : strategy) env sigma concl cstr evars =
   let res =
@@ -918,30 +918,6 @@ let apply_strategy (s : strategy) env sigma concl cstr evars =
     | Some (Some res) ->
 	Some (Some (res.rew_prf, res.rew_evars, res.rew_car, res.rew_from, res.rew_to))
 
-let split_evars_once sigma evd =
-  Evd.fold_undefined (fun ev evi deps ->
-    if Intset.mem ev deps then
-      Intset.union (Evarutil.undefined_evars_of_evar_info evd evi) deps
-    else deps) evd sigma
-
-let existentials_of_evd evd =
-  Evd.fold_undefined (fun ev _ acc -> Intset.add ev acc) evd Intset.empty
-
-let evd_of_existentials evd exs =
-  Intset.fold
-    (fun ev acc ->
-      try Evd.add acc ev (Evd.find_undefined evd ev)
-      with Not_found -> acc)
-    exs Evd.empty
-
-let split_evars sigma evd =
-  let rec aux deps =
-    let deps' = split_evars_once deps evd in
-      if Intset.equal deps' deps then
-	evd_of_existentials evd deps
-      else aux deps'
-  in aux (existentials_of_evd sigma)
-
 let merge_evars (goal,cstr) = Evd.merge goal cstr
 let solve_constraints env evars =
   Typeclasses.resolve_typeclasses env ~split:false ~fail:true
diff --git a/test-suite/bugs/closed/shouldsucceed/2393.v b/test-suite/bugs/closed/shouldsucceed/2393.v
index 6a559e75c3..fb4f92619f 100644
--- a/test-suite/bugs/closed/shouldsucceed/2393.v
+++ b/test-suite/bugs/closed/shouldsucceed/2393.v
@@ -11,6 +11,3 @@ Program Fixpoint idType (t : T) (n := sizeOf t) (b : vect n) {measure n} : T
     := match t with
        | MkT => MkT
        end.
-
-Require Import Wf_nat.
-Solve Obligations using auto with arith.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index f446cd2dfa..b286538316 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -120,6 +120,3 @@ Check C2 eq_refl.
 
 Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
  | C3 : I3 a (n:=0).
-
-Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
- | C2 {p} : I2 a (n:=p).
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 033b3f485f..d5096ea657 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -130,3 +130,39 @@ intros f0 Q H.
 setoid_rewrite H.
 tauto.
 Qed.
+
+(** Check proper refreshing of the lemma application for multiple 
+   different instances in a single setoid rewrite. *)
+
+Section mult.
+  Context (fold : forall {A} {B}, (A -> B) -> A -> B).
+  Context (add : forall A, A -> A).
+  Context (fold_lemma : forall {A B f} {eqA : relation B} x, eqA (fold A B f (add A x)) (fold _ _ f x)).
+  Context (ab : forall B, A -> B).
+  Context (anat : forall A, nat -> A).
+
+Goal forall x, (fold _ _ (fun x => ab A x) (add A x) = anat _ (fold _ _ (ab nat) (add _ x))). 
+Proof. intros.
+  setoid_rewrite fold_lemma. 
+  change (fold A A (λ x0 : A, ab A x0) x = anat A (fold A nat (ab nat) x)).
+Abort.
+
+End mult.
+
+(** Current semantics for rewriting with typeclass constraints in the lemma
+   fixes the instance at the first unification. Using @ to make them metavariables 
+   allow different instances to be used. [at] can be used to select the instance
+   too. *)
+
+Require Import Arith.
+
+Class Foo (A : Type) := {foo_neg : A -> A ; foo_prf : forall x : A, x = foo_neg x}.
+Instance: Foo nat. admit. Defined.
+Instance: Foo bool. admit. Defined.
+
+Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
+Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = foo_neg y). Abort.
+
+Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
+Proof. intros. setoid_rewrite <- @foo_prf. change (beq_nat x 0 = y). Abort.
+