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
|
Definition T := Type.
Definition U := Type.
Module Type MT.
Parameter t : T.
End MT.
Module Type MU.
Parameter t : U.
End MU.
Module F (E : MT).
Definition elt :T := E.t.
End F.
Module G (E : MU).
Include F E.
Print Universes. (* U <= T *)
End G.
Print Universes. (* Check if constraint is lost *)
Module Mt.
Definition t := T.
End Mt.
Fail Module P := G Mt. (* should yield Universe inconsistency *)
(* ... otherwise the following command will show that T has type T! *)
(* Eval cbv delta [P.elt Mt.t] in P.elt. *)
|
