aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_2304.v
blob: 663c42e48073a2b8e31ef4315d2b3ddfc8e12348 (plain)
1
2
3
(* This used to fail with an anomaly NotASort at some time *)
Class A (O: Type): Type := a: O -> Type.
Fail Goal forall (x: a tt), @a x = @a x.