blob: f54d6433d8d068ee35daf696a66f2187258c02ac (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
Require Coq.Classes.RelationClasses.
Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
{ refl : forall x, r x x }.
(* FAILURE 1 *)
Section foo.
Polymorphic Universes A.
Polymorphic Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
Fail Definition foo := PO.
End foo.
Module ILogic.
Set Universe Polymorphism.
(* Logical connectives *)
Class ILogic@{L} (A : Type@{L}) : Type := mkILogic
{
lentails: A -> A -> Prop;
lentailsPre:> RelationClasses.PreOrder lentails
}.
End ILogic.
Set Printing Universes.
(* There is stil a problem if the class is universe polymorphic *)
Section Embed_ILogic_Pre.
Polymorphic Universes A T.
Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}.
End Embed_ILogic_Pre.
|
