blob: ef79b9869b052aebd45cd0abdb432b89bcb22759 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Section foo.
Polymorphic Universes A B.
Constraint A <= B.
End foo.
(* gives an anomaly Universe undefined *)
or even, a refinement of #4503:
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.
Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
End bar.
End foo.
|
