2 files changed, 39 insertions, 1 deletions
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 62249666b..448d0082d 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -151,10 +151,25 @@ Abort.
 
 (* Check that rewriting within evars still work (was broken in 8.5beta1) *)
 
-
 Goal forall (a: unit) (H: a = tt), exists x y:nat, x = y.
 intros; eexists; eexists.
 rewrite H.
 Undo.
 subst.
 Abort.
+
+(* Check that iterated rewriting does not rewrite in the side conditions *)
+(* Example from Sigurd Schneider, extracted from contrib containers *)
+
+Lemma EQ
+  : forall (e e' : nat), True -> e = e'.
+Admitted.
+
+Lemma test (v1 v2 v3: nat) (v' : v1 = v2) : v2 = v1.
+Proof.
+  rewrite <- (EQ v1 v2) in *.
+  exact v'.
+  (* There should be only two side conditions *)
+  exact I.
+  exact I.
+Qed.
diff --git a/test-suite/success/vm_evars.v b/test-suite/success/vm_evars.v
new file mode 100644
index 000000000..2c8b099ef
--- /dev/null
+++ b/test-suite/success/vm_evars.v
@@ -0,0 +1,23 @@
+Fixpoint iter {A} (n : nat) (f : A -> A) (x : A) :=
+match n with
+| 0 => x
+| S n => iter n f (f x)
+end.
+
+Goal nat -> True.
+Proof.
+intros n.
+evar (f : nat -> nat).
+cut (iter 10 f 0 = 0).
+vm_compute.
+intros; constructor.
+instantiate (f := (fun x => x)).
+reflexivity.
+Qed.
+
+Goal exists x, x = 5 + 5.
+Proof.
+  eexists.
+  vm_compute.
+  reflexivity.
+Qed.