diff options
Diffstat (limited to 'checker/term.ml')
| -rw-r--r-- | checker/term.ml | 22 |
1 files changed, 9 insertions, 13 deletions
diff --git a/checker/term.ml b/checker/term.ml index 0236f786..d84491b3 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -20,15 +20,15 @@ open Cic (* Sorts. *) let family_of_sort = function - | Prop Null -> InProp - | Prop Pos -> InSet + | Prop -> InProp + | Set -> InSet | Type _ -> InType let family_equal = (==) let sort_of_univ u = - if Univ.is_type0m_univ u then Prop Null - else if Univ.is_type0_univ u then Prop Pos + if Univ.is_type0m_univ u then Prop + else if Univ.is_type0_univ u then Set else Type u (********************************************************************) @@ -243,7 +243,7 @@ let map_rel_decl f = function LocalDef (n, body', typ') let map_rel_context f = - List.smartmap (map_rel_decl f) + List.Smart.map (map_rel_decl f) let extended_rel_list n hyps = let rec reln l p = function @@ -356,15 +356,11 @@ let rec isArity c = (* alpha conversion : ignore print names and casts *) let compare_sorts s1 s2 = match s1, s2 with -| Prop c1, Prop c2 -> - begin match c1, c2 with - | Pos, Pos | Null, Null -> true - | Pos, Null -> false - | Null, Pos -> false - end +| Prop, Prop | Set, Set -> true | Type u1, Type u2 -> Univ.Universe.equal u1 u2 -| Prop _, Type _ -> false -| Type _, Prop _ -> false +| Prop, Set | Set, Prop -> false +| (Prop | Set), Type _ -> false +| Type _, (Prop | Set) -> false let eq_puniverses f (c1,u1) (c2,u2) = Univ.Instance.equal u1 u2 && f c1 c2 |