From af0a04b8e16c2554e0c747da6d625799b332f5fe Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 11 Oct 2017 19:41:23 +0200
Subject: Remove Sorts.contents

---
 vernac/comInductive.ml | 8 ++++----
 vernac/record.ml       | 3 +--
 2 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'vernac')

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 6057c05f5..0387b32ba 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -126,7 +126,7 @@ let make_conclusion_flexible sigma ty poly =
   else sigma
 
 let is_impredicative env u =
-  u = Prop Null || (is_impredicative_set env && u = Prop Pos)
+  u = Prop || (is_impredicative_set env && u = Set)
 
 let interp_ind_arity env sigma ind =
   let c = intern_gen IsType env sigma ind.ind_arity in
@@ -245,7 +245,7 @@ let solve_constraints_system levels level_bounds =
 let inductive_levels env evd poly arities inds =
   let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
   let levels = List.map (fun (x,(ctx,a)) ->
-    if a = Prop Null then None
+    if a = Prop then None
     else Some (univ_of_sort a)) destarities
   in
   let cstrs_levels, min_levels, sizes =
@@ -298,14 +298,14 @@ let inductive_levels env evd poly arities inds =
            (** "Polymorphic" type constraint and more than one constructor,
                should not land in Prop. Add constraint only if it would
                land in Prop directly (no informative arguments as well). *)
-            Evd.set_leq_sort env evd (Prop Pos) du
+            Evd.set_leq_sort env evd Set du
           else evd
         in
         let duu = Sorts.univ_of_sort du in
         let evd =
           if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
             if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
-              Evd.set_eq_sort env evd (Prop Null) du
+              Evd.set_eq_sort env evd Prop du
             else evd
           else Evd.set_eq_sort env evd (Type cu) du
         in
diff --git a/vernac/record.ml b/vernac/record.ml
index 202c9b92f..2d7800827 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -164,8 +164,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs =
            Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
 	   (* We can assume that the level in aritysort is not constrained
 	       and clear it, if it is flexible *)
-          Evd.set_eq_sort env_ar sigma (Prop Pos) sort,
-          EConstr.mkSort (Sorts.sort_of_univ univ)
+   Evd.set_eq_sort env_ar sigma Set sort, EConstr.mkSort (Sorts.sort_of_univ univ)
         else sigma, typ
   in
   let sigma = Evd.minimize_universes sigma in
-- 
cgit v1.2.3