From ee2adce57aac1ffe21681a9d31a8e8bc4f94210b Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 23 Jun 2014 17:38:56 +0200
Subject: Fix test-suite script for subst working with let-ins, the following
 proof was rightly failing.

---
 test-suite/success/rewrite.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 0e1e778635..f7b9897c1a 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.
-- 
cgit v1.2.3