From 711b9d8cdf6e25690d247d9e8c49f005527e64e2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 21 Jul 2017 13:43:31 +0200 Subject: Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". Noticed by Sigurd Schneider. --- test-suite/success/rewrite.v | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) (limited to 'test-suite/success') 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. -- cgit v1.2.3