aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_3682.v
blob: 07b759afb5676d0bda81263ef54a6cd21af13874 (plain)
1
2
3
4
5
6
Require Import TestSuite.admit.
Class Foo.
Definition bar `{Foo} (x : Set) := Set.
Instance: Foo := {}.
Definition bar1 := bar nat.
Definition bar2 := bar ltac:(admit).