summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/6878.v
blob: 70f1b3127af9ef9ac4e37ff4f20dbeac51c352fe (plain)
1
2
3
4
5
6
7
8

Set Universe Polymorphism.
Module Type T.
  Axiom foo : Prop.
End T.

(** Used to anomaly *)
Fail Module M : T with Definition foo := Type.