From 03e21974a3e971a294533bffb81877dc1bd270b6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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/vm.mli | 18 +++++++++++++-----
 1 file changed, 13 insertions(+), 5 deletions(-)

(limited to 'kernel/vm.mli')

diff --git a/kernel/vm.mli b/kernel/vm.mli
index ea38ee43f..bc38452d4 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -1,5 +1,13 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
 open Names
-open Term
+open Constr
 open Cbytecodes
 
 (** Debug printing *)
@@ -23,7 +31,7 @@ type arguments
 type atom =
   | Aid of Vars.id_key
   | Aind of inductive
-  | Atype of Univ.universe
+  | Atype of Univ.Universe.t
 
 (** Zippers *)
 
@@ -38,7 +46,7 @@ type stack = zipper list
 type to_up
 
 type whd =
-  | Vsort of sorts
+  | Vsort of Sorts.t
   | Vprod of vprod
   | Vfun of vfun
   | Vfix of vfix * arguments option
@@ -46,7 +54,7 @@ type whd =
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vatom_stk of atom * stack
-  | Vuniv_level of Univ.universe_level
+  | Vuniv_level of Univ.Level.t
 
 (** For debugging purposes only *)
 
@@ -66,7 +74,7 @@ external val_of_annot_switch : annot_switch -> values = "%identity"
 (** Destructors *)
 
 val whd_val : values -> whd
-val uni_lvl_val : values -> Univ.universe_level
+val uni_lvl_val : values -> Univ.Level.t
 
 (** Arguments *)
 
-- 
cgit v1.2.3