with
Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2)
| Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.CProp u2)
- | Cic.Sort (Cic.Type u1), Cic.Sort (Cic.CProp u2) ->
- CicUniv.add_ge u2 u1 ugraph
+ | Cic.Sort (Cic.Type u1), Cic.Sort (Cic.CProp u2)
| Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.Type u2) ->
- CicUniv.add_gt u2 u1 ugraph
+ CicUniv.add_ge u2 u1 ugraph
| Cic.Sort _, Cic.Sort Cic.Prop
| Cic.Sort _, Cic.Sort Cic.CProp _
| Cic.Sort _, Cic.Sort Cic.Set
| (C.Sort s1, C.Sort (C.Prop | C.Set)) ->
(* different from Coq manual!!! *)
t2',ugraph
- | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+ | (C.Sort (C.Type t1 | C.CProp t1), C.Sort (C.Type t2)) ->
let t' = CicUniv.fresh() in
(try
let ugraph1 = CicUniv.add_ge t' t1 ugraph in
C.Sort (C.Type t'),ugraph2
with
CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
- | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
+ | (C.Sort (C.CProp t1 | C.Type t1), C.Sort (C.CProp t2)) ->
let t' = CicUniv.fresh() in
(try
let ugraph1 = CicUniv.add_ge t' t1 ugraph in
C.Sort (C.CProp t'),ugraph2
with
CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
- | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_ge t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.CProp t'),ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
- | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) ->
- let t' = CicUniv.fresh() in
- (try
- let ugraph1 = CicUniv.add_gt t' t1 ugraph in
- let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
- C.Sort (C.Type t'),ugraph2
- with
- CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
| (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),ugraph
| (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1),ugraph
| (C.Meta _, C.Sort _) -> t2',ugraph