diff options
Diffstat (limited to 'test-suite/bugs/closed/3682.v')
| -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 2a282d22..9d37d1a2 100644 --- a/test-suite/bugs/closed/3682.v +++ b/test-suite/bugs/closed/3682.v @@ -3,4 +3,4 @@ Class Foo. Definition bar `{Foo} (x : Set) := Set. Instance: Foo. Definition bar1 := bar nat. -Definition bar2 := bar $(admit)$. +Definition bar2 := bar ltac:(admit). |