From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

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

(limited to 'kernel/cbytecodes.mli')

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index a996f750..215b6ad4 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -3,6 +3,14 @@ open Term
 
 type tag = int 
 
+val id_tag : tag
+val iddef_tag : tag
+val ind_tag : tag
+val fix_tag : tag
+val switch_tag : tag
+val cofix_tag : tag
+val cofix_evaluated_tag : tag
+
 type structured_constant =
   | Const_sorts of sorts
   | Const_ind of inductive
@@ -37,21 +45,24 @@ type instruction =
   | Krestart
   | Kgrab of int                        (* number of arguments *)
   | Kgrabrec of int                     (* rec arg *)
-  | Kcograb of int                      (* number of arguments *)
   | Kclosure of Label.t * int           (* label, number of free variables *)
   | Kclosurerec of int * int * Label.t array * Label.t array 
                    (* 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
   | Kconst of structured_constant
   | Kmakeblock of int * tag             (* size, tag *)
   | Kmakeprod 
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
-  | Kforce
   | Kswitch of Label.t array * Label.t array (* consts,blocks *)
-  | Kpushfield of int 
+  | Kpushfields of int 
+  | Kfield of int
+  | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
 
+
 and bytecodes = instruction list
 
 type fv_elem = FVnamed of identifier | FVrel of int
@@ -59,3 +70,4 @@ type fv_elem = FVnamed of identifier | FVrel of int
 type fv = fv_elem array
 
 val draw_instr : bytecodes -> unit
+
-- 
cgit v1.2.3