- (C.Sort _, C.Sort s2)
- when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
- (* different from Coq manual!!! *)
- C.Sort s2
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
- C.Sort (C.Type (CicUniv.fresh()))
- | (C.Sort _,C.Sort (C.Type t1)) ->
- (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
- C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
+ | (C.Sort _, C.Sort s2) when (s2 = C.Prop || s2 = C.Set) -> C.Sort s2
+ | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->C.Sort(C.Type(CicUniv.fresh()))
+ | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1)
+ | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1)