| _,None -> true
| Some t1',Some t2' -> aux test_equality_only context t1' t2'
) true l1 l2
- | (C.Sort s1, C.Sort s2) when
- s1 = s2 || (not test_equality_only) && s2 = C.Type
- -> true
+ (* 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)) ->
aux true context s1 s2 &&
aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2