From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 kernel/cbytecodes.mli | 44 +++++++++++++++++++++-----------------------
 1 file changed, 21 insertions(+), 23 deletions(-)

(limited to 'kernel/cbytecodes.mli')

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index b8de7619..f87090c7 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -1,15 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* $Id$ *)
 
 open Names
-open Term
+open Constr
 
 type tag = int
 
@@ -26,21 +28,26 @@ val cofix_evaluated_tag : tag
 val last_variant_tag : tag
 
 type structured_constant =
-  | Const_sorts of sorts
+  | 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.universe_level
-  | Const_type of Univ.universe
+  | Const_univ_level of Univ.Level.t
 
-val pp_struct_const : structured_constant -> Pp.std_ppcmds
+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
+
 module Label :
   sig
     type t = int
@@ -69,7 +76,7 @@ type instruction =
                    (** nb fv, init, lbl types, lbl bodies *)
   | Kclosurecofix of int * int * Label.t array * Label.t array
                    (** nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal of constant
+  | Kgetglobal of Constant.t
   | Kconst of structured_constant
   | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0
                                          ** is accu, all others are popped from
@@ -132,6 +139,7 @@ type fv_elem =
   FVnamed of Id.t
 | FVrel of int
 | FVuniv_var of int
+| FVevar of Evar.t
 
 type fv = fv_elem array
 
@@ -152,6 +160,7 @@ type vm_env = {
 
 
 type comp_env = {
+    arity : int;                 (* arity of the current function, 0 if none *)
     nb_uni_stack : int ;         (** number of universes on the stack       *)
     nb_stack : int;              (** number of variables on the stack       *)
     in_stack : int list;         (** position in the stack                  *)
@@ -163,16 +172,5 @@ type comp_env = {
     in_env : vm_env ref          (** the variables that are accessed        *)
   }
 
-val pp_bytecodes : bytecodes -> Pp.std_ppcmds
-val pp_fv_elem : fv_elem -> Pp.std_ppcmds
-
-(*spiwack: moved this here because I needed it for retroknowledge *)
-type block =
-  | Bconstr of constr
-  | Bstrconst of structured_constant
-  | Bmakeblock of int * block array
-  | Bconstruct_app of int * int * int * block array
-                  (** tag , nparams, arity *)
-  | Bspecial of (comp_env -> block array -> int -> bytecodes -> bytecodes) * block array
-                (** compilation function (see get_vm_constant_dynamic_info in
-                   retroknowledge.mli for more info) , argument array  *)
+val pp_bytecodes : bytecodes -> Pp.t
+val pp_fv_elem : fv_elem -> Pp.t
-- 
cgit v1.2.3