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.
---
 kernel/cbytecodes.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'kernel/cbytecodes.ml')

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 63b0e69295..9febc6449b 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -13,7 +13,7 @@
 (* This file defines the type of bytecode instructions *)
 
 open Names
-open Term
+open Constr
 
 type tag = int
 
@@ -32,13 +32,13 @@ let cofix_evaluated_tag = 7
 let last_variant_tag = 245 
 
 type structured_constant =
-  | Const_sorts of sorts
+  | Const_sorts of Sorts.t
   | Const_ind of inductive
   | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
-  | Const_univ_level of Univ.universe_level
-  | Const_type of Univ.universe
+  | Const_univ_level of Univ.Level.t
+  | Const_type of Univ.Universe.t
 
 type reloc_table = (tag * int) array
 
@@ -186,7 +186,8 @@ open Pp
 open Util
 
 let pp_sort s =
-  match family_of_sort s with
+  let open Sorts in
+  match family s with
   | InSet -> str "Set"
   | InProp -> str "Prop"
   | InType -> str "Type"
-- 
cgit v1.2.3