diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 17:38:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-06-23 18:31:17 +0200 |
| commit | ee2adce57aac1ffe21681a9d31a8e8bc4f94210b (patch) | |
| tree | dc429d5a72b20bab0a4333b9592e12dcf40da6cf | |
| parent | 54b1866084938d46e510146a46bad8a712da27b7 (diff) | |
Fix test-suite script for subst working with let-ins, the following proof was rightly failing.
| -rw-r--r-- | test-suite/success/rewrite.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 0e1e77863..f7b9897c1 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -135,6 +135,7 @@ Abort. Goal forall x y, x=y+0 -> let z := x+1 in x+1=y -> z=z -> z=x. intros. subst x. (* was failing *) +subst z. rewrite H0. -reflexivity. +auto with arith. Qed. |