+ | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.CProp t'),subst,metasenv,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+ | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+ let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+ C.Sort (C.CProp t'),subst,metasenv,ugraph2
+ with
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
+ | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
+ let t' = CicUniv.fresh() in
+ (try
+ 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
+ CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))