From 5c825f263698433ed4e8db8ccd0c14394520535a Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sat, 11 Aug 2012 13:33:26 +0000
Subject: fast bitwise operations (lor,land,lxor) on int31 and BigN

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15727 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cbytecodes.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel/cbytecodes.ml')

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index c0119aa26b..994242a8a4 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -114,6 +114,9 @@ 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
@@ -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