From f4586d1e8b1116340574d9660117f93e7a1e4e3b Mon Sep 17 00:00:00 2001
From: bgregoir
Date: Wed, 20 Jun 2007 09:43:36 +0000
Subject: ajout de head0 et tail0 en natif

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

(limited to 'kernel/cbytecodes.ml')

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index ee8cb1eea2..84d04d67e5 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -89,10 +89,13 @@ type instruction =
   | Kaddmuldivint31                     (* generic operation for shifting and
 					   cycling. Takes 3 int31 i j and s,
 					   and returns x*2^s+y/(2^(31-s) *)
-  | Kcompareint31                        (* unsigned comparison of int31
+  | Kcompareint31                       (* unsigned comparison of int31
 					   cf COMPAREINT31 in 
 					   kernel/byterun/coq_interp.c
 					   for more info *)
+  | Khead0int31                         (* Give the numbers of 0 in head of a in31*)
+  | Ktail0int31                         (* Give the numbers of 0 in tail of a in31 
+                                           ie low bits *)
   | Kisconst of Label.t                 (* conditional jump *)
   | Kareconst of int*Label.t            (* conditional jump *)
   | Kcompint31                          (* dynamic compilation of int31 *)
@@ -196,6 +199,8 @@ let rec instruction ppf = function
   | Kdiv21int31 -> fprintf ppf "\tdiv21int31"
   | Kdivint31 -> fprintf ppf "\tdivint31"
   | Kcompareint31 -> fprintf ppf "\tcompareint31"
+  | Khead0int31 -> fprintf ppf "\thead0int31"
+  | Ktail0int31 -> fprintf ppf "\ttail0int31"
   | Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31"
   | Kisconst lbl -> fprintf ppf "\tisconst %i" lbl
   | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
-- 
cgit v1.2.3