diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-21 13:43:31 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-03-01 12:05:39 +0100 |
| commit | 711b9d8cdf6e25690d247d9e8c49f005527e64e2 (patch) | |
| tree | 5a19ec52e7a510a456195d3814958abc33e47f73 /test-suite/success | |
| parent | f726e860917b56abc94f21d9d5add7594d23bb6d (diff) | |
Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".
Noticed by Sigurd Schneider.
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/rewrite.v | 17 |
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. |