- | (C.Sort s1, C.Sort s2) when s1 = s2 || s2 = C.Type -> true
- | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+ CicUniv.add_eq t2 t1
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ CicUniv.add_ge t2 t1
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort s1, C.Sort (C.Type _)) -> not test_equality_only
+ (* TASSI: CONSTRAINTS *)
+ | (C.Sort s1, C.Sort s2) -> s1 = s2
+ | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->