let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
match t1, t2 with
| C.Sort s1, C.Sort C.Prop -> t2
- | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (max u1 u2))
+ | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (u1@u2))
| C.Sort _,C.Sort (C.Type _) -> t2
| C.Sort (C.Type _) , C.Sort C.CProp -> t1
| C.Sort _, C.Sort C.CProp