aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/univ_include.v
blob: 28a3263d327597c96b1863bc811a7cbd02f1baf2 (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
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. *)