diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 13:39:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 13:39:27 +0100 |
| commit | f9c2d5d26a6a8e15549ada1f69d630acfa1a9437 (patch) | |
| tree | 16c64d31a3fea1c3fdbcb54996fb2c7e3a7c831e /test-suite/bugs/closed/4018.v | |
| parent | 5830f5867f36ebf66bc1f4126762f4b1c1444f94 (diff) | |
Fixing test-suite.
Diffstat (limited to 'test-suite/bugs/closed/4018.v')
| -rw-r--r-- | test-suite/bugs/closed/4018.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4018.v b/test-suite/bugs/closed/4018.v index c3a045943..8895e09e0 100644 --- a/test-suite/bugs/closed/4018.v +++ b/test-suite/bugs/closed/4018.v @@ -1,3 +1,3 @@ (* Catching PatternMatchingFailure was lost at some point *) Goal nat -> True. -intros [=]. +Fail intros [=]. |