From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 checker/term.ml | 22 +++++++++-------------
 1 file changed, 9 insertions(+), 13 deletions(-)

(limited to 'checker/term.ml')

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
-- 
cgit v1.2.3