From f4586d1e8b1116340574d9660117f93e7a1e4e3b Mon Sep 17 00:00:00 2001
From: bgregoir <bgregoir@85f007b7-540e-0410-9357-904b9bb8a0f7>
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.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/cbytecodes.mli')

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index a2d4f7e01..86b465543 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -90,6 +90,9 @@ type instruction =
 					   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 *)
-- 
cgit v1.2.3