diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-27 13:28:44 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-27 13:28:44 +0200 |
commit | 04e0f9fde8789a28b66f24000ac8c831ff0815af (patch) | |
tree | b9e3d026e192e7b5b0409594b11fb95ed138b6cb /checker/term.ml | |
parent | d9e6bed640083fce067343f24183382cc8e6ca7b (diff) | |
parent | 8d89102e84d41956fb1359089d573cc64d7838ca (diff) |
Merge PR #7863: Remove Sorts.contents
Diffstat (limited to 'checker/term.ml')
-rw-r--r-- | checker/term.ml | 20 |
1 files changed, 8 insertions, 12 deletions
diff --git a/checker/term.ml b/checker/term.ml index 509634bdb..d84491b38 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 (********************************************************************) @@ -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 |