From fff07f8260867740f1f8d8b09bd26baa5f99e5c6 Mon Sep 17 00:00:00 2001
From: bgregoir
Date: Sat, 22 Jul 2006 17:42:45 +0000
Subject: - Ajout d'un cast vm dans la syntaxe :  x <: t     Part contre ces
 cas sont detruis dans les "Definition"     (pas dans les "Lemma") je
 comprends pas ou ils sont enlev'e...     Si une id'ee ...

- Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland.

- Meilleur compilation des coinductifs, on utilise maintenant vraimment
  du lazy. 

- Enfin un peu plus de doc dans le code de la vm.

  Benjamin



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 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 a996f75056..215b6ad4a7 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