diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 21:07:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 21:07:28 +0200 |
| commit | 929cba74dc2ba2d1b232b61fb3539babad9e7c76 (patch) | |
| tree | f475850613f93ce5d76c13355f725d3c9d4dd08b | |
| parent | 92a183f4ada641c0ab73dd0479e98df36eeeb365 (diff) | |
Fix test-suite file.
| -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. |