aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:27:54 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-04 16:27:54 +0100
commited05111e048e864c63c2e21b8ebac675a80dc464 (patch)
tree47e7bb219ba43e901b2bfc3791e80f161246dd54 /test-suite
parent5003953d45ea0e780cd50bb9d6521799adf18079 (diff)
parent711b9d8cdf6e25690d247d9e8c49f005527e64e2 (diff)
Merge PR #915: Fix rewrite in * side conditions
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/success/rewrite.v17
1 files changed, 16 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.