From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 6 Nov 2017 23:27:09 +0100
Subject: [api] Move structures deprecated in the API to the core.

We do up to `Term` which is the main bulk of the changes.
---
 pretyping/typing.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping/typing.ml')

diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 1f35fa19aa..43066c8099 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -160,7 +160,7 @@ let check_type_fixpoint ?loc env evdref lna lar vdefj =
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
   let pj = Retyping.get_judgment_of env sigma p in
-  let ksort = family_of_sort (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in
+  let ksort = Sorts.family (ESorts.kind sigma (sort_of_arity env sigma pj.uj_type)) in
   let specif = Global.lookup_inductive (fst ind) in
   let sorts = elim_sorts specif in
   if not (List.exists ((==) ksort) sorts) then
@@ -195,11 +195,11 @@ let check_cofix env sigma pcofix =
 
 let judge_of_prop =
   { uj_val = EConstr.mkProp;
-    uj_type = EConstr.mkSort type1_sort }
+    uj_type = EConstr.mkSort Sorts.type1 }
 
 let judge_of_set =
   { uj_val = EConstr.mkSet;
-    uj_type = EConstr.mkSort type1_sort }
+    uj_type = EConstr.mkSort Sorts.type1 }
 
 let judge_of_prop_contents = function
   | Null -> judge_of_prop
-- 
cgit v1.2.3