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

3 files changed, 36 insertions, 6 deletions

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