blob: 5ba0787ee7c2184309e7d0690661cb7f9e3d878e (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Require Coq.Classes.RelationClasses.
Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
{ refl : forall x, r x x }.
Section foo.
Polymorphic Universes A.
Section bar.
Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
End bar.
End foo.
|
