diff options
| -rw-r--r-- | test-suite/bugs/closed/3682.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/3682.v b/test-suite/bugs/closed/3682.v index 71baf78cf2..b8c5b4d524 100644 --- a/test-suite/bugs/closed/3682.v +++ b/test-suite/bugs/closed/3682.v @@ -2,4 +2,4 @@ Class Foo. Definition bar `{Foo} (x : Set) := Set. Instance: Foo. Definition bar1 := bar nat. -Fail Definition bar2 := bar $(admit)$. +Definition bar2 := bar $(admit)$. |