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

---
 kernel/cbytecodes.mli | 40 ++--------------------------------------
 1 file changed, 2 insertions(+), 38 deletions(-)

(limited to 'kernel/cbytecodes.mli')

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index f87090c7..9c04c166 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -11,42 +11,7 @@
 (* $Id$ *)
 
 open Names
-open Constr
-
-type tag = int
-
-val accu_tag : tag
-
-val type_atom_tag : tag
-val max_atom_tag : tag
-val proj_tag : tag
-val fix_app_tag : tag
-val switch_tag : tag
-val cofix_tag : tag
-val cofix_evaluated_tag : tag
-
-val last_variant_tag : tag
-
-type structured_constant =
-  | Const_sort 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.Level.t
-
-val pp_struct_const : structured_constant -> Pp.t
-
-type reloc_table = (tag * int) array
-
-type annot_switch =
-   {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int}
-
-val eq_structured_constant : structured_constant -> structured_constant -> bool
-val hash_structured_constant : structured_constant -> int
-
-val eq_annot_switch : annot_switch -> annot_switch -> bool
-val hash_annot_switch : annot_switch -> int
+open Vmvalues
 
 module Label :
   sig
@@ -89,8 +54,7 @@ type instruction =
   | Ksetfield of int                    (** accu[n] = sp[0] ; sp = pop sp *)
   | Kstop
   | Ksequence of bytecodes * bytecodes
-  | Kproj of int * Constant.t  (** index of the projected argument,
-                                            name of projection *)
+  | Kproj of Projection.Repr.t
   | Kensurestackcapacity of int
 
 (** spiwack: instructions concerning integers *)
-- 
cgit v1.2.3