| _,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 || s2 = C.Type -> true
+ | (C.Sort s1, C.Sort s2) when
+ s1 = s2 || (not test_equality_only) && s2 = C.Type
+ -> true
| (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
| _,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 || s2 = C.Type -> true
+ | (C.Sort s1, C.Sort s2) when
+ s1 = s2 || (not test_equality_only) && s2 = C.Type
+ -> true
| (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