diff options
| -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 [=]. |