diff options
Diffstat (limited to 'test-suite/bugs/closed/bug_3682.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_3682.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_3682.v b/test-suite/bugs/closed/bug_3682.v index 9d37d1a2d0..07b759afb5 100644 --- a/test-suite/bugs/closed/bug_3682.v +++ b/test-suite/bugs/closed/bug_3682.v @@ -1,6 +1,6 @@ Require Import TestSuite.admit. Class Foo. Definition bar `{Foo} (x : Set) := Set. -Instance: Foo. +Instance: Foo := {}. Definition bar1 := bar nat. Definition bar2 := bar ltac:(admit). |