diff options
| -rw-r--r-- | test-suite/bugs/closed/3662.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v index 753fb33ca..bd53389b4 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. |