1 files changed, 45 insertions, 10 deletions

diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 033b3f48..653b5bf9 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -18,10 +18,10 @@ Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t.
 
 Lemma setoid_set : Setoid_Theory set same.
 
-unfold same in |- *; split ; red.
-red in |- *; auto.
+unfold same; split ; red.
+red; auto.
 
-red in |- *.
+red.
 intros.
 elim (H a); auto.
 
@@ -33,19 +33,19 @@ Qed.
 Add Setoid set same setoid_set as setsetoid.
 
 Add Morphism In : In_ext.
-unfold same in |- *; intros a s t H; elim (H a); auto.
+unfold same; intros a s t H; elim (H a); auto.
 Qed.
 
 Lemma add_aux :
  forall s t : set,
  same s t -> forall a b : A, In a (Add b s) -> In a (Add b t).
-unfold same in |- *; simple induction 2; intros.
+unfold same; simple induction 2; intros.
 rewrite H1.
-simpl in |- *; left; reflexivity.
+simpl; left; reflexivity.
 
 elim (H a).
 intros.
-simpl in |- *; right.
+simpl; right.
 apply (H2 H1).
 Qed.
 
@@ -74,15 +74,15 @@ setoid_replace (remove a (Add a Empty)) with Empty.
 
 auto.
 
-unfold same in |- *.
+unfold same.
 split.
-simpl in |- *.
+simpl.
 case (eq_dec a a).
 intros e ff; elim ff.
 
 intros; absurd (a = a); trivial.
 
-simpl in |- *.
+simpl.
 intro H; elim H.
 Qed.
 
@@ -130,3 +130,38 @@ 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 (fun 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 
+   does not fix the instance at the first unification, use [at], or simply rewrite for 
+   this semantics. *)
+
+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 = y). Abort.
+
+Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
+Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort.
+