From 929cba74dc2ba2d1b232b61fb3539babad9e7c76 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 27 Sep 2014 21:07:28 +0200
Subject: Fix test-suite file.

---
 test-suite/bugs/closed/3662.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v
index 753fb33ca2..bd53389b4f 100644
--- a/test-suite/bugs/closed/3662.v
+++ b/test-suite/bugs/closed/3662.v
@@ -39,9 +39,8 @@ Defined.
 Lemma eta A B : forall x : prod A B, x = pair (fst x) (snd x). reflexivity. Qed.
 
 Goal forall x : prod nat nat, fst x = 0.
-  intros. unfold fst. rewrite (eta x). cbv iota. cbv delta. cbv iota.
-  cbv delta. 
-  match goal with
+  intros. unfold fst.
+  Fail match goal with
     | [ |- fst ?x = 0 ] => idtac
   end.
 Abort.
-- 
cgit v1.2.3