let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
match (t1', t2') with
(C.Sort s1, C.Sort s2)
- when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
+ when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
C.Sort s2
| (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
| (_,_) ->