aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/HoTT_coq_074.v
blob: 370c7d404eb232e7ee6a65d44b7d9d147f4fd747 (plain)
1
2
3
4
5
6
7
8
9
10
Monomorphic Definition U1 := Type.
Monomorphic Definition U2 := Type.

Set Printing Universes.
Definition foo : True.
let t1 := type of U1 in
let t2 := type of U2 in
idtac t1 t2;
pose (t1 : t2). exact I. 
Defined.