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

(limited to 'kernel/cbytecodes.ml')

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 5d6d92ff..ae679027 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -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        *)
@@ -27,7 +27,7 @@ let cofix_evaluated_tag = 6
 
 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
 
@@ -67,7 +67,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
@@ -114,11 +114,14 @@ type instruction =
   | Kareconst of int*Label.t            (* conditional jump *)
   | Kcompint31                          (* dynamic compilation of int31 *)
   | Kdecompint31                        (* dynamic decompilation of int31 *)
+  | Klorint31                            (* bitwise operations: or and xor *)
+  | Klandint31
+  | Klxorint31
 (* /spiwack *)
 
 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
 
@@ -182,7 +185,7 @@ let rec instruction ppf = function
       Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
       print_string " bodies = ";
       Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
-  | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
+  | Kgetglobal (id,u) -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
   | Kconst cst ->
       fprintf ppf "\tconst"
   | Kmakeblock(n, m) ->
@@ -220,6 +223,9 @@ let rec instruction ppf = function
   | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
   | Kcompint31 -> fprintf ppf "\tcompint31"
   | Kdecompint31 -> fprintf ppf "\tdecompint"
+  | Klorint31 -> fprintf ppf "\tlorint31"
+  | Klandint31 -> fprintf ppf "\tlandint31"
+  | Klxorint31 -> fprintf ppf "\tlxorint31"
 
 (* /spiwack *)
 
-- 
cgit v1.2.3