| (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
let t' = CicUniv.fresh() in
(try
- let ugraph1 = CicUniv.add_gt t' t1 ugraph in
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
C.Sort (C.Type t'),subst,metasenv,ugraph2
with