diff options
| author | Pierre-Marie Pédrot | 2015-02-15 13:39:27 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-15 13:39:27 +0100 |
| commit | f9c2d5d26a6a8e15549ada1f69d630acfa1a9437 (patch) | |
| tree | 16c64d31a3fea1c3fdbcb54996fb2c7e3a7c831e | |
| parent | 5830f5867f36ebf66bc1f4126762f4b1c1444f94 (diff) | |
Fixing test-suite.
| -rw-r--r-- | test-suite/bugs/closed/4017.v | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4018.v | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4017.v b/test-suite/bugs/closed/4017.v index a6f177b496..aa810f4f0e 100644 --- a/test-suite/bugs/closed/4017.v +++ b/test-suite/bugs/closed/4017.v @@ -1,3 +1,5 @@ +Set Implicit Arguments. + (* Use of implicit arguments was lost in multiple variable declarations *) Variables (A1 : Type) diff --git a/test-suite/bugs/closed/4018.v b/test-suite/bugs/closed/4018.v index c3a045943c..8895e09e02 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 [=]. |