From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 kernel/cbytecodes.mli | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

(limited to 'kernel/cbytecodes.mli')

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index c8cc9503..b65268f7 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -23,7 +23,7 @@ val cofix_evaluated_tag : tag
 
 type structured_constant =
   | Const_sorts of sorts
-  | Const_ind of inductive
+  | Const_ind of pinductive
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
 
@@ -60,7 +60,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 pconstant
   | Kconst of structured_constant
   | Kmakeblock of int * tag             (** size, tag *)
   | Kmakeprod
@@ -107,13 +107,14 @@ type instruction =
   | Kisconst of Label.t                 (** conditional jump *)
   | Kareconst of int*Label.t            (** conditional jump *)
   | Kcompint31                          (** dynamic compilation of int31 *)
-  | Kdecompint31                        (** dynamix decompilation of int31 
-   /spiwack *)
-
+  | Kdecompint31                        (** dynamix decompilation of int31 *)
+  | Klorint31                           (** bitwise operations: or and xor *)
+  | Klandint31
+  | Klxorint31
 
 and bytecodes = instruction list
 
-type fv_elem = FVnamed of identifier | FVrel of int
+type fv_elem = FVnamed of Id.t | FVrel of int
 
 type fv = fv_elem array
 
-- 
cgit v1.2.3