COMMITED BYTECODE COMPILER

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7

50 files changed, 4466 insertions, 177 deletions

diff --git a/kernel/.cvsignore b/kernel/.cvsignore
new file mode 100644
index 0000000000..81f20377e1
--- /dev/null
+++ b/kernel/.cvsignore
@@ -0,0 +1 @@
+copcodes.ml
diff --git a/kernel/byterun/.cvsignore b/kernel/byterun/.cvsignore
new file mode 100644
index 0000000000..bc5f347b0d
--- /dev/null
+++ b/kernel/byterun/.cvsignore
@@ -0,0 +1 @@
+coq_jumptbl.h
diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
new file mode 100644
index 0000000000..55ad3aa5e6
--- /dev/null
+++ b/kernel/byterun/coq_fix_code.c
@@ -0,0 +1,180 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h> 
+#include "config.h"
+#include "misc.h"
+#include "mlvalues.h"
+#include "fail.h"
+#include "memory.h"
+#include "coq_instruct.h"
+#include "coq_fix_code.h"
+
+void * coq_stat_alloc (asize_t sz)
+{
+  void * result = malloc (sz);
+  if (result == NULL) raise_out_of_memory ();
+  return result;
+}
+
+#ifdef THREADED_CODE
+
+char ** coq_instr_table;
+char * coq_instr_base;
+
+value coq_makeaccu (value i) {
+  code_t q;
+  code_t res = coq_stat_alloc(8);
+  q = res;
+  *q++ = (opcode_t)(coq_instr_table[MAKEACCU] - coq_instr_base);
+  *q = (opcode_t)Int_val(i);
+  return (value)res;
+}
+
+value coq_pushpop (value i) {
+  code_t res;
+  int n;
+  n = Int_val(i);
+  if (n == 0) {
+    res = coq_stat_alloc(4);
+    *res = (opcode_t)(coq_instr_table[STOP] - coq_instr_base);
+    return (value)res;
+  }
+  else {
+    code_t q;
+    res = coq_stat_alloc(12);
+    q = res;
+    *q++ = (opcode_t)(coq_instr_table[POP] - coq_instr_base);
+    *q++ = (opcode_t)n;
+    *q = (opcode_t)(coq_instr_table[STOP] - coq_instr_base);
+    return (value)res;
+  }
+}
+  
+code_t coq_thread_code (code_t code, asize_t len){
+  opcode_t instr;
+  code_t p, q;
+  code_t res = coq_stat_alloc(len);
+  int i;
+  q = res;
+  len /= sizeof(opcode_t);
+  for (p=code; p < code + len; /*nothing*/) {
+    instr = *p++;
+    *q++ = (opcode_t)(coq_instr_table[instr] - coq_instr_base);
+    switch(instr){
+      /* instruction with zero operand */
+    case ACC0: case ACC1: case ACC2: case ACC3: case ACC4: case ACC5:
+    case ACC6: case ACC7: case PUSH: case PUSHACC0: case PUSHACC1:
+    case PUSHACC2: case PUSHACC3: case PUSHACC4: case PUSHACC5: case PUSHACC6:
+    case PUSHACC7: case ENVACC1: case ENVACC2: case ENVACC3: case ENVACC4:
+    case PUSHENVACC1: case PUSHENVACC2: case PUSHENVACC3: case PUSHENVACC4:
+    case APPLY1: case APPLY2: case APPLY3: case RESTART: case OFFSETCLOSUREM2:
+    case OFFSETCLOSURE0: case OFFSETCLOSURE2: case PUSHOFFSETCLOSUREM2:
+    case PUSHOFFSETCLOSURE0: case PUSHOFFSETCLOSURE2:
+    case CONST0: case CONST1: case CONST2: case CONST3:
+    case PUSHCONST0: case PUSHCONST1: case PUSHCONST2: case PUSHCONST3:
+    case ACCUMULATE: case STOP: case FORCE: case MAKEPROD: 
+    break;
+    
+    /* instruction with one operand */
+    case ACC: case PUSHACC: case  POP: case ENVACC: case PUSHENVACC: 
+    case PUSH_RETADDR:
+    case APPLY: case APPTERM1: case APPTERM2: case APPTERM3: case RETURN:
+    case GRAB: case COGRAB: 
+    case OFFSETCLOSURE: case PUSHOFFSETCLOSURE: 
+    case GETGLOBAL: case PUSHGETGLOBAL: 
+    case GETGLOBALBOXED: case PUSHGETGLOBALBOXED: 
+    case MAKEBLOCK1: case MAKEBLOCK2: case MAKEBLOCK3: case MAKEACCU:
+    case CONSTINT: case PUSHCONSTINT: case GRABREC: case PUSHFIELD:
+    *q++ = *p++;
+    break;
+    
+    /* instruction with two operands */
+    case APPTERM: case MAKEBLOCK: case CLOSURE:
+      *q++ = *p++; *q++ = *p++;
+      break;
+    
+    /* instruction with four operands */ 
+    case MAKESWITCHBLOCK:
+      *q++ = *p++; *q++ = *p++; *q++ = *p++; *q++ = *p++;
+    break;
+    
+    /* instruction with arbitrary operands */
+    case CLOSUREREC: {
+      int i; 
+      uint32 n = 2*(*p) + 3; /* ndefs, nvars, start, typlbls,lbls*/
+      for(i=0; i < n; i++) *q++ = *p++;
+    }
+    break; 
+
+    case SWITCH: {
+      int i;
+      uint32 sizes = *p;
+      uint32 const_size = sizes & 0xFFFF;
+      uint32 block_size = sizes >> 16;
+      sizes = const_size + block_size + 1 ;/* sizes */
+      for(i=0; i < sizes; i++) *q++ = *p++;
+    }  
+    break;
+    
+    default: 
+       invalid_argument("Fatal error in coq_thread_code : bad opcode");
+    break;
+    }
+  }
+  if (p != code + len) fprintf(stderr, "error thread code\n");
+  return res;
+}
+
+value coq_tcode_of_code(value code, value len){
+  return (value)coq_thread_code((code_t)code,(asize_t) Long_val(len));
+}
+#else
+
+value coq_makeaccu (value i) {
+  code_t q;
+  code_t res = coq_stat_alloc(8);
+  q = res;
+  *q++ = (opcode_t)MAKEACCU;
+  *q = (opcode_t)Int_val(i);
+  return (value)res;
+}
+
+value coq_pushpop (value i) {
+  code_t res;
+  int n;
+  n = Int_val(i);
+  if (n == 0) {
+    res = coq_stat_alloc(4);
+    *res = (opcode_t)STOP;
+    return (value)res;
+  }
+  else {
+    res = coq_stat_alloc(12);
+    q = res;
+    *q++ = (opcode_t)POP;
+    *q++ = (opcode_t)n;
+    *q = (opcode_t)STOP;
+    return (value)res;
+  }
+}
+
+value coq_tcode_of_code(value s, value size) 
+{
+  void * new_s = coq_stat_alloc(Int_val(size));
+  memmove(new_s, &Byte(s, 0), Int_val(size));
+  return (value)new_s;
+}
+
+#endif /* THREADED_CODE */
+
+
+
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
new file mode 100644
index 0000000000..bceb104e95
--- /dev/null
+++ b/kernel/byterun/coq_fix_code.h
@@ -0,0 +1,30 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+
+#ifndef _COQ_FIX_CODE_
+#define _COQ_FIX_CODE_
+
+#include "mlvalues.h"
+void * coq_stat_alloc (asize_t sz);
+
+#ifdef THREADED_CODE
+extern char ** coq_instr_table;
+extern char * coq_instr_base;
+#define Is_instruction(i1,i2) \
+       (*i1 == (opcode_t)(coq_instr_table[i2] - coq_instr_base))
+#else 
+#define Is_instruction(i1,i2) (*i1 == i2)
+#endif
+
+value coq_tcode_of_code(value code, value len);
+value coq_makeaccu (value i);
+value coq_pushpop (value i);
+#endif /* _COQ_FIX_CODE_ */
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
new file mode 100644
index 0000000000..2f08532648
--- /dev/null
+++ b/kernel/byterun/coq_gc.h
@@ -0,0 +1,48 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#ifndef _COQ_CAML_GC_
+#define _COQ_CAML_GC_
+#include "mlvalues.h"
+#include "alloc.h"
+
+typedef void (*scanning_action) (value, value *);
+
+
+CAMLextern char *young_ptr;
+CAMLextern char *young_limit;
+CAMLextern void (*scan_roots_hook) (scanning_action);
+CAMLextern void minor_collection (void);
+
+#define Caml_white (0 << 8)
+#define Caml_black (3 << 8)
+
+#define Make_header(wosize, tag, color)                                 \
+  (((header_t) (((header_t) (wosize) << 10)                             \
+		+ (color)                                               \
+		+ (tag_t) (tag)))   					\
+   )
+
+
+#define Alloc_small(result, wosize, tag) do{                            \
+  young_ptr -= Bhsize_wosize (wosize);                                  \
+  if (young_ptr < young_limit){                                         \
+    young_ptr += Bhsize_wosize (wosize);                                \
+    Setup_for_gc;                                                       \
+    minor_collection ();                                                \
+    Restore_after_gc;                                                   \
+    young_ptr -= Bhsize_wosize (wosize);                                \
+  }                                                                     \
+  Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black);        \
+  (result) = Val_hp (young_ptr);                                        \
+  }while(0) 
+
+
+#endif /*_COQ_CAML_GC_ */
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
new file mode 100644
index 0000000000..2c23a4c89e
--- /dev/null
+++ b/kernel/byterun/coq_instruct.h
@@ -0,0 +1,40 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#ifndef _COQ_INSTRUCT_
+#define _COQ_INSTRUCT_
+
+enum instructions {
+  ACC0, ACC1, ACC2, ACC3, ACC4, ACC5, ACC6, ACC7, ACC,
+  PUSH, 
+  PUSHACC0, PUSHACC1, PUSHACC2, PUSHACC3, PUSHACC4,
+  PUSHACC5, PUSHACC6, PUSHACC7, PUSHACC, 
+  POP,
+  ENVACC1, ENVACC2, ENVACC3, ENVACC4, ENVACC,
+  PUSHENVACC1, PUSHENVACC2, PUSHENVACC3, PUSHENVACC4, PUSHENVACC,
+  PUSH_RETADDR,
+  APPLY, APPLY1, APPLY2, APPLY3,
+  APPTERM, APPTERM1, APPTERM2, APPTERM3,
+  RETURN, RESTART, GRAB, GRABREC, COGRAB, 
+  CLOSURE, CLOSUREREC, 
+  OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE,
+  PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, 
+  PUSHOFFSETCLOSURE,
+  GETGLOBAL, PUSHGETGLOBAL,
+  GETGLOBALBOXED, PUSHGETGLOBALBOXED,
+  MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, 
+  MAKESWITCHBLOCK, MAKEACCU, MAKEPROD,
+  FORCE, SWITCH, PUSHFIELD,
+  CONST0, CONST1, CONST2, CONST3, CONSTINT,
+  PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
+  ACCUMULATE, STOP
+};
+
+#endif /* _COQ_INSTRUCT_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
new file mode 100644
index 0000000000..a5f6f01d7c
--- /dev/null
+++ b/kernel/byterun/coq_interp.c
@@ -0,0 +1,857 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+/* The bytecode interpreter */
+
+#include <stdio.h>
+#include "coq_gc.h"
+#include "coq_instruct.h"
+#include "coq_fix_code.h"
+#include "coq_memory.h"  
+#include "coq_values.h"
+
+
+/* Registers for the abstract machine:
+        pc         the code pointer
+        sp         the stack pointer (grows downward)
+        accu       the accumulator
+        env        heap-allocated environment
+        trapsp     pointer to the current trap frame
+        extra_args number of extra arguments provided by the caller
+
+sp is a local copy of the global variable extern_sp. */
+
+
+
+/* Instruction decoding */
+
+
+#ifdef THREADED_CODE
+#  define Instruct(name) coq_lbl_##name: 
+#  if defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
+#    define coq_Jumptbl_base ((char *) &&coq_lbl_ACC0)
+#  else
+#    define coq_Jumptbl_base ((char *) 0)
+#    define coq_jumptbl_base ((char *) 0)
+#  endif
+#  ifdef DEBUG
+#    define Next goto next_instr
+#  else
+#    ifdef __ia64__
+#      define Next goto *(void *)(coq_jumptbl_base + *((uint32 *) pc)++)
+#    else
+#      define Next goto *(void *)(coq_jumptbl_base + *pc++)
+#    endif
+#  endif
+#else 
+#  define Instruct(name) case name: print_instr(name);
+#  define Next break
+#endif 
+
+/* GC interface */
+#define Setup_for_gc { sp -= 2; sp[0] = accu; sp[1] = coq_env; coq_sp = sp; }
+#define Restore_after_gc { accu = sp[0]; coq_env = sp[1]; sp += 2; }
+
+
+/* Register optimization.
+   Some compilers underestimate the use of the local variables representing
+   the abstract machine registers, and don't put them in hardware registers,
+   which slows down the interpreter considerably.
+   For GCC, Xavier Leroy have hand-assigned hardware registers for 
+   several architectures.
+*/
+
+#if defined(__GNUC__) && !defined(DEBUG)
+#ifdef __mips__
+#define PC_REG asm("$16")
+#define SP_REG asm("$17")
+#define ACCU_REG asm("$18")
+#endif
+#ifdef __sparc__
+#define PC_REG asm("%l0")
+#define SP_REG asm("%l1")
+#define ACCU_REG asm("%l2")
+#endif
+#ifdef __alpha__
+#ifdef __CRAY__
+#define PC_REG asm("r9")
+#define SP_REG asm("r10")
+#define ACCU_REG asm("r11")
+#define JUMPTBL_BASE_REG asm("r12")
+#else
+#define PC_REG asm("$9")
+#define SP_REG asm("$10")
+#define ACCU_REG asm("$11")
+#define JUMPTBL_BASE_REG asm("$12")
+#endif
+#endif
+#ifdef __i386__
+#define PC_REG asm("%esi")
+#define SP_REG asm("%edi")
+#define ACCU_REG
+#endif
+#if defined(PPC) || defined(_POWER) || defined(_IBMR2)
+#define PC_REG asm("26")
+#define SP_REG asm("27")
+#define ACCU_REG asm("28")
+#endif
+#ifdef __hppa__
+#define PC_REG asm("%r18")
+#define SP_REG asm("%r17")
+#define ACCU_REG asm("%r16")
+#endif
+#ifdef __mc68000__
+#define PC_REG asm("a5")
+#define SP_REG asm("a4")
+#define ACCU_REG asm("d7")
+#endif
+#ifdef __arm__
+#define PC_REG asm("r9")
+#define SP_REG asm("r8")
+#define ACCU_REG asm("r7")
+#endif
+#ifdef __ia64__
+#define PC_REG asm("36")
+#define SP_REG asm("37")
+#define ACCU_REG asm("38")
+#define JUMPTBL_BASE_REG asm("39")
+#endif
+#endif
+
+/* The interpreter itself */
+
+value coq_interprete
+(code_t coq_pc, value coq_accu, value coq_env, long coq_extra_args)
+{
+  /*Declaration des variables */
+#ifdef PC_REG
+  register code_t pc PC_REG;
+  register value * sp SP_REG;
+  register value accu ACCU_REG;
+#else
+  register code_t pc;
+  register value * sp;
+  register value accu;
+#endif
+#if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
+#ifdef JUMPTBL_BASE_REG
+  register char * coq_jumptbl_base JUMPTBL_BASE_REG;
+#else
+  register char * coq_jumptbl_base;
+#endif
+#endif
+#ifdef THREADED_CODE
+  static void * coq_jumptable[] = {
+#    include "coq_jumptbl.h"
+  };
+#else 
+  opcode_t curr_instr;
+#endif
+  value * global_transp;
+
+  if (coq_pc == NULL) {           /* Interpreter is initializing */
+#ifdef THREADED_CODE
+    coq_instr_table = (char **) coq_jumptable;
+    coq_instr_base = coq_Jumptbl_base;
+#endif
+    return Val_unit;
+  }
+#if defined(THREADED_CODE) && defined(ARCH_SIXTYFOUR) && !defined(ARCH_CODE32)
+  coq_jumptbl_base = coq_Jumptbl_base;
+#endif
+
+  /* Initialisation */
+  if (default_transp == BOXED) global_transp = &coq_global_boxed;
+  else global_transp = &coq_global_transp;
+  sp = coq_sp;
+  pc = coq_pc;
+  accu = coq_accu;
+#ifdef THREADED_CODE
+  goto *(void *)(coq_jumptbl_base + *pc++); /* Jump to the first instruction */
+#else
+  while(1) {
+    curr_instr = *pc++;
+    switch(curr_instr) {
+#endif
+/* Basic stack operations */
+      
+      Instruct(ACC0){
+	accu = sp[0]; Next;
+      }
+      Instruct(ACC1){
+	accu = sp[1]; Next;
+      }
+      Instruct(ACC2){
+	accu = sp[2]; Next;
+      }
+      Instruct(ACC3){
+	accu = sp[3]; Next;
+      }
+      Instruct(ACC4){
+	accu = sp[4]; Next;
+      }
+      Instruct(ACC5){
+	accu = sp[5]; Next;
+      }
+      Instruct(ACC6){
+	accu = sp[6]; Next;
+      }
+      Instruct(ACC7){
+        accu = sp[7]; Next;
+      }      
+      Instruct(PUSH){
+	*--sp = accu; Next;
+      }
+      Instruct(PUSHACC0) {
+        *--sp = accu; Next;
+      }
+      Instruct(PUSHACC1){
+        *--sp = accu; accu = sp[1]; Next;
+      }
+      Instruct(PUSHACC2){
+        *--sp = accu; accu = sp[2]; Next;
+      }
+      Instruct(PUSHACC3){
+	*--sp = accu; accu = sp[3]; Next;
+      }
+      Instruct(PUSHACC4){
+	*--sp = accu; accu = sp[4]; Next;
+      }
+      Instruct(PUSHACC5){
+	*--sp = accu; accu = sp[5]; Next;
+      }
+      Instruct(PUSHACC6){
+	*--sp = accu; accu = sp[6]; Next;
+      }
+      Instruct(PUSHACC7){
+	*--sp = accu; accu = sp[7]; Next;
+      }
+      Instruct(PUSHACC){
+	*--sp = accu;
+      }
+      /* Fallthrough */
+      
+      Instruct(ACC){
+	accu = sp[*pc++];
+        Next;
+      }
+      
+      Instruct(POP){
+	sp += *pc++;
+	Next;
+      }
+      /* Access in heap-allocated environment */
+      
+      Instruct(ENVACC1){
+	accu = Field(coq_env, 1); Next;
+      }
+      Instruct(ENVACC2){
+	accu = Field(coq_env, 2); Next;
+      }
+      Instruct(ENVACC3){
+	accu = Field(coq_env, 3); Next;
+      }
+      Instruct(ENVACC4){
+	accu = Field(coq_env, 4); Next;
+      }
+      Instruct(PUSHENVACC1){
+	*--sp = accu; accu = Field(coq_env, 1); Next;
+      }
+      Instruct(PUSHENVACC2){
+	*--sp = accu; accu = Field(coq_env, 2); Next;
+      }
+      Instruct(PUSHENVACC3){
+	*--sp = accu; accu = Field(coq_env, 3); Next;
+      }
+      Instruct(PUSHENVACC4){
+	*--sp = accu; accu = Field(coq_env, 4); Next;
+      }
+      Instruct(PUSHENVACC){
+	*--sp = accu;
+      }
+      /* Fallthrough */
+      Instruct(ENVACC){
+	accu = Field(coq_env, *pc++);
+        Next;
+      }
+      /* Function application */
+      
+      Instruct(PUSH_RETADDR) {
+	sp -= 3;
+	sp[0] = (value) (pc + *pc);
+	sp[1] = coq_env;
+	sp[2] = Val_long(coq_extra_args);
+	coq_extra_args = 0;
+	pc++;
+	Next;
+      }
+      Instruct(APPLY) {
+	coq_extra_args = *pc - 1;
+	pc = Code_val(accu);
+	coq_env = accu;
+	goto check_stacks;
+      }
+      Instruct(APPLY1) {
+	value arg1 = sp[0];
+	sp -= 3;
+	sp[0] = arg1;
+	sp[1] = (value)pc;
+	sp[2] = coq_env;
+	sp[3] = Val_long(coq_extra_args);
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args = 0;
+	goto check_stacks;
+      }
+      Instruct(APPLY2) {
+	value arg1 = sp[0];
+	value arg2 = sp[1];
+	sp -= 3;
+	sp[0] = arg1;
+	sp[1] = arg2;
+	sp[2] = (value)pc;
+	sp[3] = coq_env;
+	sp[4] = Val_long(coq_extra_args);
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args = 1;
+	goto check_stacks;
+      }
+      Instruct(APPLY3) {
+	value arg1 = sp[0];
+	value arg2 = sp[1];
+	value arg3 = sp[2];
+	sp -= 3;
+	sp[0] = arg1;
+	sp[1] = arg2;
+	sp[2] = arg3;
+	sp[3] = (value)pc;
+	sp[4] = coq_env;
+	sp[5] = Val_long(coq_extra_args);
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args = 2;
+	goto check_stacks;
+      }
+
+      Instruct(APPTERM) {
+	int nargs = *pc++;
+	int slotsize = *pc;
+	value * newsp;
+	int i;
+	/* Slide the nargs bottom words of the current frame to the top
+	   of the frame, and discard the remainder of the frame */
+	newsp = sp + slotsize - nargs;
+	for (i = nargs - 1; i >= 0; i--) newsp[i] = sp[i];
+	sp = newsp;
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args += nargs - 1;
+	goto check_stacks;
+      }
+      Instruct(APPTERM1) {
+	value arg1 = sp[0];
+	sp = sp + *pc - 1;
+	sp[0] = arg1;
+	pc = Code_val(accu);
+	coq_env = accu;
+	goto check_stacks;
+      }
+      Instruct(APPTERM2) {
+	value arg1 = sp[0];
+	value arg2 = sp[1];
+	sp = sp + *pc - 2;
+	sp[0] = arg1;
+	sp[1] = arg2;
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args += 1;
+	goto check_stacks;
+      }
+      Instruct(APPTERM3) {
+	value arg1 = sp[0];
+	value arg2 = sp[1];
+	value arg3 = sp[2];
+	sp = sp + *pc - 3;
+	sp[0] = arg1;
+	sp[1] = arg2;
+	sp[2] = arg3;
+	pc = Code_val(accu);
+	coq_env = accu;
+	coq_extra_args += 2;
+	goto check_stacks;
+      }
+      
+      Instruct(RETURN) {
+	sp += *pc++;
+	if (coq_extra_args > 0) {
+	  coq_extra_args--;
+	  pc = Code_val(accu);
+	  coq_env = accu;
+	} else {
+	  pc = (code_t)(sp[0]);
+	  coq_env = sp[1];
+	  coq_extra_args = Long_val(sp[2]);
+	  sp += 3;
+	}
+	Next;
+      }
+      
+      Instruct(RESTART) {
+	int num_args = Wosize_val(coq_env) - 2;
+	int i;
+	sp -= num_args;
+	for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2);
+	coq_env = Field(coq_env, 1);
+	coq_extra_args += num_args;
+	Next;
+      }
+      
+      Instruct(GRAB) {
+	int required = *pc++;
+	if (coq_extra_args >= required) {
+	  coq_extra_args -= required;
+	} else {
+	  mlsize_t num_args, i;
+	  num_args = 1 + coq_extra_args; /* arg1 + extra args */
+          Alloc_small(accu, num_args + 2, Closure_tag); 
+	  Field(accu, 1) = coq_env;
+	  for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+	  Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
+	  sp += num_args;
+	  pc = (code_t)(sp[0]);
+	  coq_env = sp[1];
+	  coq_extra_args = Long_val(sp[2]);
+	  sp += 3;
+	}
+	Next;
+      }
+
+      Instruct(COGRAB){
+	int required = *pc++;
+	if(forcable == Val_true) {
+	  /* L'instruction précédante est FORCE */
+	  if (coq_extra_args > 0) coq_extra_args--;
+	  pc++;
+	} else { /* L'instruction précédante est APPLY */
+	  mlsize_t num_args, i;
+	  num_args = 1 + coq_extra_args; /* arg1 + extra args */
+	  Alloc_small(accu, num_args + 2, Closure_tag); 
+	  Field(accu, 1) = coq_env;
+	  for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+	  Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
+	  sp += num_args;
+	  pc = (code_t)(sp[0]);
+	  coq_env = sp[1];
+	  coq_extra_args = Long_val(sp[2]);
+	  sp += 3;
+	}
+	Next;
+      }
+      Instruct(GRABREC) { 
+	int rec_pos = *pc++; /* commence a zero */
+	if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) {
+	  pc++;/* On saute le Restart */
+	} else {
+	  if (coq_extra_args < rec_pos) {
+	    mlsize_t num_args, i;
+	    num_args = 1 + coq_extra_args; /* arg1 + extra args */
+	    Alloc_small(accu, num_args + 2, Closure_tag); 
+	    Field(accu, 1) = coq_env;
+	    for (i = 0; i < num_args; i++) Field(accu, i + 2) = sp[i];
+	    Code_val(accu) = pc - 3; 
+	    sp += num_args;
+	    pc = (code_t)(sp[0]);
+	    coq_env = sp[1];
+	    coq_extra_args = Long_val(sp[2]);
+	    sp += 3;
+	  } else {
+	    /* L'argument recursif est un accumulateur */
+	    mlsize_t num_args, i;
+	    /* Construction du PF partiellement appliqué */ 
+	    Alloc_small(accu, rec_pos + 2, Closure_tag); 
+	    Field(accu, 1) = coq_env;
+	    for (i = 0; i < rec_pos; i++) Field(accu, i + 2) = sp[i];
+	    Code_val(accu) = pc;
+	    sp += rec_pos;
+	    *--sp = accu;
+	      /* Construction de l'atom */
+	    Alloc_small(accu, 2, ATOM_FIX_TAG);
+	    Field(accu,1) = sp[0];
+	    Field(accu,0)  = sp[1];
+	    sp++; sp[0] = accu;
+	      /* Construction de l'accumulateur */
+	    num_args = coq_extra_args - rec_pos;
+	    Alloc_small(accu, 2+num_args, Accu_tag);
+	    Code_val(accu) = accumulate;
+	    Field(accu,1) = sp[0]; sp++;
+	    for (i = 0; i < num_args;i++)Field(accu, i + 2) = sp[i];
+	    sp += num_args;
+	    pc = (code_t)(sp[0]);
+	    coq_env = sp[1];
+	    coq_extra_args = Long_val(sp[2]);
+	    sp += 3;
+	  }
+	}
+	Next;
+      }
+	
+      Instruct(CLOSURE) {
+	int nvars = *pc++;
+	int i;
+	if (nvars > 0) *--sp = accu;
+	Alloc_small(accu, 1 + nvars, Closure_tag);
+	Code_val(accu) = pc + *pc;
+	pc++;
+	for (i = 0; i < nvars; i++) Field(accu, i + 1) = sp[i];
+	sp += nvars;
+	Next;
+      }
+
+      Instruct(CLOSUREREC) {
+	int nfuncs = *pc++;
+	int nvars = *pc++;
+	int start = *pc++;
+	int i;
+	value * p;
+	if (nvars > 0) *--sp = accu;
+	/* construction du vecteur de type */
+	Alloc_small(accu, nfuncs, 0);
+	for(i = 0; i < nfuncs; i++) {
+	  Field(accu,i) = (value)(pc+pc[i]);
+	}
+	pc += nfuncs;
+	*--sp=accu;
+	Alloc_small(accu, nfuncs * 2 + nvars, Closure_tag);
+	Field(accu, nfuncs * 2 + nvars - 1) = *sp++;
+	/* On remplie la partie pour les variables libres */
+	p = &Field(accu, nfuncs * 2 - 1);
+	for (i = 0; i < nvars; i++) {
+	  *p++ = *sp++;
+	}
+	p = &Field(accu, 0);
+	*p = (value) (pc + pc[0]);
+	p++;
+	for (i = 1; i < nfuncs; i++) {
+	  *p = Make_header(i * 2, Infix_tag, Caml_white);
+	  p++;                                /* color irrelevant. */
+	  *p = (value) (pc + pc[i]);
+	  p++;
+	}
+	pc += nfuncs;
+	accu = accu + 2 * start * sizeof(value);
+	Next;
+      }
+     
+      Instruct(PUSHOFFSETCLOSURE) {
+	*--sp = accu;
+      } /* fallthrough */
+      Instruct(OFFSETCLOSURE) {
+	accu = coq_env + *pc++ * sizeof(value); Next;
+      }
+      Instruct(PUSHOFFSETCLOSUREM2) {
+	*--sp = accu;
+      } /* fallthrough */
+      Instruct(OFFSETCLOSUREM2) {
+	accu = coq_env - 2 * sizeof(value); Next;
+      }
+      Instruct(PUSHOFFSETCLOSURE0) {
+	*--sp = accu; 
+      }/* fallthrough */
+      Instruct(OFFSETCLOSURE0) {
+	accu = coq_env; Next;
+      }
+      Instruct(PUSHOFFSETCLOSURE2){
+	*--sp = accu; /* fallthrough */
+      }
+      Instruct(OFFSETCLOSURE2) {
+	accu = coq_env + 2 * sizeof(value); Next;
+      }
+
+/* Access to global variables */
+
+      Instruct(PUSHGETGLOBAL) {
+	*--sp = accu;
+      }
+      /* Fallthrough */
+      Instruct(GETGLOBAL){
+	accu = Field(coq_global_data, *pc);
+        pc++;
+        Next;
+      }    
+      Instruct(PUSHGETGLOBALBOXED) {
+	*--sp = accu;
+      }
+      /* Fallthrough */
+      Instruct(GETGLOBALBOXED){
+
+	accu = Field(*global_transp, *pc);
+        pc++;
+        Next;
+      }
+/* Allocation of blocks */
+
+      Instruct(MAKEBLOCK) {
+	mlsize_t wosize = *pc++;
+	tag_t tag = *pc++;
+	mlsize_t i;
+	value block;
+	Alloc_small(block, wosize, tag);
+	Field(block, 0) = accu;
+	for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
+	accu = block;
+	Next;
+      }
+      Instruct(MAKEBLOCK1) {
+	
+	tag_t tag = *pc++;
+	value block;
+	Alloc_small(block, 1, tag);
+	Field(block, 0) = accu;
+	accu = block;
+	Next;
+      }
+      Instruct(MAKEBLOCK2) {
+	
+	tag_t tag = *pc++;
+	value block;
+	Alloc_small(block, 2, tag);
+	Field(block, 0) = accu;
+	Field(block, 1) = sp[0];
+	sp += 1;
+	accu = block;
+	Next;
+      }
+      Instruct(MAKEBLOCK3) {
+	tag_t tag = *pc++;
+	value block;
+	Alloc_small(block, 3, tag);
+	Field(block, 0) = accu;
+	Field(block, 1) = sp[0];
+	Field(block, 2) = sp[1];
+	sp += 2;
+	accu = block;
+	Next;
+      }
+
+  
+/* Access to components of blocks */
+        
+	
+/* Branches and conditional branches */
+      Instruct(FORCE) {
+	if (Is_block(accu) && Tag_val(accu) == Closure_tag) {
+	  /* On pousse l'addresse de retour et l'argument */
+	  sp -= 3;
+	  sp[0] = (value) (pc);
+	  sp[1] = coq_env;
+	  sp[2] = Val_long(coq_extra_args);
+	  /* On evalue le cofix */
+	  coq_extra_args = 0;
+	  pc = Code_val(accu);
+	  coq_env = accu;
+	  goto check_stacks;
+	}
+	Next;
+      }
+           
+    
+      Instruct(SWITCH) {
+	uint32 sizes = *pc++;
+	if (Is_block(accu)) {
+	  long index = Tag_val(accu);
+	  pc += pc[(sizes & 0xFFFF) + index];
+	} else {
+	  long index = Long_val(accu);
+	  pc += pc[index];
+	}
+	  Next;
+      }
+      Instruct(PUSHFIELD){
+	int i;
+	int size = *pc++;
+	sp -= size;
+	for(i=0;i<size;i++)sp[i] = Field(accu,i);
+	Next;
+      }
+	
+      Instruct(MAKESWITCHBLOCK) {
+	mlsize_t sz;
+	int i, annot;
+	code_t typlbl,swlbl;
+	typlbl = (code_t)pc + *pc; 
+	pc++;
+	swlbl = (code_t)pc + *pc; 
+	pc++;
+	annot = *pc++;
+	sz = *pc++;
+	*--sp = accu;
+	*--sp=Field(coq_global_data, annot);
+	/* On sauve la pile */
+	if (sz == 0) accu = Atom(0);
+	else {
+	  Alloc_small(accu, sz, Default_tag);
+	  if (Field(*sp, 2) == Val_true) {
+	    for (i = 0; i < sz; i++) Field(accu, i) = sp[i+2];
+	  }else{
+	    for (i = 0; i < sz; i++) Field(accu, i) = sp[i+5];
+	  }
+	}
+	*--sp = accu;
+	/* On cree le zipper switch */
+	Alloc_small(accu, 5, Default_tag);
+	Field(accu, 0) =  (value)typlbl; Field(accu, 1) = (value)swlbl; 
+	Field(accu, 2) = sp[1]; Field(accu, 3) = sp[0]; 
+	Field(accu, 4) = coq_env;
+	sp++;sp[0] = accu;
+	/* On cree l'atome */
+	Alloc_small(accu, 2, ATOM_SWITCH_TAG);
+	Field(accu, 0) = sp[1]; Field(accu, 1) = sp[0];
+	sp++;sp[0] = accu;
+	/* On cree l'accumulateur */
+	Alloc_small(accu, 2, Accu_tag);
+	Code_val(accu) = accumulate; 
+	Field(accu,1) = *sp++;
+	Next;
+      }
+
+      /* Stack checks */
+      
+    check_stacks:
+      if (sp < coq_stack_threshold) {
+	coq_sp = sp;
+	realloc_coq_stack(Coq_stack_threshold);
+	sp = coq_sp;
+      }
+      Next;
+      /* Fall through CHECK_SIGNALS */
+
+/* Integer constants */
+
+      Instruct(CONST0){
+	accu = Val_int(0); Next;}
+      Instruct(CONST1){
+	accu = Val_int(1); Next;}
+      Instruct(CONST2){
+	accu = Val_int(2); Next;}
+      Instruct(CONST3){
+	accu = Val_int(3); Next;}
+      
+      Instruct(PUSHCONST0){
+	*--sp = accu; accu = Val_int(0); Next;
+      }
+      Instruct(PUSHCONST1){
+	*--sp = accu; accu = Val_int(1); Next;
+      }
+      Instruct(PUSHCONST2){
+	*--sp = accu; accu = Val_int(2); Next;
+      }
+      Instruct(PUSHCONST3){
+	*--sp = accu; accu = Val_int(3); Next;
+      }
+
+      Instruct(PUSHCONSTINT){
+	*--sp = accu;
+      }
+      /* Fallthrough */
+      Instruct(CONSTINT) {
+	accu = Val_int(*pc);
+	pc++;
+	Next;
+      }
+
+/* Debugging and machine control */
+
+      Instruct(STOP){
+	coq_sp = sp;
+	return accu;
+      }
+      
+      Instruct(ACCUMULATE) {
+	mlsize_t i, size;
+	size = Wosize_val(coq_env);
+	Alloc_small(accu, size + coq_extra_args + 1, Accu_tag);
+	for(i = 0; i < size; i++) Field(accu, i) = Field(coq_env, i);
+	for(i = size; i <= coq_extra_args + size; i++) 
+	  Field(accu, i) = *sp++;
+	pc = (code_t)(sp[0]);
+	coq_env = sp[1];
+	coq_extra_args = Long_val(sp[2]);
+	sp += 3;
+	Next;
+      }
+      
+      Instruct(MAKEACCU) {
+	int i;
+	Alloc_small(accu, coq_extra_args + 3, Accu_tag);
+	Code_val(accu) = accumulate;
+	Field(accu,1) = Field(coq_atom_tbl, *pc);
+	for(i = 2; i < coq_extra_args + 3; i++) Field(accu, i) = *sp++;
+	pc = (code_t)(sp[0]);
+	coq_env = sp[1];
+	coq_extra_args = Long_val(sp[2]);
+	sp += 3;
+	Next;
+      }
+     
+      Instruct(MAKEPROD) {
+	*--sp=accu;
+	Alloc_small(accu,2,0);
+	Field(accu, 0) = sp[0];
+	Field(accu, 1) = sp[1];
+	sp += 2;
+	Next;
+      }
+      
+#ifndef THREADED_CODE
+    default:
+      /*fprintf(stderr, "%d\n", *pc);*/
+      failwith("Coq VM: Fatal error: bad opcode");
+    }
+  }
+#endif
+}
+
+value coq_push_ra(value tcode) { 
+  coq_sp -= 3;
+  coq_sp[0] = (value) tcode;
+  coq_sp[1] = Val_unit;
+  coq_sp[2] = Val_long(0);
+  return Val_unit;
+}
+
+value coq_push_val(value v) {
+  *--coq_sp = v;
+  return Val_unit;
+}
+
+value coq_push_arguments(value args) {
+  int nargs,i;
+  nargs = Wosize_val(args) - 2;
+  coq_sp -= nargs;
+  for(i = 0; i < nargs; i++) coq_sp[i] = Field(args, i+2);
+  return Val_unit;
+}
+
+value coq_push_vstack(value stk) {
+  int len,i;
+  len = Wosize_val(stk);
+  coq_sp -= len;
+  for(i = 0; i < len; i++) coq_sp[i] = Field(stk,i);
+  return Val_unit;
+}
+
+value  coq_interprete_ml(value tcode, value a, value e, value ea) {
+  return coq_interprete((code_t)tcode, a, e, Long_val(ea));
+}
+
+value coq_eval_tcode (value tcode, value e) {
+  return coq_interprete_ml(tcode, Val_unit, e, 0);
+}
diff --git a/kernel/byterun/coq_interp.h b/kernel/byterun/coq_interp.h
new file mode 100644
index 0000000000..76e6894404
--- /dev/null
+++ b/kernel/byterun/coq_interp.h
@@ -0,0 +1,23 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+
+value coq_push_ra(value tcode);
+
+value coq_push_val(value v);
+
+value coq_push_arguments(value args);
+
+value coq_push_vstack(value stk);
+
+value  coq_interprete_ml(value tcode, value a, value e, value ea);
+
+value coq_eval_tcode (value tcode, value e);
+
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
new file mode 100644
index 0000000000..233397b020
--- /dev/null
+++ b/kernel/byterun/coq_memory.c
@@ -0,0 +1,270 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#include <stdio.h>
+#include <string.h> 
+#include "coq_gc.h"
+#include "coq_instruct.h"
+#include "coq_fix_code.h"
+#include "coq_memory.h"
+
+/* stack */
+
+value * coq_stack_low;
+value * coq_stack_high;
+value * coq_stack_threshold;
+asize_t coq_max_stack_size = Coq_max_stack_size;
+/* global_data */
+
+
+value coq_global_data;
+value coq_global_transp;
+value coq_global_boxed;
+int default_transp;
+value coq_atom_tbl;
+
+/* interp state */
+
+long coq_saved_sp_offset;
+value * coq_sp;
+value forcable;
+/* Some predefined pointer code */ 
+code_t accumulate;
+
+/* functions over global environment */
+
+void coq_stat_free (void * blk)
+{
+  free (blk);
+}
+
+value coq_static_alloc(value size) /* ML */
+{
+  return (value) coq_stat_alloc((asize_t) Long_val(size));
+}
+
+value coq_static_free(value blk)  /* ML */
+{
+  coq_stat_free((void *) blk);
+  return Val_unit;
+}
+
+value accumulate_code(value unit) /* ML */
+{
+  return (value) accumulate;
+}
+
+static void (*coq_prev_scan_roots_hook) (scanning_action);
+
+static void coq_scan_roots(scanning_action action)
+{
+  register value * i;
+  /* Scan the global variables */
+  (*action)(coq_global_data, &coq_global_data);
+  (*action)(coq_global_transp, &coq_global_transp);
+  (*action)(coq_global_boxed, &coq_global_boxed);
+  (*action)(coq_atom_tbl, &coq_atom_tbl);
+  /* Scan the stack */
+  for (i = coq_sp; i < coq_stack_high; i++) {
+    (*action) (*i, i);
+  };
+  /* Hook */
+  if (coq_prev_scan_roots_hook != NULL) (*coq_prev_scan_roots_hook)(action);
+
+
+}
+
+void init_coq_stack()
+{
+  coq_stack_low = (value *) coq_stat_alloc(Coq_stack_size);
+  coq_stack_high = coq_stack_low + Coq_stack_size / sizeof (value);
+  coq_stack_threshold = coq_stack_low + Coq_stack_threshold / sizeof(value);
+  coq_max_stack_size = Coq_max_stack_size;
+}  
+
+void init_coq_global_data(long requested_size)
+{
+  int i;
+  
+  coq_global_data = alloc_shr(requested_size, 0);
+  for (i = 0; i < requested_size; i++) 
+    Field (coq_global_data, i) = Val_unit;
+  
+  default_transp = BOXED;
+
+  coq_global_transp = alloc_shr(requested_size, 0);
+  for (i = 0; i < requested_size; i++) 
+    Field (coq_global_transp, i) = Val_unit;
+  
+  coq_global_boxed = alloc_shr(requested_size, 0);
+  for (i = 0; i < requested_size; i++) 
+    Field (coq_global_boxed, i) = Val_unit;
+}
+
+void init_coq_atom_tbl(long requested_size){
+  int i;
+  coq_atom_tbl = alloc_shr(requested_size, 0);
+  for (i = 0; i < requested_size; i++) Field (coq_atom_tbl, i) = Val_unit;
+}
+
+void init_coq_interpreter()
+{
+  coq_sp = coq_stack_high;
+  coq_interprete(NULL, Val_unit, Val_unit, 0);
+}
+
+static int coq_vm_initialized = 0;
+
+value init_coq_vm(value unit) /* ML */
+{
+  int i;
+  if (coq_vm_initialized == 1) {
+    fprintf(stderr,"already open \n");fflush(stderr);}
+  else {
+
+    /* Allocate the table of global and the stack */
+    init_coq_stack();
+    init_coq_global_data(Coq_global_data_Size);
+    init_coq_atom_tbl(40);
+    /* Initialing the interpreter */
+    forcable = Val_true;
+    init_coq_interpreter();
+    
+    /* Some predefined pointer code */
+    accumulate = (code_t) coq_stat_alloc(sizeof(opcode_t));
+    *accumulate = ACCUMULATE;
+    accumulate = 
+      (code_t) coq_tcode_of_code((value)accumulate, Val_int(sizeof(opcode_t))); 
+
+  /* Initialize GC */
+    if (coq_prev_scan_roots_hook == NULL)
+      coq_prev_scan_roots_hook = scan_roots_hook;
+    scan_roots_hook = coq_scan_roots;
+    coq_vm_initialized = 1;
+  } 
+  return Val_unit;;
+}
+
+void realloc_coq_stack(asize_t required_space)
+{
+  asize_t size;
+  value * new_low, * new_high, * new_sp;
+  value * p;
+  size = coq_stack_high - coq_stack_low;
+  do {
+    size *= 2;
+  } while (size < coq_stack_high - coq_sp + required_space);
+  new_low = (value *) coq_stat_alloc(size * sizeof(value));
+  new_high = new_low + size;
+
+#define shift(ptr) \
+    ((char *) new_high - ((char *) coq_stack_high - (char *) (ptr)))
+
+  new_sp = (value *) shift(coq_sp);
+  memmove((char *) new_sp,
+        (char *) coq_sp,
+        (coq_stack_high - coq_sp) * sizeof(value));
+  coq_stat_free(coq_stack_low);
+  coq_stack_low = new_low;
+  coq_stack_high = new_high;
+  coq_stack_threshold = coq_stack_low + Coq_stack_threshold / sizeof(value);
+  coq_sp = new_sp;
+#undef shift
+}
+
+value get_coq_global_data(value unit)                /* ML */
+{
+  return coq_global_data;
+}
+
+value get_coq_atom_tbl(value unit)                  /* ML */
+{
+  return coq_atom_tbl;
+}
+
+value get_coq_global_transp(value unit)             /* ML */
+{
+  return coq_global_transp;
+}
+
+value get_coq_global_boxed(value unit)        /* ML */
+{
+  return coq_global_boxed;
+}
+
+value realloc_coq_global_data(value size)           /* ML */
+{
+  mlsize_t requested_size, actual_size, i;
+  value new_global_data;
+  requested_size = Long_val(size);
+  actual_size = Wosize_val(coq_global_data);
+  if (requested_size >= actual_size) {
+    requested_size = (requested_size + 0x100) & 0xFFFFFF00;
+    new_global_data = alloc_shr(requested_size, 0);
+    for (i = 0; i < actual_size; i++)
+      initialize(&Field(new_global_data, i), Field(coq_global_data, i));
+    for (i = actual_size; i < requested_size; i++){
+      Field (new_global_data, i) = Val_long (0);
+    }
+    coq_global_data = new_global_data;
+  }
+  return Val_unit;
+}
+
+value realloc_coq_global_boxed(value size)           /* ML */
+{
+  mlsize_t requested_size, actual_size, i;
+  value new_global_transp, new_global_boxed;
+  requested_size = Long_val(size);
+  actual_size = Wosize_val(coq_global_transp);
+  if (requested_size >= actual_size) {
+    requested_size = (requested_size + 0x100) & 0xFFFFFF00;
+    new_global_transp = alloc_shr(requested_size, 0);
+    new_global_boxed = alloc_shr(requested_size, 0);
+    for (i = 0; i < actual_size; i++){
+      initialize(&Field(new_global_transp, i), Field(coq_global_transp, i));
+      initialize(&Field(new_global_boxed, i), 
+		 Field(coq_global_boxed, i));
+    }
+    for (i = actual_size; i < requested_size; i++){
+      Field (new_global_transp, i) = Val_long (0);
+      Field (new_global_boxed, i) = Val_long (0);
+    }
+    coq_global_transp = new_global_transp;
+    coq_global_boxed = new_global_boxed;
+  }
+  return Val_unit;
+}
+
+value realloc_coq_atom_tbl(value size)            /* ML */
+{
+  mlsize_t requested_size, actual_size, i;
+  value new_atom_tbl;
+  requested_size = Long_val(size);
+  actual_size = Wosize_val(coq_atom_tbl);
+  if (requested_size >= actual_size) {
+    requested_size = (requested_size + 0x100) & 0xFFFFFF00;
+    new_atom_tbl = alloc_shr(requested_size, 0);
+    for (i = 0; i < actual_size; i++)
+      initialize(&Field(new_atom_tbl, i), Field(coq_atom_tbl, i));
+    for (i = actual_size; i < requested_size; i++){
+      Field (new_atom_tbl, i) = Val_long (0);
+    }
+    coq_atom_tbl = new_atom_tbl;
+  }
+  return Val_unit;
+}
+
+value swap_coq_global_transp (value unit){
+  if (default_transp==BOXED) default_transp = TRANSP;
+  else default_transp = BOXED;
+  return Val_unit;
+}
+
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
new file mode 100644
index 0000000000..0884f06a86
--- /dev/null
+++ b/kernel/byterun/coq_memory.h
@@ -0,0 +1,68 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#ifndef _COQ_MEMORY_
+#define _COQ_MEMORY_
+
+#include "config.h"
+#include "fail.h"
+#include "misc.h"
+#include "memory.h"
+#include "mlvalues.h"
+
+
+#define Coq_stack_size (4096 * sizeof(value))
+#define Coq_stack_threshold (256 * sizeof(value))
+#define Coq_global_data_Size (4096 * sizeof(value))
+#define Coq_max_stack_size (256 * 1024)
+
+#define TRANSP 0
+#define BOXED 1
+
+/* stack */
+
+extern value * coq_stack_low;
+extern value * coq_stack_high;
+extern value * coq_stack_threshold;
+
+/* global_data */
+
+extern value coq_global_data;
+extern value coq_global_transp;
+extern value coq_global_boxed;
+extern int default_transp;
+extern value coq_atom_tbl;
+/* interp state */
+
+extern value * coq_sp;
+extern value forcable;
+/* Some predefined pointer code */ 
+extern code_t accumulate;
+
+/* functions over global environment */
+
+value coq_static_alloc(value size);  /* ML */
+value coq_static_free(value string); /* ML */
+
+value init_coq_vm(value unit); /* ML */
+value re_init_coq_vm(value unit); /* ML */
+
+void  realloc_coq_stack(asize_t required_space); 
+value get_coq_global_data(value unit); /* ML */
+value realloc_coq_global_data(value size); /* ML */
+value get_coq_global_transp(value unit); /* ML */
+value get_coq_global_boxed(value unit);
+value realloc_coq_global_boxed(value size); /* ML */
+value get_coq_atom_tbl(value unit); /* ML */
+value realloc_coq_atom_tbl(value size); /* ML */
+
+#endif /* _COQ_MEMORY_ */
+
+
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
new file mode 100644
index 0000000000..baf3ab0903
--- /dev/null
+++ b/kernel/byterun/coq_values.c
@@ -0,0 +1,69 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#include <stdio.h>
+#include "coq_fix_code.h"
+#include "coq_instruct.h"
+#include "coq_memory.h"
+#include "coq_values.h"
+#include "memory.h"
+/* KIND OF VALUES */
+
+#define Setup_for_gc
+#define Restore_after_gc
+
+value coq_kind_of_closure(value v) {
+  opcode_t * c;
+  int res;
+  int is_app = 0;
+  c = Code_val(v);
+  if (Is_instruction(c, GRAB)) return Val_int(0);
+  if (Is_instruction(c, RESTART)) {is_app = 1; c++;}
+  if (Is_instruction(c, GRABREC)) return Val_int(1+is_app);
+  if (Is_instruction(c, COGRAB)) return Val_int(3+is_app);
+  if (Is_instruction(c, MAKEACCU)) return Val_int(5);
+  return Val_int(0);
+}
+
+
+/* DESTRUCT ACCU */
+
+value coq_closure_arity(value clos) {
+  opcode_t * c = Code_val(clos);
+  if (Is_instruction(c,RESTART)) {
+    c++;
+    if (Is_instruction(c,GRAB)) return Val_int(3 + c[1] - Wosize_val(clos));
+    else { 
+      if (Wosize_val(clos) != 2) failwith("Coq Values : coq_closure_arity");
+      return Val_int(1);
+    }
+  }
+  if (Is_instruction(c,GRAB)) return Val_int(1 + c[1]);
+  return Val_int(1);
+}
+
+/* Fonction sur les  fix */
+
+value coq_offset(value v) {
+  if (Tag_val(v) == Closure_tag) return Val_int(0);
+  else return Val_long(-Wsize_bsize(Infix_offset_val(v)));
+}
+
+value coq_offset_closure(value v, value offset){
+  return (value)&Field(v, Int_val(offset));
+}
+
+value coq_offset_tcode(value code,value offset){
+  return((value)((code_t)code + Int_val(offset)));
+}
+
+value coq_int_tcode(value code, value offset) {
+  return Val_int(*((code_t) code + Int_val(offset)));
+}
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
new file mode 100644
index 0000000000..a186d62aa6
--- /dev/null
+++ b/kernel/byterun/coq_values.h
@@ -0,0 +1,28 @@
+/***********************************************************************/
+/*                                                                     */
+/*                           Coq Compiler                              */
+/*                                                                     */
+/*        Benjamin Gregoire, projets Logical and Cristal               */
+/*                        INRIA Rocquencourt                           */
+/*                                                                     */
+/*                                                                     */
+/***********************************************************************/
+
+#ifndef _COQ_VALUES_
+#define _COQ_VALUES_
+
+#include "alloc.h"
+#include "mlvalues.h"
+
+#define ATOM_FIX_TAG 3
+#define ATOM_SWITCH_TAG 4
+
+#define Accu_tag 0
+#define Default_tag 0
+
+/* Les blocs accumulate */
+#define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
+
+#endif /* _COQ_VALUES_ */
+
+
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
new file mode 100644
index 0000000000..48331a6870
--- /dev/null
+++ b/kernel/cbytecodes.ml
@@ -0,0 +1,64 @@
+open Names
+open Term
+
+type tag = int 
+
+type structured_constant =
+  | Const_sorts of sorts
+  | Const_ind of inductive
+  | Const_b0 of tag                
+  | Const_bn of tag * structured_constant array
+
+type reloc_table = (tag * int) array 
+
+type annot_switch = 
+   {ci : case_info; rtbl : reloc_table; tailcall : bool}
+ 
+module Label = 
+  struct
+    type t = int
+    let no = -1
+    let counter = ref no
+    let create () = incr counter; !counter
+    let reset_label_counter () = counter := no 
+  end
+
+
+type instruction =
+  | Klabel of Label.t
+  | Kacc of int
+  | Kenvacc of int
+  | Koffsetclosure of int
+  | Kpush
+  | Kpop of int
+  | Kpush_retaddr of Label.t
+  | Kapply of int                       (*  number of arguments *)
+  | Kappterm of int * int               (* number of arguments, slot size *)
+  | Kreturn of int                      (* slot size *)
+  | Kjump
+  | 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 *)
+  | 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 
+  | Kstop
+  | Ksequence of bytecodes * bytecodes
+
+and bytecodes = instruction list
+
+type fv_elem = FVnamed of identifier | FVrel of int
+
+type fv = fv_elem array
+
+
+
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
new file mode 100644
index 0000000000..84882358ad
--- /dev/null
+++ b/kernel/cbytecodes.mli
@@ -0,0 +1,60 @@
+open Names
+open Term
+
+type tag = int 
+
+type structured_constant =
+  | Const_sorts of sorts
+  | Const_ind of inductive
+  | Const_b0 of tag                
+  | Const_bn of tag * structured_constant array
+
+type reloc_table = (tag * int) array 
+
+type annot_switch = 
+   {ci : case_info; rtbl : reloc_table; tailcall : bool}
+
+module Label : 
+  sig
+    type t = int
+    val no : t
+    val create : unit -> t
+    val reset_label_counter : unit -> unit
+  end 
+
+type instruction =
+  | Klabel of Label.t
+  | Kacc of int
+  | Kenvacc of int
+  | Koffsetclosure of int
+  | Kpush
+  | Kpop of int
+  | Kpush_retaddr of Label.t
+  | Kapply of int                       (*  number of arguments *)
+  | Kappterm of int * int               (* number of arguments, slot size *)
+  | Kreturn of int                      (* slot size *)
+  | Kjump
+  | 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 *)
+  | 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 
+  | Kstop
+  | Ksequence of bytecodes * bytecodes
+
+and bytecodes = instruction list
+
+type fv_elem = FVnamed of identifier | FVrel of int
+
+type fv = fv_elem array
+
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
new file mode 100644
index 0000000000..033f073190
--- /dev/null
+++ b/kernel/cbytegen.ml
@@ -0,0 +1,483 @@
+open Util
+open Names
+open Cbytecodes
+open Cemitcodes
+open Term
+open Declarations
+open Environ
+
+(*i Compilation des variables + calcul des variables libres *)
+
+(* Representation des environnements machines :                       *)
+(*[t0|C0| ... |tc|Cc| ... |t(nbr-1)|C(nbr-1)| fv1 | fv1 | .... | fvn] *)
+(*               ^<----------offset--------->                         *)
+
+
+type fv = fv_elem list
+
+type vm_env = {size : int; fv_rev : fv}
+    (* size = n;   fv_rev = [fvn; ... ;fv1] *)
+         
+type t = {
+    nb_stack : int;        (* nbre de variables sur la pile *)
+    in_stack : int list;   (* position dans la pile *)
+    nb_rec : int;          (* nbre de fonctions mutuellement recursives = 
+			                                              nbr *)
+    pos_rec : int;         (* position de la fonction courante = c *)
+    offset : int;          
+    in_env : vm_env ref
+  }	
+
+let empty_fv = {size= 0; fv_rev = []}
+
+let fv r = !(r.in_env)
+
+(* [add_param n] rend la liste [sz+1;sz+2;...;sz+n] *)
+let rec add_param n sz l =
+  if n = 0 then l else add_param (n - 1) sz (n+sz::l) 
+
+(* [push_param ] ajoute les parametres de fonction dans la pile *)
+let push_param n sz r =
+  { r with
+    nb_stack = r.nb_stack + n;
+    in_stack = add_param n sz r.in_stack }
+
+(* [push_local e sz] ajoute une nouvelle variable dans la pile a la position *)
+let push_local sz r = 
+  { r with 
+    nb_stack = r.nb_stack + 1;
+    in_stack = (sz + 1) :: r.in_stack }
+
+
+(* Table de relocation initiale *)
+let empty () = 
+  { nb_stack = 0; in_stack = [];
+    nb_rec = 0;pos_rec = 0;
+    offset = 0; in_env = ref empty_fv }
+
+let init_fun arity = 
+  { nb_stack = arity; in_stack = add_param arity 0 [];
+    nb_rec = 0; pos_rec = 0;
+    offset = 1; in_env = ref empty_fv } 
+
+let init_type ndef rfv =
+  { nb_stack = 0; in_stack = [];
+    nb_rec = 0; pos_rec = 0;
+    offset = 2*(ndef-1)+1; in_env = rfv }
+
+let init_fix ndef pos_rec arity rfv =
+  { nb_stack = arity; in_stack = add_param arity 0 [];
+    nb_rec = ndef; pos_rec = pos_rec;
+    offset = 2 * (ndef - pos_rec - 1)+1; in_env = rfv} 
+
+let find_at el l = 
+  let rec aux n = function
+    | [] -> raise Not_found
+    | hd :: tl -> if hd = el then n else aux (n+1) tl
+  in aux 1 l
+
+let pos_named id r =
+  let env = !(r.in_env) in
+  let cid = FVnamed id in
+  try Kenvacc(r.offset + env.size - (find_at cid env.fv_rev))
+  with Not_found ->
+    let pos = env.size in
+    r.in_env := { size = pos+1; fv_rev =  cid:: env.fv_rev};
+    Kenvacc (r.offset + pos)
+
+let pos_rel i r sz = 
+  if i <= r.nb_stack then
+    Kacc(sz - (List.nth r.in_stack (i-1)))
+  else if i <= r.nb_stack + r.nb_rec 
+  then Koffsetclosure (2 * (r.nb_rec + r.nb_stack - r.pos_rec - i))
+  else 
+    let db = FVrel(i - r.nb_stack - r.nb_rec) in
+    let env = !(r.in_env) in
+    try Kenvacc(r.offset + env.size - (find_at db env.fv_rev))
+    with Not_found ->
+      let pos = env.size in
+      r.in_env := { size = pos+1; fv_rev =  db:: env.fv_rev};
+      Kenvacc(r.offset + pos)
+
+
+(*i  Examination of the continuation *)
+
+(* Discard all instructions up to the next label.
+   This function is to be applied to the continuation before adding a
+   non-terminating instruction (branch, raise, return, appterm)
+   in front of it. *)
+
+let rec discard_dead_code cont = cont
+(*function
+    [] -> []
+  | (Klabel _ | Krestart ) :: _ as cont -> cont
+  | _ :: cont -> discard_dead_code cont
+*)
+
+(* Return a label to the beginning of the given continuation.
+   If the sequence starts with a branch, use the target of that branch
+   as the label, thus avoiding a jump to a jump. *)
+
+let label_code = function
+  | Klabel lbl :: _ as cont -> (lbl, cont)
+  | cont -> let lbl = Label.create() in (lbl, Klabel lbl :: cont)
+
+(* Return a branch to the continuation. That is, an instruction that,
+   when executed, branches to the continuation or performs what the
+   continuation performs. We avoid generating branches to returns. *)
+
+let make_branch cont =
+  match cont with
+  | (Kreturn _ as return) :: _ -> return, cont
+  | Klabel lbl as b :: _ -> b, cont
+  | _ -> let b = Klabel(Label.create()) in b,b::cont
+
+(* Check if we're in tailcall position *)
+
+let rec is_tailcall = function
+  | Kreturn k :: _ -> Some k
+  | Klabel _ :: c -> is_tailcall c
+  | _ -> None
+
+(* Extention of the continuation ****)
+	
+(* Add a Kpop n instruction in front of a continuation *)
+let rec add_pop n = function
+  | Kpop m :: cont -> add_pop (n+m) cont
+  | Kreturn m:: cont -> Kreturn (n+m) ::cont
+  | cont -> if n = 0 then cont else Kpop n :: cont
+
+let add_grab arity lbl cont =
+  if arity = 1 then Klabel lbl :: cont
+  else Krestart :: Klabel lbl :: Kgrab (arity - 1) :: cont
+ 
+
+(* Environnement global *****)
+
+let global_env = ref empty_env
+
+let set_global_env env = global_env := env
+
+
+(* Code des fermetures ****)
+let fun_code = ref []
+
+let init_fun_code () = fun_code := []
+
+(* Compilation des constructeurs et des inductifs *)
+
+(* Inv : nparam + arity > 0 *)
+let code_construct tag nparams arity cont =
+  let f_cont =
+      add_pop nparams
+      (if arity = 0 then 
+	[Kconst (Const_b0 tag); Kreturn 0]
+       else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0])
+    in 
+    let lbl = Label.create() in
+    fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)];
+    Kclosure(lbl,0) :: cont
+
+type block = 
+  | Bconstr of constr
+  | Bstrconst of structured_constant
+  | Bmakeblock of int * block array
+  | Bconstruct_app of int * int * int * block array
+                  (* tag , nparams, arity *)
+
+let get_strcst = function
+  | Bstrconst sc -> sc
+  | _ -> raise Not_found 
+
+let rec str_const c =
+  match kind_of_term c with
+  | Sort s -> Bstrconst (Const_sorts s)
+  | Cast(c,_) -> str_const c 
+  | App(f,args) -> 
+      begin
+	match kind_of_term f with
+	| Construct((kn,j),i) -> 
+	    let oib = (lookup_mind kn !global_env).mind_packets.(j) in
+	    let num,arity = oib.mind_reloc_tbl.(i-1) in
+	    let nparams = oib.mind_nparams in
+	    if nparams + arity = Array.length args then
+	    if arity = 0 then Bstrconst(Const_b0 num)
+	    else
+	      let rargs = Array.sub args nparams arity in
+	      let b_args = Array.map str_const rargs in
+	      try 
+		let sc_args = Array.map get_strcst b_args in
+		Bstrconst(Const_bn(num, sc_args))
+	      with Not_found ->
+		Bmakeblock(num,b_args)
+	    else  
+	    let b_args = Array.map str_const args in
+	    Bconstruct_app(num, nparams, arity, b_args)
+	| _ -> Bconstr c
+      end
+  | Ind ind -> Bstrconst (Const_ind ind)
+  | Construct ((kn,j),i) ->  
+      let oib = (lookup_mind kn !global_env).mind_packets.(j) in
+      let num,arity = oib.mind_reloc_tbl.(i-1) in
+      let nparams = oib.mind_nparams in
+      if nparams + arity = 0 then Bstrconst(Const_b0 num)
+      else Bconstruct_app(num,nparams,arity,[||])
+  | _ -> Bconstr c
+
+(* compilation des applications *)
+let comp_args comp_expr reloc args sz cont =
+  let nargs_m_1 = Array.length args - 1 in  
+  let c = ref (comp_expr reloc args.(0) (sz + nargs_m_1) cont) in
+  for i = 1 to nargs_m_1 do
+    c := comp_expr reloc args.(i) (sz + nargs_m_1 - i) (Kpush :: !c)
+  done; 
+  !c
+  
+let comp_app comp_fun comp_arg reloc f args sz cont =
+  let nargs = Array.length args in
+  match is_tailcall cont with
+  | Some k -> 
+      comp_args comp_arg reloc args sz
+	(Kpush ::
+	 comp_fun reloc f (sz + nargs)
+	   (Kappterm(nargs, k + nargs) :: (discard_dead_code cont)))
+  | None ->
+      if nargs < 4 then
+	comp_args comp_arg reloc args sz
+	  (Kpush :: (comp_fun reloc f (sz+nargs) (Kapply nargs :: cont)))
+      else 
+	let lbl,cont1 = label_code cont in
+	Kpush_retaddr lbl ::
+	(comp_args comp_arg reloc args (sz + 3)
+	   (Kpush :: (comp_fun reloc f (sz+3+nargs) (Kapply nargs :: cont1))))
+
+(* Compilation des variables libres *)
+  
+let compile_fv_elem reloc fv sz cont =
+  match fv with
+  | FVrel i -> pos_rel i reloc sz :: cont
+  | FVnamed id -> pos_named id reloc :: cont
+
+(* compilation des constantes *)
+
+let rec get_allias env kn =
+  let tps = (lookup_constant kn env).const_body_code in
+  match Cemitcodes.force tps with
+  | BCallias kn' -> get_allias env kn'
+  | _ -> kn
+
+(* compilation des expressions *)
+ 
+let rec compile_constr reloc c sz cont =
+  match kind_of_term c with
+  | Meta _ -> raise (Invalid_argument "Cbytegen.gen_lam : Meta")
+  | Evar _ -> raise (Invalid_argument "Cbytegen.gen_lam : Evar")
+ 
+  | Cast(c,_) -> compile_constr reloc c sz cont
+
+  | Rel i -> pos_rel i reloc sz :: cont
+  | Var id -> pos_named id reloc :: cont
+  | Const kn -> Kgetglobal (get_allias !global_env kn) :: cont
+  
+  | Sort _  | Ind _ | Construct _ ->
+      compile_str_cst reloc (str_const c) sz cont
+  
+  | LetIn(_,xb,_,body) ->
+      compile_constr reloc xb sz 
+	(Kpush :: 
+	(compile_constr (push_local sz reloc) body (sz+1) (add_pop 1 cont)))
+  | Prod(id,dom,codom) ->
+      let cont1 = 
+	Kpush :: compile_constr reloc dom (sz+1) (Kmakeprod :: cont) in
+      compile_constr reloc (mkLambda(id,dom,codom)) sz cont1
+  | Lambda _ ->
+      let params, body = decompose_lam c in
+      let arity = List.length params in
+      let r_fun = init_fun arity in
+      let lbl_fun = Label.create() in
+      let cont_fun = 
+	compile_constr r_fun body arity [Kreturn arity] in
+      fun_code := [Ksequence(add_grab arity lbl_fun cont_fun,!fun_code)];
+      let fv = fv r_fun in
+      compile_fv reloc fv.fv_rev sz (Kclosure(lbl_fun,fv.size) :: cont)
+ 
+  | App(f,args) -> 
+      begin 
+	match kind_of_term f with
+	| Construct _ -> compile_str_cst reloc (str_const c) sz cont
+	| _ -> comp_app compile_constr compile_constr reloc f args sz cont 
+      end
+  | Fix ((rec_args,init),(_,type_bodies,rec_bodies)) ->
+      let ndef = Array.length type_bodies in
+      let rfv = ref empty_fv in
+      let lbl_types = Array.create ndef Label.no in
+      let lbl_bodies = Array.create ndef Label.no in
+      (* Compilation des types *)
+      let rtype = init_type ndef rfv in
+      for i = 0 to ndef - 1 do
+	let lbl,fcode = 
+	  label_code 
+	    (compile_constr rtype type_bodies.(i) 0 [Kstop]) in 
+	lbl_types.(i) <- lbl; 
+	fun_code := [Ksequence(fcode,!fun_code)]
+      done;
+      (* Compilation des corps *)
+      for i = 0 to ndef - 1 do
+	let params,body = decompose_lam rec_bodies.(i) in
+	let arity = List.length params in
+	let rbody = init_fix ndef i arity rfv in
+	let cont1 = 
+	  compile_constr rbody body arity [Kreturn arity] in
+	let lbl = Label.create () in
+	lbl_bodies.(i) <- lbl;
+	let fcode =  
+	  if arity = 1 then 
+	    Klabel lbl :: Kgrabrec 0 :: Krestart :: cont1
+	  else
+	    Krestart :: Klabel lbl :: Kgrabrec rec_args.(i) ::
+	    Krestart :: Kgrab (arity - 1) :: cont1
+	in
+	fun_code := [Ksequence(fcode,!fun_code)]
+      done;
+      let fv = !rfv in
+      compile_fv reloc fv.fv_rev sz 
+	(Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont)
+  
+  | CoFix(init,(_,type_bodies,rec_bodies)) ->
+      let ndef = Array.length type_bodies in
+      let rfv = ref empty_fv in
+      let lbl_types = Array.create ndef Label.no in
+      let lbl_bodies = Array.create ndef Label.no in
+      (* Compilation des types *)
+      let rtype = init_type ndef rfv in
+      for i = 0 to ndef - 1 do
+	let lbl,fcode = 
+	  label_code 
+	    (compile_constr rtype type_bodies.(i) 0 [Kstop]) in
+	lbl_types.(i) <- lbl; 
+	fun_code := [Ksequence(fcode,!fun_code)]
+      done;
+      (* Compilation des corps *)
+      for i = 0 to ndef - 1 do
+	let params,body = decompose_lam rec_bodies.(i) in
+	let arity = List.length params in
+	let rbody = init_fix ndef i arity rfv in
+	let lbl = Label.create () in
+
+	let cont1 = 
+	  compile_constr rbody body arity [Kreturn(arity)] in
+	let cont2 = 
+	  if arity <= 1 then cont1 else Kgrab (arity - 1) :: cont1 in
+	let cont3 = 
+	  Krestart :: Klabel lbl :: Kcograb arity :: Krestart :: cont2 in
+	fun_code := [Ksequence(cont3,!fun_code)];
+	lbl_bodies.(i) <- lbl
+      done;
+      let fv = !rfv in
+      compile_fv reloc fv.fv_rev sz 
+	(Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont)
+  
+  | Case(ci,t,a,branchs) ->
+      let ind = ci.ci_ind in
+      let mib = lookup_mind (fst ind) !global_env in
+      let oib = mib.mind_packets.(snd ind) in
+      let tbl = oib.mind_reloc_tbl in
+      let lbl_consts = Array.create oib.mind_nb_constant Label.no in
+      let lbl_blocks = Array.create (oib.mind_nb_args+1) Label.no in
+      let branch1,cont = make_branch cont in
+      (* Compilation du type *)
+      let lbl_typ,fcode = 	
+	label_code (compile_constr reloc t sz [Kpop sz; Kstop])
+      in fun_code := [Ksequence(fcode,!fun_code)];
+      (* Compilation des branches *) 
+      let lbl_sw = Label.create () in
+      let sz_b,branch,is_tailcall =
+	match branch1 with 
+	| Kreturn k -> assert (k = sz); sz, branch1, true
+	| _ -> sz+3, Kjump, false
+      in
+      let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in
+     (* Compilation de la branche accumulate *)
+      let lbl_accu, code_accu = 
+	label_code(Kmakeswitchblock(lbl_typ,lbl_sw,annot,sz) :: branch::cont) 
+      in
+      lbl_blocks.(0) <- lbl_accu;
+      let c = ref code_accu in
+      (* Compilation des branches constructeurs *)
+      for i = 0 to Array.length tbl - 1 do
+	let tag, arity = tbl.(i) in
+	if arity = 0 then
+	  let lbl_b,code_b = 
+	    label_code(compile_constr reloc branchs.(i) sz_b (branch :: !c)) in
+	  lbl_consts.(tag) <- lbl_b; 
+	  c := code_b
+	else 
+	  let args, body = decompose_lam branchs.(i) in
+	  let nargs = List.length args in
+	  let lbl_b,code_b = 
+	    label_code(
+	    if nargs = arity then
+	      Kpushfield arity ::
+	      compile_constr (push_param arity sz_b reloc)
+		body (sz_b+arity) (add_pop arity (branch :: !c))
+	    else
+	      let sz_appterm = if is_tailcall then sz_b + arity else arity in
+	      Kpushfield arity :: 
+	      compile_constr reloc branchs.(i) (sz_b+arity)
+		(Kappterm(arity,sz_appterm) :: !c))
+	  in
+	  lbl_blocks.(tag) <- lbl_b;
+	  c := code_b
+      done;
+      c :=  Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
+      let code_sw = 
+	match branch1 with
+	| Klabel lbl -> Kpush_retaddr lbl ::  !c
+	| _ -> !c 
+      in
+      let cont_a = if mib.mind_finite then code_sw else Kforce :: code_sw in
+      compile_constr reloc a sz cont_a 
+ 
+and compile_fv reloc l sz cont =
+  match l with
+  | [] -> cont
+  | [fvn] -> compile_fv_elem reloc fvn sz cont
+  | fvn :: tl ->
+      compile_fv_elem reloc fvn sz 
+	(Kpush :: compile_fv reloc tl (sz + 1) cont)
+      
+and compile_str_cst reloc sc sz cont =
+  match sc with
+  | Bconstr c -> compile_constr reloc c sz cont
+  | Bstrconst sc -> Kconst sc :: cont
+  | Bmakeblock(tag,args) ->
+      let nargs = Array.length args in
+      comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont)
+  | Bconstruct_app(tag,nparams,arity,args) ->
+      if args = [||] then code_construct tag nparams arity cont
+      else
+	comp_app 
+	  (fun _ _ _ cont -> code_construct tag nparams arity cont) 
+	  compile_str_cst reloc () args sz cont
+      
+let compile env c =
+  set_global_env env;
+  init_fun_code ();
+  Label.reset_label_counter ();
+  let reloc = empty () in
+  let init_code = compile_constr reloc c 0 [Kstop] in
+  let fv = List.rev (!(reloc.in_env).fv_rev) in
+  init_code,!fun_code, Array.of_list fv
+
+let compile_constant_body env kn body opaque boxed =
+  if opaque then BCconstant
+  else match body with
+  | None -> BCconstant
+  | Some sb ->
+      let body = Declarations.force sb in
+      match kind_of_term body with
+      | Const kn' -> BCallias (get_allias env kn')
+      | _ -> 
+	  let to_patch = to_memory (compile env body) in
+	  BCdefined (boxed,to_patch)
+
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
new file mode 100644
index 0000000000..407edea442
--- /dev/null
+++ b/kernel/cbytegen.mli
@@ -0,0 +1,16 @@
+open Names
+open Cbytecodes
+open Cemitcodes 
+open Term
+open Declarations
+open Environ
+
+
+
+val compile : env -> constr -> bytecodes * bytecodes * fv
+                              (* init, fun, fv *)
+
+val compile_constant_body : 
+    env -> constant -> constr_substituted option -> bool -> bool -> body_code
+                                              (* opaque *) (* boxed *)
+
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
new file mode 100644
index 0000000000..ab1f00d110
--- /dev/null
+++ b/kernel/cemitcodes.ml
@@ -0,0 +1,339 @@
+open Names
+open Term
+open Cbytecodes
+open Copcodes
+
+(* Relocation information *)
+type reloc_info =
+  | Reloc_annot of annot_switch 
+  | Reloc_const of structured_constant
+  | Reloc_getglobal of constant
+
+type patch = reloc_info * int 
+
+let patch_int buff pos n =
+  String.unsafe_set buff pos (Char.unsafe_chr n);
+  String.unsafe_set buff (pos + 1) (Char.unsafe_chr (n asr 8));
+  String.unsafe_set buff (pos + 2) (Char.unsafe_chr (n asr 16));
+  String.unsafe_set buff (pos + 3) (Char.unsafe_chr (n asr 24))
+
+let cGETGLOBALBOXED = Char.unsafe_chr opGETGLOBALBOXED
+let cGETGLOBAL = Char.unsafe_chr opGETGLOBAL
+
+let cPUSHGETGLOBALBOXED = Char.unsafe_chr opPUSHGETGLOBALBOXED
+let cPUSHGETGLOBAL = Char.unsafe_chr opPUSHGETGLOBAL
+
+let is_PUSHGET c =
+ c = cPUSHGETGLOBAL || c = cPUSHGETGLOBALBOXED
+
+let patch_getglobal buff pos (boxed,n) =
+ let posinstr = pos - 4 in
+ let c = String.unsafe_get buff posinstr in
+ begin match is_PUSHGET c, boxed with
+ | true, true -> String.unsafe_set buff posinstr cPUSHGETGLOBALBOXED
+ | true, false -> String.unsafe_set buff posinstr cPUSHGETGLOBAL
+ | false, true -> String.unsafe_set buff posinstr cGETGLOBALBOXED
+ | false,false -> String.unsafe_set buff posinstr cGETGLOBAL
+ end;
+ patch_int buff pos n
+ 
+(* Buffering of bytecode *)
+
+let out_buffer = ref(String.create 1024)
+and out_position = ref 0
+
+let out_word b1 b2 b3 b4 =
+  let p = !out_position in
+  if p >= String.length !out_buffer then begin
+    let len = String.length !out_buffer in
+    let new_buffer = String.create (2 * len) in
+    String.blit !out_buffer 0 new_buffer 0 len;
+    out_buffer := new_buffer
+  end;
+  String.unsafe_set !out_buffer p (Char.unsafe_chr b1);
+  String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2);
+  String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
+  String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
+  out_position := p + 4
+
+let out opcode =
+  out_word opcode 0 0 0
+
+let out_int n =
+  out_word n (n asr 8) (n asr 16) (n asr 24)
+
+(* Handling of local labels and backpatching *)
+
+type label_definition =
+    Label_defined of int
+  | Label_undefined of (int * int) list
+
+let label_table  = ref ([| |] : label_definition array)
+(* le ieme element de la table = Label_defined n signifie que l'on a 
+   deja rencontrer le label i et qu'il est a l'offset n.
+                               = Label_undefined l signifie que l'on a 
+   pas encore rencontrer ce label, le premier entier indique ou est l'entier 
+   a patcher dans la string, le deuxieme son origine  *)
+
+let extend_label_table needed =
+  let new_size = ref(Array.length !label_table) in
+  while needed >= !new_size do new_size := 2 * !new_size done;
+  let new_table = Array.create !new_size (Label_undefined []) in
+  Array.blit !label_table 0 new_table 0 (Array.length !label_table);
+  label_table := new_table
+
+let backpatch (pos, orig) =
+  let displ = (!out_position - orig) asr 2 in
+  !out_buffer.[pos] <- Char.unsafe_chr displ;
+  !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8);
+  !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16);
+  !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24)
+
+let define_label lbl =
+  if lbl >= Array.length !label_table then extend_label_table lbl;
+  match (!label_table).(lbl) with
+    Label_defined _ ->
+      raise(Failure "CEmitcode.define_label")
+  | Label_undefined patchlist ->
+      List.iter backpatch patchlist;
+      (!label_table).(lbl) <- Label_defined !out_position
+
+let out_label_with_orig orig lbl =
+  if lbl >= Array.length !label_table then extend_label_table lbl;
+  match (!label_table).(lbl) with
+    Label_defined def ->
+      out_int((def - orig) asr 2)
+  | Label_undefined patchlist ->
+      if patchlist = [] then
+	(!label_table).(lbl) <-
+          Label_undefined((!out_position, orig) :: patchlist);
+      out_int 0
+
+let out_label l = out_label_with_orig !out_position l
+
+(* Relocation information *)
+
+let reloc_info = ref ([] : (reloc_info * int) list)
+
+let enter info =
+  reloc_info := (info, !out_position) :: !reloc_info
+
+let slot_for_const c =
+  enter (Reloc_const c);
+  out_int 0
+
+and slot_for_annot a =
+  enter (Reloc_annot a);
+  out_int 0
+
+and slot_for_getglobal id =
+  enter (Reloc_getglobal id);
+  out_int 0
+
+
+(* Emission of one instruction *)
+
+
+let emit_instr = function
+  | Klabel lbl -> define_label lbl
+  | Kacc n ->
+      if n < 8 then out(opACC0 + n) else (out opACC; out_int n)
+  | Kenvacc n ->
+      if n >= 1 && n <= 4
+      then out(opENVACC1 + n - 1)
+      else (out opENVACC; out_int n)
+  | Koffsetclosure ofs ->
+      if ofs = -2 || ofs = 0 || ofs = 2
+      then out (opOFFSETCLOSURE0 + ofs / 2)
+      else (out opOFFSETCLOSURE; out_int ofs)
+  | Kpush ->      
+      out opPUSH
+  | Kpop n ->      
+      out opPOP; out_int n
+  | Kpush_retaddr lbl -> 
+      out opPUSH_RETADDR; out_label lbl
+  | Kapply n ->
+      if n < 4 then out(opAPPLY1 + n - 1) else (out opAPPLY; out_int n)
+  | Kappterm(n, sz) ->
+      if n < 4 then (out(opAPPTERM1 + n - 1); out_int sz)
+               else (out opAPPTERM; out_int n; out_int sz)
+  | Kreturn n ->
+      out opRETURN; out_int n
+  | Kjump ->
+      out opRETURN; out_int 0
+  | Krestart ->
+      out opRESTART
+  | Kgrab n -> 
+      out opGRAB; out_int n
+  | Kgrabrec(rec_arg) -> 
+      out opGRABREC; out_int rec_arg
+  | Kcograb n -> 
+      out opCOGRAB; out_int n
+  | Kclosure(lbl, n) -> 
+      out opCLOSURE; out_int n; out_label lbl
+  | Kclosurerec(nfv,init,lbl_types,lbl_bodies) ->
+      out opCLOSUREREC;out_int (Array.length lbl_bodies);
+      out_int nfv; out_int init;
+      let org = !out_position in
+      Array.iter (out_label_with_orig org) lbl_types;
+      let org = !out_position in
+      Array.iter (out_label_with_orig org) lbl_bodies
+  | Kgetglobal q -> 
+      out opGETGLOBAL; slot_for_getglobal q
+  | Kconst((Const_b0 i)) -> 
+      if i >= 0 && i <= 3
+          then out (opCONST0 + i)
+          else (out opCONSTINT; out_int i) 
+  | Kconst c ->
+      out opGETGLOBAL; slot_for_const c
+  | Kmakeblock(n, t) ->
+      if n = 0 then raise (Invalid_argument "emit_instr : block size = 0")
+      else if n < 4 then (out(opMAKEBLOCK1 + n - 1); out_int t)
+      else (out opMAKEBLOCK; out_int n; out_int t)
+  | Kmakeprod ->
+      out opMAKEPROD
+  | Kmakeswitchblock(typlbl,swlbl,annot,sz) ->
+      out opMAKESWITCHBLOCK;
+      out_label typlbl; out_label swlbl;
+      slot_for_annot annot;out_int sz
+  | Kforce -> 
+      out opFORCE
+  | Kswitch (tbl_const, tbl_block) ->
+      out opSWITCH;
+      out_int (Array.length tbl_const + (Array.length tbl_block lsl 16));
+      let org = !out_position in
+      Array.iter (out_label_with_orig org) tbl_const;
+      Array.iter (out_label_with_orig org) tbl_block
+  | Kpushfield n ->
+      out opPUSHFIELD;out_int n
+  | Kstop -> 
+      out opSTOP
+  | Ksequence _ -> raise (Invalid_argument "Cemitcodes.emit_instr")
+
+(* Emission of a list of instructions. Include some peephole optimization. *)
+
+let rec emit = function
+  | [] -> ()
+  (* Peephole optimizations *)
+  | Kpush :: Kacc n :: c ->
+      if n < 8 then out(opPUSHACC0 + n) else (out opPUSHACC; out_int n);
+      emit c
+  | Kpush :: Kenvacc n :: c -> 
+      if n >= 1 && n <= 4
+      then out(opPUSHENVACC1 + n - 1)
+      else (out opPUSHENVACC; out_int n);
+      emit c
+  | Kpush :: Koffsetclosure ofs :: c -> 
+      if ofs = -2 || ofs = 0 || ofs = 2
+      then out(opPUSHOFFSETCLOSURE0 + ofs / 2)
+      else (out opPUSHOFFSETCLOSURE; out_int ofs);
+      emit c
+  | Kpush :: Kgetglobal id :: c ->
+      out opPUSHGETGLOBAL; slot_for_getglobal id; emit c 
+  | Kpush :: Kconst (Const_b0 i) :: c -> 
+      if i >= 0 && i <= 3
+      then out (opPUSHCONST0 + i)
+      else (out opPUSHCONSTINT; out_int i);
+      emit c
+  | Kpush :: Kconst const :: c ->
+      out opPUSHGETGLOBAL; slot_for_const const;
+      emit c 
+  | Kpop n :: Kjump :: c ->
+      out opRETURN; out_int n; emit c
+  | Ksequence(c1,c2)::c ->
+      emit c1; emit c2;emit c
+  (* Default case *)
+  | instr :: c ->
+      emit_instr instr; emit c
+
+(* Initialization *)
+
+let init () =
+  out_position := 0;
+  label_table := Array.create 16 (Label_undefined []);
+  reloc_info := []
+
+type emitcodes = string
+
+let length = String.length
+
+type to_patch = emitcodes * (patch list) * fv
+
+(* Substitution *)
+let rec subst_strcst s sc =
+  match sc with
+  | Const_sorts _ | Const_b0 _ -> sc
+  | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
+  | Const_ind(ind) -> let kn,i = ind in Const_ind((subst_kn s kn, i))
+
+let subst_patch s (ri,pos) = 
+  match ri with
+  | Reloc_annot a ->
+      let (kn,i) = a.ci.ci_ind in
+      let ci = {a.ci with ci_ind = (subst_kn s kn,i)} in
+      (Reloc_annot {a with ci = ci},pos)
+  | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
+  | Reloc_getglobal kn -> (Reloc_getglobal (subst_kn s kn), pos)
+
+let subst_to_patch s (code,pl,fv) = code,List.map (subst_patch s) pl,fv
+
+type body_code =
+  | BCdefined of bool * to_patch
+  | BCallias of constant
+  | BCconstant
+
+let subst_body_code s = function
+  | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp)
+  | BCallias kn -> BCallias (subst_kn s kn)
+  | BCconstant -> BCconstant
+
+type to_patch_substituted = body_code substituted
+
+let from_val = from_val
+
+let force = force subst_body_code
+
+let subst_to_patch_subst = subst_substituted 
+
+let is_boxed tps =
+  match force tps with
+  | BCdefined(b,_) -> b
+  | _ -> false
+
+let to_memory (init_code, fun_code, fv) =
+  init();
+  emit init_code;
+  emit fun_code;
+  let code = String.create !out_position in
+  String.unsafe_blit !out_buffer 0 code 0 !out_position;
+  let reloc = List.rev !reloc_info in
+  Array.iter (fun lbl -> 
+    (match lbl with
+      Label_defined _ -> assert true
+    | Label_undefined patchlist -> 
+	assert (patchlist = []))) !label_table;
+  (code, reloc, fv)
+
+
+
+
+
+
+
+(* Code pour la machine virtuelle *)
+let mkAccu_code n =
+  init ();
+  out opMAKEACCU; out_int n;
+  let code = String.create !out_position in
+  String.unsafe_blit !out_buffer 0 code 0 !out_position; 
+  code
+
+let mkPopStop_code n =
+  init();
+  if n = 0 then out opSTOP
+  else (out opPOP; out_int n; out opSTOP);
+  let code = String.create !out_position in
+  String.unsafe_blit !out_buffer 0 code 0 !out_position; 
+  code
+
+    
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
new file mode 100644
index 0000000000..fed577158a
--- /dev/null
+++ b/kernel/cemitcodes.mli
@@ -0,0 +1,41 @@
+open Names
+open Cbytecodes
+
+type reloc_info =
+  | Reloc_annot of annot_switch 
+  | Reloc_const of structured_constant
+  | Reloc_getglobal of constant
+
+type patch = reloc_info * int 
+(* A virer *)
+val subst_patch : substitution -> patch -> patch
+ 
+type emitcodes 
+
+val length : emitcodes -> int 
+
+val patch_int : emitcodes -> (*pos*)int -> int -> unit
+val patch_getglobal : emitcodes -> (*pos*)int -> (bool*int) -> unit
+
+type to_patch = emitcodes * (patch list) * fv
+
+val subst_to_patch : substitution -> to_patch -> to_patch
+
+type body_code =
+  | BCdefined of bool*to_patch
+  | BCallias of constant
+  | BCconstant
+
+
+type to_patch_substituted 
+
+val from_val : body_code -> to_patch_substituted 
+
+val force : to_patch_substituted -> body_code
+
+val is_boxed : to_patch_substituted -> bool
+
+val subst_to_patch_subst : substitution -> to_patch_substituted -> to_patch_substituted
+
+val to_memory : bytecodes * bytecodes * fv -> to_patch
+               (* init code, fun code, fv *) 
diff --git a/kernel/closure.ml b/kernel/closure.ml
index f4db948a02..51c355c9a1 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -16,7 +16,6 @@ open Declarations
 open Environ
 open Esubst
 
-
 let stats = ref false
 let share = ref true
 
@@ -52,8 +51,6 @@ let with_stats c =
   end else
     Lazy.force c
 
-type transparent_state = Idpred.t * KNpred.t
-
 let all_opaque = (Idpred.empty, KNpred.empty)
 let all_transparent = (Idpred.full, KNpred.full)
 
@@ -326,11 +323,7 @@ fin obsolčte **************)
  * instantiations (cbv or lazy) are.
  *)
 
-type table_key =
-  | ConstKey of constant
-  | VarKey of identifier
-  | FarRelKey of int
-   (* FarRel: index in the rel_context part of _initial_ environment *)
+type table_key = id_key
 
 type 'a infos = {
   i_flags : reds;
@@ -349,7 +342,7 @@ let ref_value_cache info ref =
   try
     let body =
       match ref with
-	| FarRelKey n ->
+	| RelKey n ->
 	    let (s,l) = info.i_rels in lift n (List.assoc (s-n) l)
 	| VarKey id -> List.assoc id info.i_vars
 	| ConstKey cst -> constant_value info.i_env cst
@@ -573,7 +566,7 @@ let clos_rel e i =
     | Inl(n,mt) -> lift_fconstr n mt
     | Inr(k,None) -> {norm=Norm; term= FRel k}
     | Inr(k,Some p) ->
-        lift_fconstr (k-p) {norm=Norm;term=FFlex(FarRelKey p)}
+        lift_fconstr (k-p) {norm=Norm;term=FFlex(RelKey p)}
 
 (* since the head may be reducible, we might introduce lifts of 0 *)
 let compact_stack head stk =
@@ -730,7 +723,7 @@ let mk_clos2 = mk_clos_deep mk_clos
 let rec to_constr constr_fun lfts v =
   match v.term with
     | FRel i -> mkRel (reloc_rel i lfts)
-    | FFlex (FarRelKey p) -> mkRel (reloc_rel p lfts)
+    | FFlex (RelKey p) -> mkRel (reloc_rel p lfts)
     | FFlex (VarKey x) -> mkVar x
     | FAtom c ->
         (match kind_of_term c with
@@ -1023,8 +1016,8 @@ let rec knr info m stk =
       (match ref_value_cache info (VarKey id) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
-  | FFlex(FarRelKey k) when red_set info.i_flags fDELTA ->
-      (match ref_value_cache info (FarRelKey k) with
+  | FFlex(RelKey k) when red_set info.i_flags fDELTA ->
+      (match ref_value_cache info (RelKey k) with
           Some v -> kni info v stk
         | None -> (set_norm m; (m,stk)))
   | FConstruct(ind,c) when red_set info.i_flags fIOTA ->
diff --git a/kernel/closure.mli b/kernel/closure.mli
index e0cfe7b51a..dae1689419 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -27,7 +27,7 @@ val with_stats: 'a Lazy.t -> 'a
   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of 
   a LetIn expression is Letin reduction *)
 
-type transparent_state = Idpred.t * KNpred.t
+
 
 val all_opaque      : transparent_state
 val all_transparent : transparent_state
@@ -82,13 +82,8 @@ val betadeltaiotanolet : reds
 
 val unfold_red : evaluable_global_reference -> reds
 
-(************************************************************************)
-
-type table_key =
-  | ConstKey of constant
-  | VarKey of identifier
-  | FarRelKey of int
-   (* FarRel: index in the [rel_context] part of {\em initial} environment *)
+(***********************************************************************)
+type table_key = id_key
 
 type 'a infos
 val ref_value_cache: 'a infos -> table_key -> 'a option
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 11d4435c2f..1504220ac4 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -9,7 +9,6 @@
 (* $Id$ *)
 
 open Names
-open Closure
 
 (* Opaque constants *)
 let cst_transp = ref KNpred.full
@@ -31,13 +30,13 @@ let is_opaque_var kn = not (Idpred.mem kn !var_transp)
 let is_opaque = function
   | ConstKey cst -> is_opaque_cst cst
   | VarKey id -> is_opaque_var id
-  | FarRelKey _ -> false
+  | RelKey _ -> false
 
 (* Unfold the first only if it is not opaque and the second is opaque *)
 let oracle_order k1 k2 = is_opaque k2 & not (is_opaque k1)
 
 (* summary operations *)
-
+type transparent_state = Idpred.t * KNpred.t
 let init() = (cst_transp := KNpred.full; var_transp := Idpred.full)
 let freeze () = (!var_transp, !cst_transp)
 let unfreeze (vo,co) = (cst_transp := co; var_transp := vo)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 8dad2e2bdb..351df9d86a 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -9,13 +9,13 @@
 (* $Id$ *)
 
 open Names
-open Closure
+
 
 (* Order on section paths for unfolding.
    If [oracle_order kn1 kn2] is true, then unfold kn1 first.
    Note: the oracle does not introduce incompleteness, it only
    tries to postpone unfolding of "opaque" constants. *)
-val oracle_order : table_key -> table_key -> bool
+val oracle_order : 'a tableKey -> 'a tableKey -> bool
 
 (* Changing the oracle *)
 val set_opaque_const      : kernel_name -> unit
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index c37c81cf60..5c058b4661 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -169,4 +169,5 @@ let cook_constant env r =
       cb.const_hyps
       ~init:empty_named_context in
   let body,typ = abstract_constant r.d_abstract hyps (body,typ) in
-  (body, typ, cb.const_constraints, cb.const_opaque)
+  let boxed = Cemitcodes.is_boxed cb.const_body_code in
+  (body, typ, cb.const_constraints, cb.const_opaque, boxed)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 7bd64d3267..289373eff8 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -32,7 +32,8 @@ type recipe = {
   d_modlist : work_list }
 
 val cook_constant :
-  env -> recipe -> constr_substituted option * constr * constraints * bool
+  env -> recipe -> 
+    constr_substituted option * constr * constraints * bool * bool
 
 (*s Utility functions used in module [Discharge]. *)
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
new file mode 100644
index 0000000000..3cc6f49d56
--- /dev/null
+++ b/kernel/csymtable.ml
@@ -0,0 +1,163 @@
+open Names
+open Term
+open Vm
+open Cemitcodes
+open Cbytecodes
+open Declarations
+open Environ
+open Cbytegen
+open Cemitcodes
+
+external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
+external free_tcode : tcode -> unit = "coq_static_free"
+external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
+ 
+(*******************)
+(* Linkage du code *)
+(*******************)
+
+(* Table des globaux *)
+
+(* [global_data] contient les valeurs des constantes globales 
+   (axiomes,definitions), les annotations des switch et les structured 
+   constant *)
+external global_data : unit -> values array = "get_coq_global_data"
+
+(* [realloc_global_data n] augmente de n la taille de [global_data] *)
+external realloc_global_data : int -> unit = "realloc_coq_global_data"
+
+let check_global_data n =
+  if n >= Array.length (global_data()) then realloc_global_data n
+  
+let num_global = ref 0
+
+let set_global v = 
+  let n = !num_global in
+  check_global_data n;
+  (global_data()).(n) <- v;
+  incr num_global;
+  n
+
+(* [global_transp],[global_boxed] contiennent les valeurs des 
+   definitions gelees. Les deux versions sont maintenues en //. 
+   [global_transp] contient la version transparente.
+   [global_boxed] contient la version gelees. *)
+
+external global_transp : unit -> values array = "get_coq_global_transp"
+external global_boxed : unit -> values array = "get_coq_global_boxed"
+
+(* [realloc_global_data n] augmente de n la taille de [global_data] *)
+external realloc_global_boxed : int -> unit = "realloc_coq_global_boxed"
+
+let check_global_boxed n =
+  if n >= Array.length (global_boxed()) then realloc_global_boxed n
+  
+let num_boxed = ref 0
+
+let set_boxed kn v = 
+  let n = !num_boxed in
+  check_global_boxed n;
+  (global_transp()).(n) <- v;
+  let vb = val_of_constant_def kn v in
+  (global_boxed()).(n) <- vb;
+  incr num_boxed;
+  n
+
+(* table pour les structured_constant et les annotations des switchs *)
+
+let str_cst_tbl = Hashtbl.create 31
+    (* (structured_constant * int) Hashtbl.t*)
+
+let annot_tbl = Hashtbl.create 31
+    (* (annot_switch * int) Hashtbl.t  *)
+
+(************************)
+(* traduction des patch *)
+
+(* slot_for_*, calcul la valeur de l'objet, la place
+   dans la table global, rend sa position dans la table *)
+ 
+let slot_for_str_cst key =
+  try Hashtbl.find str_cst_tbl key 
+  with Not_found -> 
+    let n = set_global (val_of_str_const key) in
+    Hashtbl.add str_cst_tbl key n;
+    n
+
+let slot_for_annot key =
+  try Hashtbl.find annot_tbl key 
+  with Not_found -> 
+    let n =  set_global (Obj.magic key) in
+    Hashtbl.add annot_tbl key n;
+    n
+
+let rec slot_for_getglobal env kn =
+  let ck = lookup_constant_key kn env in
+  try constant_key_pos ck
+  with NotEvaluated ->
+    match force (constant_key_body ck).const_body_code with
+    | BCdefined(boxed,(code,pl,fv)) -> 
+	let v = eval_to_patch env (code,pl,fv) in
+   	let pos = 
+	  if boxed then set_boxed kn v 
+	  else set_global v in
+	let bpos = boxed,pos in
+	set_pos_constant ck bpos;
+	bpos
+    | BCallias kn' ->
+	let bpos = slot_for_getglobal env kn' in
+	set_pos_constant ck bpos;
+	bpos
+    | BCconstant -> 
+	let v = val_of_constant kn in
+	let pos = set_global v in
+	let bpos = false,pos in
+	set_pos_constant ck bpos;
+	bpos  
+
+and slot_for_fv env fv=
+  match fv with
+  | FVnamed id -> 
+      let nv = lookup_namedval id env in
+      begin
+	match kind_of_named nv with
+	| VKvalue v -> v
+	| VKaxiom id ->
+	    let v = val_of_named id in
+	    set_namedval nv v; v
+	| VKdef(c,e) ->
+	    let v = val_of_constr e c in
+	    set_namedval nv v; v
+      end
+  | FVrel i ->
+      let rv = lookup_relval i env in
+      begin
+	match kind_of_rel rv with
+	| VKvalue v -> v
+	| VKaxiom k ->
+	    let v = val_of_rel k in
+	    set_relval rv v; v
+	| VKdef(c,e) ->
+	    let v = val_of_constr e c in
+	    let k = nb_rel e in
+	    set_relval rv v; v
+      end
+ 
+and eval_to_patch env (buff,pl,fv) = 
+  let patch = function
+    | Reloc_annot a, pos -> patch_int buff pos (slot_for_annot a)
+    | Reloc_const sc, pos -> patch_int buff pos (slot_for_str_cst sc)
+    | Reloc_getglobal kn, pos -> 
+	patch_getglobal buff pos (slot_for_getglobal env kn)
+  in 
+  List.iter patch pl;
+  let nfv = Array.length fv in
+  let vm_env = Array.map (slot_for_fv env) fv in 
+  let tc = tcode_of_code buff (length buff) in
+  eval_tcode tc vm_env
+
+and val_of_constr env c = 
+  let (_,fun_code,_ as ccfv) = compile env c in
+  eval_to_patch env (to_memory ccfv)
+ 
+  
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
new file mode 100644
index 0000000000..8bb0b890c8
--- /dev/null
+++ b/kernel/csymtable.mli
@@ -0,0 +1,6 @@
+open Names
+open Term
+open Environ
+
+val val_of_constr : env -> constr -> values 
+
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 152c1e5bf8..b5505bce35 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -21,33 +21,22 @@ open Sign
 
 (*s Constants (internal representation) (Definition/Axiom) *)
 
-type subst_internal = 
-  | Constr of constr 
-  | LazyConstr of substitution * constr
+type constr_substituted = constr substituted
 
-type constr_substituted = subst_internal ref
+let from_val = from_val
 
-let from_val c = ref (Constr c)
+let force = force subst_mps 
 
-let force cs = match !cs with
-    Constr c -> c
-  | LazyConstr (subst,c) -> 
-      let c' = subst_mps subst c in
-	cs := Constr c';
-	c'
-
-let subst_constr_subst subst cs = match !cs with
-    Constr c -> ref (LazyConstr (subst,c))
-  | LazyConstr (subst',c) -> 
-      let subst'' = join subst' subst in
-	ref (LazyConstr (subst'',c))
+let subst_constr_subst = subst_substituted
 
 type constant_body = {
-  const_hyps : section_context; (* New: younger hyp at top *)
-  const_body : constr_substituted option;
-  const_type : types;
-  const_constraints : constraints;
-  const_opaque : bool }
+    const_hyps : section_context; (* New: younger hyp at top *)
+    const_body : constr_substituted option;
+    const_type : types;  
+    const_body_code : Cemitcodes.to_patch_substituted;
+   (* const_type_code : Cemitcodes.to_patch; *)
+    const_constraints : constraints;
+    const_opaque : bool }
 
 (*s Inductive types (internal representation with redundant
     information). *)
@@ -89,38 +78,43 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
    inductives *) 
 
 type one_inductive_body = {
-  mind_typename : identifier;
-  mind_nparams : int;
-  mind_params_ctxt : rel_context;
-  mind_nrealargs : int;
-  mind_nf_arity : types;
-  mind_user_arity : types;
-  mind_sort : sorts;
-  mind_kelim : sorts_family list;
-  mind_consnames : identifier array;
-  mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *)
-  mind_user_lc : types array;
-  mind_recargs : wf_paths;
- }
+    mind_typename : identifier;
+    mind_nparams : int;
+    mind_params_ctxt : rel_context;
+    mind_nrealargs : int;
+    mind_nf_arity : types;
+    mind_user_arity : types;
+    mind_sort : sorts;
+    mind_kelim : sorts_family list;
+    mind_consnames : identifier array;
+    mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *)
+    mind_user_lc : types array;
+    mind_recargs : wf_paths;
+    mind_nb_constant : int; (* number of constant constructor *)
+    mind_nb_args : int; (* number of no constant constructor *)
+    mind_reloc_tbl :  Cbytecodes.reloc_table; 
+  }
 
 type mutual_inductive_body = {
-  mind_record : bool;
-  mind_finite : bool;
-  mind_ntypes : int;
-  mind_hyps : section_context;
-  mind_packets : one_inductive_body array;
-  mind_constraints : constraints;
-  mind_equiv : kernel_name option
- }
+    mind_record : bool;
+    mind_finite : bool;
+    mind_ntypes : int;
+    mind_hyps : section_context;
+    mind_packets : one_inductive_body array;
+    mind_constraints : constraints;
+    mind_equiv : kernel_name option
+  }
 
 (* TODO: should be changed to non-coping after Term.subst_mps *)
-let subst_const_body sub cb = 
-  { const_body = option_app (subst_constr_subst sub) cb.const_body;
-    const_type = type_app (Term.subst_mps sub) cb.const_type;
+let subst_const_body sub cb = {
     const_hyps = (assert (cb.const_hyps=[]); []);
+    const_body = option_app (subst_constr_subst sub) cb.const_body;
+    const_type = type_app (Term.subst_mps sub) cb.const_type;
+    const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
+    (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
     const_constraints = cb.const_constraints;
-    const_opaque = cb.const_opaque}
-  
+    const_opaque = cb.const_opaque } 
+
 let subst_mind_packet sub mbp = 
   { mind_consnames = mbp.mind_consnames;
     mind_typename = mbp.mind_typename;
@@ -136,8 +130,11 @@ let subst_mind_packet sub mbp =
     mind_nparams = mbp.mind_nparams;
     mind_params_ctxt = 
       map_rel_context (Term.subst_mps sub) mbp.mind_params_ctxt;
-    mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*);
-}
+    mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); 
+    mind_nb_constant = mbp.mind_nb_constant;
+    mind_nb_args = mbp.mind_nb_args;
+    mind_reloc_tbl = mbp.mind_reloc_tbl }
+
 
 let subst_mind sub mib = 
   { mind_record = mib.mind_record ; 
@@ -146,8 +143,7 @@ let subst_mind sub mib =
     mind_hyps = (assert (mib.mind_hyps=[]); []) ;
     mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ;
     mind_constraints = mib.mind_constraints ;
-    mind_equiv = option_app (subst_kn sub) mib.mind_equiv;
-}
+    mind_equiv = option_app (subst_kn sub) mib.mind_equiv }
 
 
 (*s Modules: signature component specifications, module types, and
@@ -171,7 +167,6 @@ and module_specification_body =
       msb_equiv : module_path option; 
       msb_constraints : constraints }
 
-
 type structure_elem_body = 
   | SEBconst of constant_body
   | SEBmind of mutual_inductive_body
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index a168abdfb2..50c8660143 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -12,6 +12,7 @@
 open Names
 open Univ
 open Term
+open Cemitcodes
 open Sign
 (*i*)
 
@@ -27,11 +28,13 @@ val from_val : constr -> constr_substituted
 val force : constr_substituted -> constr
 
 type constant_body = {
-  const_hyps : section_context; (* New: younger hyp at top *)
-  const_body : constr_substituted option;
-  const_type : types;
-  const_constraints : constraints;
-  const_opaque : bool }
+    const_hyps : section_context; (* New: younger hyp at top *)
+    const_body : constr_substituted option;
+    const_type : types;  
+    const_body_code : to_patch_substituted;
+   (* const_type_code : to_patch;*)
+    const_constraints : constraints;
+    const_opaque : bool }
 
 val subst_const_body : substitution -> constant_body -> constant_body
 
@@ -62,29 +65,34 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
    inductives *) 
 
 type one_inductive_body = {
-  mind_typename : identifier;
-  mind_nparams : int;
-  mind_params_ctxt : rel_context;
-  mind_nrealargs : int;
-  mind_nf_arity : types;
-  mind_user_arity : types;
-  mind_sort : sorts;
-  mind_kelim : sorts_family list;
-  mind_consnames : identifier array;
-  mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *)
-  mind_user_lc : types array;
-  mind_recargs : wf_paths;
- }
+    mind_typename : identifier;
+    mind_nparams : int;
+    mind_params_ctxt : rel_context;
+    mind_nrealargs : int;
+    mind_nf_arity : types;
+    mind_user_arity : types;
+    mind_sort : sorts;
+    mind_kelim : sorts_family list;
+    mind_consnames : identifier array;
+    mind_nf_lc : types array; (* constrs and arity with pre-expanded ccl *)
+    mind_user_lc : types array;
+    mind_recargs : wf_paths;
+    mind_nb_constant : int; (* number of constant constructor *)
+    mind_nb_args : int; (* number of no constant constructor *)
+    mind_reloc_tbl :  Cbytecodes.reloc_table; 
+  }
+
+
 
 type mutual_inductive_body = {
-  mind_record : bool;
-  mind_finite : bool;
-  mind_ntypes : int;
-  mind_hyps : section_context;
-  mind_packets : one_inductive_body array;
-  mind_constraints : constraints;
-  mind_equiv : kernel_name option;
- }
+    mind_record : bool; 
+    mind_finite : bool;
+    mind_ntypes : int;
+    mind_hyps : section_context;
+    mind_packets : one_inductive_body array;
+    mind_constraints : constraints;
+    mind_equiv : kernel_name option;
+  }
 
 
 val subst_mind : substitution -> mutual_inductive_body -> mutual_inductive_body
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 4d485ff8cc..504c11fdfb 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -59,7 +59,8 @@ type mutual_inductive_entry = {
 type definition_entry = {
   const_entry_body   : constr;
   const_entry_type   : types option;
-  const_entry_opaque : bool }
+  const_entry_opaque : bool;
+  const_entry_boxed  : bool}
 
 type parameter_entry = types
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 4d485ff8cc..4b4cee03ab 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -59,7 +59,8 @@ type mutual_inductive_entry = {
 type definition_entry = {
   const_entry_body   : constr;
   const_entry_type   : types option;
-  const_entry_opaque : bool }
+  const_entry_opaque : bool;
+  const_entry_boxed  : bool }
 
 type parameter_entry = types
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 41b664309d..3563a13400 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -23,10 +23,13 @@ type compilation_unit_name = dir_path * checksum
 
 type global = Constant | Inductive
 
+type key = (bool*int) option ref 
+type constant_key = constant_body * key
+ 
 type engagement = ImpredicativeSet
 
 type globals = {
-  env_constants : constant_body KNmap.t;
+  env_constants : constant_key KNmap.t;
   env_inductives : mutual_inductive_body KNmap.t;
   env_modules : module_body MPmap.t;
   env_modtypes : module_type_body KNmap.t }
@@ -36,10 +39,20 @@ type stratification = {
   env_engagement : engagement option
 }
 
-type env = {
-  env_globals        : globals;
-  env_named_context  : named_context;
-  env_rel_context    : rel_context;
+type 'a val_kind =   
+  | VKvalue of values
+  | VKaxiom of 'a
+  | VKdef of constr * env
+
+and 'a lazy_val = 'a val_kind ref
+
+and env = {
+  env_globals       : globals;
+  env_named_context : named_context;
+  env_named_val     : (identifier * (identifier lazy_val)) list;
+  env_rel_context   : rel_context;
+  env_rel_val       : inv_rel_key lazy_val list;
+  env_nb_rel        : int;
   env_stratification : stratification }
 
 let empty_env = { 
@@ -49,11 +62,16 @@ let empty_env = {
     env_modules = MPmap.empty;
     env_modtypes = KNmap.empty };
   env_named_context = empty_named_context;
+  env_named_val = [];
   env_rel_context = empty_rel_context;
+  env_rel_val = [];
+  env_nb_rel = 0;
   env_stratification = {
     env_universes = initial_universes;
     env_engagement = None } }
 
+
+
 let engagement env = env.env_stratification.env_engagement
 let universes env = env.env_stratification.env_universes
 let named_context env = env.env_named_context
@@ -63,6 +81,9 @@ let empty_context env =
   env.env_rel_context = empty_rel_context 
   && env.env_named_context = empty_named_context
 
+exception NotEvaluated 
+exception AllReadyEvaluated
+
 (* Rel context *)
 let lookup_rel n env =
   Sign.lookup_rel n env.env_rel_context
@@ -75,68 +96,135 @@ let evaluable_rel n env =
   with Not_found -> 
     false
 
+let nb_rel env = env.env_nb_rel
+
 let push_rel d env =
+  let _,body,_ = d in
+  let rval =
+    match body with
+    | None -> ref (VKaxiom env.env_nb_rel)
+    | Some c -> ref (VKdef(c,env))
+  in     
   { env with
-      env_rel_context = add_rel_decl d env.env_rel_context }
+    env_rel_context = add_rel_decl d env.env_rel_context;
+    env_rel_val = rval :: env.env_rel_val;
+    env_nb_rel = env.env_nb_rel + 1 }
+ 
 
 let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x
+    
 let push_rec_types (lna,typarray,_) env =
   let ctxt =
     array_map2_i
       (fun i na t -> (na, None, type_app (lift i) t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
-
+    
 let reset_rel_context env =
   { env with
-      env_rel_context = empty_rel_context }
+    env_rel_context = empty_rel_context;
+    env_rel_val = [];
+    env_nb_rel = 0 }
 
 let fold_rel_context f env ~init =
   snd (Sign.fold_rel_context
 	 (fun d (env,e) -> (push_rel d env, f env d e))
          (rel_context env) ~init:(reset_rel_context env,init))
-
-
+    
+(* Abstract machine rel values *)
+type relval = int lazy_val
+      
+let kind_of_rel r = !r
+    
+let set_relval r v =
+  match !r with
+  | VKvalue _ -> raise AllReadyEvaluated
+  | _ -> r := VKvalue v
+	
+let lookup_relval n env =
+  try List.nth env.env_rel_val (n - 1)
+  with _ -> raise Not_found
+      
 (* Named context *)
 let lookup_named id env =
   Sign.lookup_named id env.env_named_context
+    
 
-(* A local const is evaluable if it is defined and not opaque *)
+    
+(* A local const is evaluable if it is defined  *)
 let evaluable_named id env =
   try 
     match lookup_named id env with
-        (_,Some _,_) -> true
-      | _ -> false
+      (_,Some _,_) -> true
+    | _ -> false
   with Not_found -> 
     false
-
-let push_named d env =
-  { env with
-      env_named_context = Sign.add_named_decl d env.env_named_context }
+      
+let push_named d env = 
+  let id,body,_ = d in
+  let rval =
+    match body with
+    | None -> ref (VKaxiom id)
+    | Some c -> ref (VKdef(c,env))
+  in
+  { env with  
+    env_named_context = Sign.add_named_decl d env.env_named_context;
+    env_named_val =  (id,rval):: env.env_named_val }
 
 let reset_context env =
   { env with
-      env_named_context = empty_named_context;
-      env_rel_context = empty_rel_context }
+    env_named_context = empty_named_context;
+    env_named_val = [];
+    env_rel_context = empty_rel_context;
+    env_rel_val = [];
+    env_nb_rel = 0 }
 
 let reset_with_named_context ctxt env =
-  { env with
-      env_named_context = ctxt;
-      env_rel_context = empty_rel_context }
-
+  Sign.fold_named_context push_named ctxt ~init:(reset_context env)
+    
 let fold_named_context f env ~init =
   snd (Sign.fold_named_context
 	 (fun d (env,e) -> (push_named d env, f env d e))
          (named_context env) ~init:(reset_context env,init))
-
+    
 let fold_named_context_reverse f ~init env =
   Sign.fold_named_context_reverse f ~init:init (named_context env) 
-
+    
+(* Abstract machine values of local vars referred by names *)
+type namedval = identifier lazy_val
+
+let kind_of_named r = !r
+
+let set_namedval r v =
+  match !r with
+  | VKvalue _ -> raise AllReadyEvaluated
+  | _ -> r := VKvalue v
+	
+let lookup_namedval id env =
+  snd (List.find (fun (id',_) -> id = id') env.env_named_val)
+  
 (* Global constants *)
-let lookup_constant kn env =
+
+let notevaluated = None
+    
+let constant_key_pos (cb,r) =
+  match !r with
+  | None -> raise NotEvaluated
+  | Some key -> key
+
+let constant_key_body = fst 
+
+let set_pos_constant (cb,r) bpos =
+  if !r = notevaluated then r := Some bpos 
+  else raise AllReadyEvaluated
+
+let lookup_constant_key kn env =
   KNmap.find kn env.env_globals.env_constants
 
-let add_constant kn cb env =
-  let new_constants = KNmap.add kn cb env.env_globals.env_constants in
+let lookup_constant kn env = constant_key_body (lookup_constant_key kn env)
+
+let add_constant kn cs env =
+  let new_constants = 
+    KNmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in
   let new_globals = 
     { env.env_globals with 
 	env_constants = new_constants } in 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 71fc8e6d8a..d570655ee6 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -22,7 +22,9 @@ open Sign
 
 (* Environments have the following components:
    - a context for de Bruijn variables
+   - a context for de Bruijn variables vm values
    - a context for section variables and goal assumptions
+   - a context for section variables and goal assumptions vm values 
    - a context for global constants and axioms
    - a context for inductive definitions
    - a set of universe constraints
@@ -54,6 +56,18 @@ val push_rec_types   : rec_declaration -> env -> env
 val lookup_rel    : int -> env -> rel_declaration
 val evaluable_rel : int -> env -> bool
 
+(* Abstract machine rel values *)
+type 'a val_kind =   
+  | VKvalue of values
+  | VKaxiom of 'a
+  | VKdef of constr * env
+
+type relval
+
+val kind_of_rel : relval -> inv_rel_key val_kind
+val set_relval : relval -> values -> unit
+val lookup_relval : int -> env -> relval
+val nb_rel : env -> int
 (*s Recurrence on [rel_context] *)
 val fold_rel_context :
   (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
@@ -67,6 +81,13 @@ val push_named : named_declaration -> env -> env
 val lookup_named    : variable -> env -> named_declaration
 val evaluable_named : variable -> env -> bool
 
+(* Abstract machine values of local vars referred by names *)
+type namedval
+
+val kind_of_named : namedval -> identifier val_kind
+val set_namedval : namedval -> values -> unit
+val lookup_namedval : identifier -> env -> namedval
+ 
 (*s Recurrence on [named_context]: older declarations processed first *)
 val fold_named_context :
   (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
@@ -87,6 +108,15 @@ val add_constant : constant -> constant_body -> env -> env
 
 (* Looks up in the context of global constant names *)
 (* raises [Not_found] if the required path is not found *)
+type constant_key 
+exception NotEvaluated
+exception AllReadyEvaluated
+
+val constant_key_pos : constant_key -> bool*int  
+val constant_key_body : constant_key -> constant_body
+val set_pos_constant : constant_key -> (bool*int) -> unit
+
+val lookup_constant_key : constant -> env -> constant_key
 val lookup_constant    : constant -> env -> constant_body
 val evaluable_constant : constant -> env -> bool
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index dbf7bc58e0..5f9f907f52 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -511,6 +511,19 @@ let build_inductive env env_ar record finite inds recargs cst =
     (* Elimination sorts *)
     let isunit = isunit && ntypes = 1 && (not (is_recursive recargs.(0))) in
     let kelim = allowed_sorts env issmall isunit ar_sort in
+    let nconst, nblock = ref 0, ref 0 in 
+    let transf num =
+      let arity = List.length (dest_subterms recarg).(num) in
+      if arity = 0 then 
+	let p  = (!nconst, 0) in
+	incr nconst; p
+      else 
+	let p = (!nblock + 1, arity) in
+	incr nblock; p
+     (* les tag des constructeur constant commence a 0,
+	les tag des constructeur non constant a 1 (0 => accumulator) *)
+    in 
+    let rtbl = Array.init (List.length cnames) transf in
     (* Build the inductive packet *)
     { mind_typename = id;
       mind_nparams = nparamargs;
@@ -523,7 +536,10 @@ let build_inductive env env_ar record finite inds recargs cst =
       mind_consnames = Array.of_list cnames;
       mind_user_lc = lc;
       mind_nf_lc = nf_lc;
-      mind_recargs = recarg;
+      mind_recargs = recarg;    
+      mind_nb_constant = !nconst;
+      mind_nb_args = !nblock;
+      mind_reloc_tbl = rtbl;
     } in
   let packets = array_map2 build_one_packet inds recargs in
   (* Build the mutual inductive *)
diff --git a/kernel/make-opcodes b/kernel/make-opcodes
new file mode 100644
index 0000000000..c8f573c682
--- /dev/null
+++ b/kernel/make-opcodes
@@ -0,0 +1,2 @@
+$1=="enum" {n=0; next; }
+           {for (i = 1; i <= NF; i++) {printf("let op%s = %d\n", $i, n++);}}
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index a96bc52fce..a3639ef988 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -145,7 +145,7 @@ and translate_entry_list env msid is_definition sig_e =
     let kn = make_kn mp empty_dirpath l in
     match e with
       | SPEconst ce ->
-	  let cb = translate_constant env ce in
+	  let cb = translate_constant env kn ce in
 	    begin match cb.const_hyps with
 	      |	(_::_) -> error_local_context (Some l)
 	      | [] ->
diff --git a/kernel/names.ml b/kernel/names.ml
index 68622703d6..8211cf845b 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -203,8 +203,29 @@ let occur_uid uid sub =
 
 let occur_msid = occur_uid
 let occur_mbid = occur_uid
-
-
+    
+type 'a lazy_subst =
+  | LSval of 'a
+  | LSlazy of substitution * 'a
+	
+type 'a substituted = 'a lazy_subst ref
+      
+let from_val a = ref (LSval a)
+    
+let force fsubst r = 
+  match !r with
+  | LSval a -> a
+  | LSlazy(s,a) -> 
+      let a' = fsubst s a in
+      r := LSval a';
+      a' 
+
+let subst_substituted s r =
+  match !r with
+  | LSval a -> ref (LSlazy(s,a))
+  | LSlazy(s',a) ->
+      let s'' = join s' s in
+      ref (LSlazy(s'',a))
 
 (* Kernel names *)
 
@@ -353,3 +374,23 @@ let hcons_names () =
   let hmod = Hashcons.simple_hcons Hmod.f (hdir,huniqid,hstring) in
   let hkn = Hashcons.simple_hcons Hkn.f (hmod,hdir,hstring) in
   (hkn,hdir,hname,hident,hstring)
+
+
+(*******)
+
+type transparent_state = Idpred.t * KNpred.t
+
+type 'a tableKey =
+  | ConstKey of constant
+  | VarKey of identifier
+  | RelKey of 'a 
+
+
+type inv_rel_key = int (* index in the [rel_context] part of environment
+			  starting by the end, {\em inverse} 
+			  of de Bruijn indice *)
+
+type id_key = inv_rel_key tableKey
+
+
+
diff --git a/kernel/names.mli b/kernel/names.mli
index bd7b526873..a08d1be238 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -103,6 +103,11 @@ val map_mbid : mod_bound_id -> module_path -> substitution
 *)
 val join : substitution -> substitution -> substitution
 
+type 'a substituted
+val from_val : 'a -> 'a substituted
+val force : (substitution -> 'a -> 'a) -> 'a substituted -> 'a
+val subst_substituted : substitution -> 'a substituted -> 'a substituted
+
 (*i debugging *)
 val debug_string_of_subst : substitution -> string
 val debug_pr_subst : substitution -> Pp.std_ppcmds
@@ -174,3 +179,19 @@ type evaluable_global_reference =
 val hcons_names : unit ->
   (kernel_name -> kernel_name) * (dir_path -> dir_path) *
   (name -> name) * (identifier -> identifier) * (string -> string)
+
+
+(******)
+
+type 'a tableKey =
+  | ConstKey of constant
+  | VarKey of identifier
+  | RelKey of 'a 
+
+type transparent_state = Idpred.t * KNpred.t
+
+type inv_rel_key = int (* index in the [rel_context] part of environment
+			  starting by the end, {\em inverse} 
+			  of de Bruijn indice *)
+
+type id_key = inv_rel_key tableKey
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 28628cbda7..85d668f7a4 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -317,16 +317,15 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
     fold 0 cuniv
   else raise NotConvertible
 
-
+let clos_fconv cv_pb env t1 t2 =
+  let infos = create_clos_infos betaiotazeta env in
+  ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
 
 let fconv cv_pb env t1 t2 =
-  if eq_constr t1 t2 then 
-    Constraint.empty
-  else
-    let infos = create_clos_infos betaiotazeta env in
-    ccnv cv_pb infos ELID ELID (inject t1) (inject t2)
-      Constraint.empty
+  if eq_constr t1 t2 then Constraint.empty
+  else clos_fconv cv_pb env t1 t2
 
+let conv_cmp = fconv
 let conv = fconv CONV
 let conv_leq = fconv CUMUL
 
@@ -341,6 +340,32 @@ let conv_leq_vecti env v1 v2 =
     v1
     v2
 
+(* option for conversion *)
+let use_vm = ref true
+let vm_fconv = ref (fun _ _ _ _ -> error "VM not installed")
+let set_vm_conv_cmp f = vm_fconv := f
+
+let vm_conv cv_pb env t1 t2 =
+  if eq_constr t1 t2 then 
+    Constraint.empty
+  else if !use_vm then
+    try !vm_fconv cv_pb env t1 t2
+    with Not_found | Invalid_argument _ ->
+      (* If compilation fails, fall-back to closure conversion *)
+      clos_fconv cv_pb env t1 t2
+  else clos_fconv cv_pb env t1 t2
+
+let vm_conv_leq_vecti env v1 v2 =
+  array_fold_left2_i 
+    (fun i c t1 t2 ->
+      let c' =
+        try vm_conv CUMUL env t1 t2 
+        with NotConvertible -> raise (NotConvertibleVect i) in
+      Constraint.union c c')
+    Constraint.empty
+    v1
+    v2
+
 (*
 let convleqkey = Profile.declare_profile "Kernel_reduction.conv_leq";;
 let conv_leq env t1 t2 =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 4f519fff7a..ca4ab8c948 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -29,13 +29,26 @@ exception NotConvertible
 exception NotConvertibleVect of int
 type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints
 
+type conv_pb = CONV | CUMUL
+
+val sort_cmp : 
+    conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints
+
 val conv_sort      : sorts conversion_function
 val conv_sort_leq  : sorts conversion_function
 
-val conv           : types conversion_function
+val conv_cmp       : conv_pb -> constr conversion_function
+
+val conv           : constr conversion_function
 val conv_leq       : types conversion_function
 val conv_leq_vecti : types array conversion_function
 
+(* option for conversion *)
+val use_vm : bool ref
+val set_vm_conv_cmp : (conv_pb -> types conversion_function) -> unit
+val vm_conv : conv_pb -> types conversion_function
+val vm_conv_leq_vecti : types array conversion_function
+
 (************************************************************************)
 
 (* Builds an application node, reducing beta redexes it may produce. *) 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0182b39073..1ca0fec4a7 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -132,15 +132,15 @@ let hcons_constant_body cb =
 
 let add_constant dir l decl senv =
   check_label l senv.labset;
-  let cb = match decl with 
-      ConstantEntry ce -> translate_constant senv.env ce
+  let kn = make_kn senv.modinfo.modpath dir l in 
+  let cb = 
+    match decl with 
+    | ConstantEntry ce -> translate_constant senv.env kn ce
     | GlobalRecipe r ->
-        let cb = translate_recipe senv.env r in
-        if dir = empty_dirpath then hcons_constant_body cb else cb
+	let cb = translate_recipe senv.env kn r in
+	if dir = empty_dirpath then hcons_constant_body cb else cb
   in
-(*  let cb = if dir = empty_dirpath then hcons_constant_body cb else cb in*)
   let env' = Environ.add_constraints cb.const_constraints senv.env in
-  let kn = make_kn senv.modinfo.modpath dir l in
   let env'' = Environ.add_constant kn cb env' in
   kn, { old = senv.old;
 	env = env'';
@@ -417,7 +417,6 @@ let check_engagement env c =
 let set_engagement c senv =
   {senv with env = Environ.set_engagement c senv.env}
 
-
 (* Libraries = Compiled modules *)
 
 type compiled_library = 
diff --git a/kernel/sign.ml b/kernel/sign.ml
index d448ea3100..aebb420f41 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -53,13 +53,11 @@ let empty_rel_context = []
 
 let add_rel_decl d ctxt = d::ctxt
 
-let lookup_rel n sign =
-  let rec lookrec = function
-    | (1, decl :: _) -> decl
-    | (n, _ :: sign) -> lookrec (n-1,sign)
-    | (_, [])        -> raise Not_found
-  in 
-  lookrec (n,sign)
+let rec lookup_rel n sign =
+  match n, sign with
+  | 1, decl :: _ -> decl
+  | n, _ :: sign -> lookup_rel (n-1) sign
+  | _, []        -> raise Not_found
 
 let rel_context_length = List.length
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 08bcd1ddd2..1855858ca0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1137,6 +1137,7 @@ let nb_prod =
 let rec eq_constr m n = 
   (m==n) or
   compare_constr eq_constr m n
+
 let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
 (*******************)
@@ -1184,3 +1185,11 @@ let hcons_constr (hkn,hdir,hname,hident,hstr) =
   (hcci,htcci)
 
 let (hcons1_constr, hcons1_types) = hcons_constr (hcons_names())
+
+
+(*******)
+(* Type of abstract machine values *)
+type values
+
+
+
diff --git a/kernel/term.mli b/kernel/term.mli
index 8c72a9ff30..5ef42f96c1 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -523,3 +523,7 @@ val hcons_constr:
 
 val hcons1_constr : constr -> constr
 val hcons1_types : types -> types
+
+(**************************************)
+
+type values
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b2ecfa5990..291c409e9a 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -19,6 +19,8 @@ open Inductive
 open Environ
 open Entries
 open Type_errors
+open Cemitcodes
+open Cbytegen
 open Indtypes
 open Typeops
 
@@ -85,33 +87,38 @@ let infer_declaration env dcl =
   | DefinitionEntry c ->
       let (j,cst) = infer env c.const_entry_body in
       let (typ,cst) = constrain_type env j cst c.const_entry_type in
-      Some (Declarations.from_val j.uj_val), typ, cst, c.const_entry_opaque
+      Some (Declarations.from_val j.uj_val), typ, cst,
+        c.const_entry_opaque, c.const_entry_boxed
   | ParameterEntry t ->
       let (j,cst) = infer env t in
-      None, Typeops.assumption_of_judgment env j, cst, false
+      None, Typeops.assumption_of_judgment env j, cst, false, false
 
-let build_constant_declaration env (body,typ,cst,op) =
-  let ids = match body with 
+let build_constant_declaration env kn (body,typ,cst,op,boxed) =
+  let ids =
+    match body with 
     | None -> global_vars_set env typ
     | Some b ->
         Idset.union 
 	  (global_vars_set env (Declarations.force b)) 
-	  (global_vars_set env typ) 
+	  (global_vars_set env typ)
   in
+  let tps = from_val (compile_constant_body env kn body op boxed) in
   let hyps = keep_hyps env ids in
-    { const_body = body;
+    { const_hyps = hyps;
+      const_body = body;
       const_type = typ;
-      const_hyps = hyps;
+      const_body_code = tps;
+     (* const_type_code = to_patch env typ;*)
       const_constraints = cst;
       const_opaque = op }
 
 (*s Global and local constant declaration. *)
 
-let translate_constant env ce =
-  build_constant_declaration env (infer_declaration env ce)
+let translate_constant env kn ce =
+  build_constant_declaration env kn (infer_declaration env ce)
 
-let translate_recipe env r = 
-  build_constant_declaration env (Cooking.cook_constant env r)
+let translate_recipe env kn r = 
+  build_constant_declaration env kn (Cooking.cook_constant env r)
 
 (* Insertion of inductive types. *)
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 74dc9dc8c2..e3105fb904 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -24,11 +24,11 @@ val translate_local_def : env -> constr * types option ->
 
 val translate_local_assum : env -> types ->
   types * Univ.constraints
-
-val translate_constant : env -> constant_entry -> constant_body
+ 
+val translate_constant : env -> constant -> constant_entry -> constant_body
 
 val translate_mind : 
   env -> mutual_inductive_entry -> mutual_inductive_body
 
 val translate_recipe : 
-  env -> Cooking.recipe -> constant_body
+  env -> constant -> Cooking.recipe -> constant_body
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 46cf163bf0..05b7619e52 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -20,6 +20,9 @@ open Reduction
 open Inductive
 open Type_errors
 
+let conv = vm_conv CONV
+let conv_leq = vm_conv CUMUL
+let conv_leq_vecti = vm_conv_leq_vecti
 
 (* This should be a type (a priori without intension to be an assumption) *)
 let type_judgment env j =
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
new file mode 100644
index 0000000000..41817c3e01
--- /dev/null
+++ b/kernel/vconv.ml
@@ -0,0 +1,537 @@
+open Names
+open Declarations
+open Term
+open Vm
+open Environ
+open Conv_oracle
+open Reduction 
+open Closure
+open Vm
+open Csymtable
+open Univ
+open Cbytecodes
+
+
+(**** Test la structure des piles ****)
+
+let compare_zipper z1 z2 =
+  match z1, z2 with
+  | Zapp args1, Zapp args2 -> nargs args1 = nargs args2
+  | Zfix _, Zfix _ -> true 
+  | Zswitch _, Zswitch _ -> true
+  | _ , _ -> false
+
+let rec compare_stack stk1 stk2 =
+  match stk1, stk2 with
+  | [], [] -> true
+  | z1::stk1, z2::stk2 ->
+      if compare_zipper z1 z2 then compare_stack stk1 stk2
+      else false
+  | _, _ -> false 
+
+(**** Conversion ****)
+let conv_vect fconv vect1 vect2 cu =
+  let n = Array.length vect1 in
+  if n = Array.length vect2 then
+    let rcu = ref cu in
+    for i = 0 to n - 1 do
+      rcu := fconv vect1.(i) vect2.(i) !rcu
+    done;
+    !rcu
+  else raise NotConvertible
+
+let rec conv_val infos pb k v1 v2 cu =
+  if v1 == v2 then cu else conv_whd infos pb k (whd_val v1) (whd_val v2) cu 
+    
+and conv_whd infos pb k whd1 whd2 cu =
+  match whd1, whd2 with
+  | Vsort s1, Vsort s2 -> sort_cmp pb s1 s2 cu 
+  | Vprod p1, Vprod p2 ->
+      let cu = conv_val infos CONV k (dom p1) (dom p2) cu in
+      conv_fun infos pb k (codom p1) (codom p2) cu
+  | Vfun f1, Vfun f2 -> conv_fun infos CONV k f1 f2 cu
+  | Vfix f1, Vfix f2 -> conv_fix infos k f1 f2 cu
+  | Vfix_app fa1, Vfix_app fa2 ->
+      let f1 = fix fa1 in
+      let args1 = args_of_fix fa1 in
+      let f2 = fix fa2 in
+      let args2 = args_of_fix fa2 in
+      conv_arguments infos k args1 args2 (conv_fix infos k f1 f2 cu)
+  | Vcofix cf1, Vcofix cf2 -> 
+      conv_cofix infos k cf1 cf2 cu
+  | Vcofix_app cfa1, Vcofix_app cfa2 ->	
+      let cf1 = cofix cfa1 in
+      let args1 = args_of_cofix cfa1 in
+      let cf2 = cofix cfa2 in
+      let args2 = args_of_cofix cfa2 in
+      conv_arguments infos k args1 args2 (conv_cofix infos k cf1 cf2 cu)
+  | Vconstr_const i1, Vconstr_const i2 -> 
+      if i1 = i2 then cu else raise NotConvertible 
+  | Vconstr_block b1, Vconstr_block b2 ->
+      let sz = bsize b1 in
+      if btag b1 = btag b2 && sz = bsize b2 then
+	let rcu = ref cu in
+	for i = 0 to sz - 1 do
+	  rcu := conv_val infos CONV k (bfield b1 i) (bfield b2 i) !rcu
+	done;
+	!rcu
+      else raise NotConvertible
+  | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) -> 
+      conv_atom infos pb k a1 stk1 a2 stk2 cu
+  | _, Vatom_stk(Aiddef(_,v),stk) -> 
+      conv_whd infos pb k whd1 (whd_stack v stk) cu
+  | Vatom_stk(Aiddef(_,v),stk), _ -> 
+      conv_whd infos pb k (whd_stack v stk) whd2 cu
+  | _, _ -> raise NotConvertible
+
+and conv_atom infos pb k a1 stk1 a2 stk2 cu =
+  match a1, a2 with
+  | Aind (kn1,i1), Aind(kn2,i2) ->
+      if i1 = i2 && mind_equiv infos kn1 kn2 then
+	conv_stack infos k stk1 stk2 cu
+      else raise NotConvertible
+  | Aid ik1, Aid ik2 -> 
+      if ik1 = ik2 then conv_stack infos k stk1 stk2 cu 
+      else raise NotConvertible
+  | Aiddef(ik1,v1), Aiddef(ik2,v2) ->
+      begin
+	try
+	  if ik1 = ik2 then conv_stack infos k stk1 stk2 cu 
+	  else raise NotConvertible
+	with NotConvertible ->
+	  if oracle_order ik1 ik2 then             
+            conv_whd infos pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
+          else conv_whd infos pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
+      end
+  | Aiddef(ik1,v1), _ ->
+      conv_whd infos pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
+  | _, Aiddef(ik2,v2) ->
+      conv_whd infos pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
+  | Afix_app _, _ | _, Afix_app _ | Aswitch _, _ | _, Aswitch _ -> 
+      Util.anomaly "Vconv.conv_atom : Vm.whd_val doesn't work"
+  | _, _ -> raise NotConvertible 
+
+and conv_stack infos k stk1 stk2 cu =
+  if compare_stack stk1 stk2 then
+    let rec conv_rec stk1 stk2 cu =
+      match stk1, stk2 with
+      |	[], [] -> cu
+      |	Zapp args1 :: stk1, Zapp args2 :: stk2 ->
+	  conv_rec stk1 stk2 (conv_arguments infos k args1 args2 cu) 
+      |	Zfix fa1 :: stk1, Zfix fa2 :: stk2 ->
+	  let f1 = fix fa1 in
+	  let args1 = args_of_fix fa1 in
+	  let f2 = fix fa2 in
+	  let args2 = args_of_fix fa2 in
+	  conv_rec stk1 stk2 
+	    (conv_arguments infos k args1 args2 (conv_fix infos k f1 f2 cu))
+      |	Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
+	  if eq_tbl sw1 sw2 then
+	    let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
+	    let rcu = ref (conv_val infos CONV k vt1 vt2 cu) in
+	    let b1, b2 = branch_of_switch k sw1, branch_of_switch k sw2 in
+	    for i = 0 to Array.length b1 - 1 do
+	      rcu := 
+		conv_val infos CONV (k + fst b1.(i)) 
+		  (snd b1.(i)) (snd b2.(i)) !rcu
+	    done;
+	    conv_rec stk1 stk2 !rcu
+	  else raise NotConvertible
+      |	_, _ -> raise NotConvertible
+    in conv_rec stk1 stk2 cu
+  else raise NotConvertible
+
+and conv_fun infos pb k f1 f2 cu =
+  if f1 == f2 then cu
+  else
+    let arity,b1,b2 = decompose_vfun2 k f1 f2 in
+    conv_val infos pb (k+arity) b1 b2 cu
+
+and conv_fix infos k f1 f2 cu =
+  if f1 == f2 then cu 
+  else
+    if check_fix f1 f2 then
+      let tf1 = types_of_fix f1 in
+      let tf2 = types_of_fix f2 in
+      let cu = conv_vect (conv_val infos CONV k) tf1 tf2 cu in
+      let bf1 = bodies_of_fix k f1 in
+      let bf2 = bodies_of_fix k f2 in
+      conv_vect (conv_fun infos CONV (k + (fix_ndef f1))) bf1 bf2 cu
+    else raise NotConvertible
+
+and conv_cofix infos k cf1 cf2 cu =
+  if cf1 == cf2 then cu
+  else
+    if check_cofix cf1 cf2 then
+      let tcf1 = types_of_cofix cf1 in
+      let tcf2 = types_of_cofix cf2 in
+      let cu = conv_vect (conv_val infos CONV k) tcf1 tcf2 cu in
+      let bcf1 = bodies_of_cofix k cf1 in
+      let bcf2 = bodies_of_cofix k cf2 in
+      conv_vect (conv_val infos CONV (k + (cofix_ndef cf1))) bcf1 bcf2 cu
+    else raise NotConvertible
+
+and conv_arguments infos k args1 args2 cu =
+  if args1 == args2 then cu
+  else
+    let n = nargs args1 in
+    if n = nargs args2 then
+      let rcu = ref cu in
+      for i = 0 to n - 1 do
+	rcu := conv_val infos CONV k (arg args1 i) (arg args2 i) !rcu
+      done;
+      !rcu
+    else raise NotConvertible
+
+let rec conv_eq pb t1 t2 cu =
+  if t1 == t2 then cu 
+  else
+    match kind_of_term t1, kind_of_term t2 with
+    | Rel n1, Rel n2 -> 
+	if n1 = n2 then cu else raise NotConvertible
+    | Meta m1, Meta m2 ->
+	if m1 = m2 then cu else raise NotConvertible
+    | Var id1, Var id2 -> 
+	if id1 = id2 then cu else raise NotConvertible
+    | Sort s1, Sort s2 -> sort_cmp pb s1 s2 cu
+    | Cast (c1,_), _ -> conv_eq pb c1 t2 cu
+    | _, Cast (c2,_) -> conv_eq pb t1 c2 cu
+    | Prod (_,t1,c1), Prod (_,t2,c2) -> 
+	conv_eq pb c1 c2 (conv_eq CONV t1 t2 cu)
+    | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq CONV c1 c2 cu
+    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> 
+	conv_eq pb c1 c2 (conv_eq CONV b1 b2 cu)
+    | App (c1,l1), App (c2,l2) ->
+	conv_eq_vect l1 l2 (conv_eq CONV c1 c2 cu)
+    | Evar (e1,l1), Evar (e2,l2) ->
+	if e1 = e2 then conv_eq_vect l1 l2 cu
+	else raise NotConvertible
+    | Const c1, Const c2 -> 
+	if c1 = c2 then cu else raise NotConvertible
+    | Ind c1, Ind c2 -> 
+	if c1 = c2 then cu else raise NotConvertible
+    | Construct c1, Construct c2 -> 
+	if c1 = c2 then cu else raise NotConvertible
+    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
+	let pcu = conv_eq CONV p1 p2 cu in
+	let ccu = conv_eq CONV c1 c2 pcu in
+	conv_eq_vect bl1 bl2 ccu
+    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
+	if ln1 = ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu)
+	else raise NotConvertible
+    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->	
+	if ln1 = ln2 then conv_eq_vect tl1 tl2 (conv_eq_vect bl1 bl2 cu)
+	else raise NotConvertible
+    | _ -> raise NotConvertible
+
+and conv_eq_vect vt1 vt2 cu =
+  let len = Array.length vt1 in
+  if len = Array.length vt2 then
+    let rcu = ref cu in
+    for i = 0 to len-1 do
+      rcu := conv_eq CONV vt1.(i) vt2.(i) !rcu
+    done; !rcu
+  else raise NotConvertible
+      
+let vconv pb env t1 t2 =
+  let cu =
+    try conv_eq pb t1 t2 Constraint.empty
+    with NotConvertible ->
+      let infos = create_clos_infos betaiotazeta env in
+      let v1 = val_of_constr env t1 in
+      let v2 = val_of_constr env t2 in
+      let cu = conv_val infos pb (nb_rel env) v1 v2 Constraint.empty in
+      cu
+  in cu
+
+let _ = Reduction.set_vm_conv_cmp vconv
+
+(*******************************************)
+(**** Calcul de la forme normal d'un terme *)
+(*******************************************)
+
+let crazy_type = mkSet 
+
+let decompose_prod env t =
+  let (name,dom,codom as res) = destProd (whd_betadeltaiota env t) in
+  if name = Anonymous then (Name (id_of_string "x"),dom,codom)
+  else res
+
+exception Find_at of int
+
+(* rend le numero du constructeur correspondant au tag [tag],
+   [cst] = true si c'est un constructeur constant *)
+
+let invert_tag cst tag reloc_tbl =
+  try 
+    for j = 0 to Array.length reloc_tbl - 1 do
+      let tagj,arity = reloc_tbl.(j) in
+      if tag = tagj && (cst && arity = 0 || not(cst || arity = 0)) then
+	raise (Find_at j)
+      else ()
+    done;raise Not_found 
+  with Find_at j -> (j+1)   
+             (*** Argggg, ces constructeurs de ... qui commencent a 1*)
+
+(* Build the substitution that replaces Rels by the appropriate 
+  inductives *)
+let ind_subst mind mib =
+  let ntypes = mib.mind_ntypes in
+  let make_Ik k = mkInd (mind,ntypes-k-1) in 
+  Util.list_tabulate make_Ik ntypes
+
+(* Instantiate inductives and parameters in constructor type
+   in normal form *)
+let constructor_instantiate mind mib params ctyp =
+  let si = ind_subst mind mib in
+  let ctyp1 = substl si ctyp in
+  let nparams = Array.length params in
+  if nparams = 0 then ctyp1
+  else
+    let _,ctyp2 = decompose_prod_n nparams ctyp1 in
+    let sp = Array.to_list params in substl sp ctyp2
+  
+let destApplication t =
+  try destApplication t 
+  with _ -> t,[||]
+
+let construct_of_constr_const env tag typ =
+  let cind,params = destApplication (whd_betadeltaiota env typ) in
+  let ind = destInd cind in
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  let rtbl = mip.mind_reloc_tbl in
+  let i = invert_tag true tag rtbl in
+  mkApp(mkConstruct(ind,i), params)
+
+let find_rectype typ =
+  let cind,args = destApplication typ in
+  let ind = destInd cind in
+  ind, args
+
+let construct_of_constr_block env tag typ =
+  let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env typ) in
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
+  let nparams = mip.mind_nparams in
+  let rtbl = mip.mind_reloc_tbl in
+  let i = invert_tag false tag rtbl in
+  let params = Array.sub allargs 0 nparams in
+  let specif = mip.mind_nf_lc in
+  let ctyp = constructor_instantiate mind mib params specif.(i-1) in
+  (mkApp(mkConstruct(ind,i), params), ctyp)
+  	
+let constr_type_of_idkey env idkey =
+  match idkey with
+  | ConstKey cst ->
+      let ty = (lookup_constant cst env).const_type in
+      mkConst cst, ty
+  | VarKey id -> 
+      let (_,_,ty) = lookup_named id env in 
+      mkVar id, ty
+  | RelKey i -> 
+      let n = (nb_rel env - i) in
+      let (_,_,ty) = lookup_rel n env in
+      mkRel n, lift n ty
+
+let type_of_ind env ind = 
+  let (_,mip) = Inductive.lookup_mind_specif env ind in
+  mip.mind_nf_arity
+
+let build_branches_type (mind,_ as ind) mib mip params dep p rtbl =
+  (* [build_one_branch i cty] construit le type de la ieme branche (commence
+     a 0) et les lambda correspondant aux realargs *)
+  let build_one_branch i cty =
+    let typi = constructor_instantiate mind mib params cty in
+    let decl,indapp = Term.decompose_prod typi in
+    let ind,cargs = find_rectype indapp in
+    let nparams = Array.length params in
+    let carity = snd (rtbl.(i)) in
+    let crealargs = Array.sub cargs nparams (Array.length cargs - nparams) in
+    let codom = 
+      let papp = mkApp(p,crealargs) in
+      if dep then
+	let cstr = ith_constructor_of_inductive ind (i+1) in
+        let relargs = Array.init carity (fun i -> mkRel (carity-i)) in
+	let dep_cstr = mkApp(mkApp(mkConstruct cstr,params),relargs) in
+	mkApp(papp,[|dep_cstr|])
+      else papp
+    in 
+    decl, codom
+  in Array.mapi build_one_branch mip.mind_nf_lc
+
+(** La fonction de normalisation *)
+
+let rec nf_val env v t = nf_whd env (whd_val v) t 
+
+and nf_whd env whd typ =
+  match whd with
+  | Vsort s -> mkSort s
+  | Vprod p ->
+      let dom = nf_val env (dom p) crazy_type in
+      let name = Name (id_of_string "x") in
+      let vc = body_of_vfun (nb_rel env) (codom p) in
+      let codom = nf_val (push_rel (name,None,dom) env) vc crazy_type in      
+      mkProd(name,dom,codom)	  
+  | Vfun f -> nf_fun env f typ
+  | Vfix f -> nf_fix env f
+  | Vfix_app fa ->
+      let f = fix fa in
+      let vargs = args_of_fix fa in
+      let fd = nf_fix env f in
+      let (_,i),(_,ta,_) = destFix fd in
+      let t = ta.(i) in
+      let _, args = nf_args  env vargs t in
+      mkApp(fd,args)
+  | Vcofix cf -> nf_cofix env cf 
+  | Vcofix_app cfa -> 
+      let cf = cofix cfa in
+      let vargs = args_of_cofix cfa in
+      let cfd = nf_cofix env cf in
+      let i,(_,ta,_) = destCoFix cfd in
+      let t = ta.(i) in
+      let _, args = nf_args env vargs t in
+      mkApp(cfd,args) 
+  | Vconstr_const n -> construct_of_constr_const env n typ
+  | Vconstr_block b ->
+      let capp,ctyp = construct_of_constr_block env (btag b) typ in
+      let args = nf_bargs env b ctyp in
+      mkApp(capp,args)
+  | Vatom_stk(Aid idkey, stk) ->
+      let c,typ = constr_type_of_idkey env idkey in
+      nf_stk env c typ stk
+  | Vatom_stk(Aiddef(idkey,_), stk) ->
+      let c,typ = constr_type_of_idkey env idkey in
+      nf_stk env c typ stk
+  | Vatom_stk(Aind ind, stk) ->
+      nf_stk env (mkInd ind) (type_of_ind env ind) stk 
+  | Vatom_stk(_,stk) -> assert false
+
+and nf_stk env c t stk  =
+  match stk with
+  | [] -> c
+  | Zapp vargs :: stk ->
+      let t, args = nf_args env vargs t in
+      nf_stk env (mkApp(c,args)) t stk 
+  | Zfix fa :: stk ->   
+      let f = fix fa in
+      let vargs = args_of_fix fa in
+      let fd = nf_fix env f in
+      let (_,i),(_,ta,_) = destFix fd in
+      let tf = ta.(i) in
+      let typ, args = nf_args env vargs tf in
+      let _,_,codom = decompose_prod env typ in
+      nf_stk env (mkApp(mkApp(fd,args),[|c|])) (subst1 c codom) stk
+  | Zswitch sw :: stk -> 
+    
+      let (mind,_ as ind),allargs = find_rectype (whd_betadeltaiota env t) in
+      let (mib,mip) = Inductive.lookup_mind_specif env ind in
+      let nparams = mip.mind_nparams in
+      let params,realargs = Util.array_chop nparams allargs in
+      (* calcul du predicat du case, 
+        [dep] indique si c'est un case dependant *)
+      let dep,p = 
+	let dep = ref false in
+	let rec nf_predicate env v pT =
+	  match whd_val v, kind_of_term pT with
+	  | Vfun f, Prod _ ->
+	      let k = nb_rel env in
+	      let vb = body_of_vfun k f in
+	      let name,dom,codom = decompose_prod env pT in
+	      let body = 
+		nf_predicate (push_rel (name,None,dom) env) vb codom in
+              mkLambda(name,dom,body)
+	  | Vfun f, _ ->
+	      dep := true;
+	      let k = nb_rel env in
+	      let vb = body_of_vfun k f in
+	      let name = Name (id_of_string "c") in
+	      let n = mip.mind_nrealargs in
+	      let rargs = Array.init n (fun i -> mkRel (n-i)) in
+	      let dom = mkApp(mkApp(mkInd ind,params),rargs) in
+	      let body = 
+		nf_val (push_rel (name,None,dom) env) vb crazy_type in
+	      mkLambda(name,dom,body)
+          | _, _ -> nf_val env v crazy_type
+	in 
+	let aux = nf_predicate env (type_of_switch sw) mip.mind_nf_arity in
+	!dep,aux in
+      (* Calcul du type des branches *)
+      let btypes = 
+	build_branches_type ind mib mip params dep p mip.mind_reloc_tbl in
+      (* calcul des branches *)
+      let bsw = branch_of_switch (nb_rel env) sw in
+      let mkbranch i (n,v) =
+	let decl,codom = btypes.(i) in
+	let env = 
+	  List.fold_right 
+	    (fun (name,t) env -> push_rel (name,None,t) env) decl env in
+	let b = nf_val env v codom in
+	compose_lam decl b 
+      in 
+      let branchs = Array.mapi mkbranch bsw in
+      let tcase = 
+	if dep then mkApp(mkApp(p, params), [|c|])
+	else mkApp(p, params)
+      in
+      let ci = case_info sw in
+      nf_stk env (mkCase(ci, p, c, branchs)) tcase stk
+       
+and nf_args env vargs t =
+  let t = ref t in
+  let len = nargs vargs in
+  let targs = 
+    Array.init len 
+      (fun i ->
+	let _,dom,codom = decompose_prod env !t in
+	let c = nf_val env (arg vargs i) dom in
+	t := subst1 c codom; c) in
+  !t,targs
+
+and nf_bargs env b t =
+  let t = ref t in
+  let len = bsize b in
+  Array.init len 
+    (fun i ->
+      let _,dom,codom = decompose_prod env !t in
+      let c = nf_val env (bfield b i) dom in
+      t := subst1 c codom; c) 
+
+and nf_fun env f typ =
+  let k = nb_rel env in
+  let vb = body_of_vfun k f in
+  let name,dom,codom = decompose_prod env typ in
+  let body = nf_val (push_rel (name,None,dom) env) vb codom in
+  mkLambda(name,dom,body)
+
+and nf_fix env f =
+  let init = fix_init f in
+  let rec_args = rec_args f in
+  let ndef = fix_ndef f in
+  let vt = types_of_fix f in
+  let ft = Array.map (fun v -> nf_val env v crazy_type) vt in
+  let name = Array.init ndef (fun _ -> (Name (id_of_string "Ffix"))) in
+  let k = nb_rel env in
+  let vb = bodies_of_fix k f in 
+  let env = push_rec_types (name,ft,ft) env in 
+  let fb = Util.array_map2 (fun v t -> nf_fun env v t) vb ft in
+  mkFix ((rec_args,init),(name,ft,fb))
+  
+and nf_cofix env cf =
+  let init = cofix_init cf in
+  let ndef = cofix_ndef cf in
+  let vt = types_of_cofix cf in
+  let cft = Array.map (fun v -> nf_val env v crazy_type) vt in
+  let name = Array.init ndef (fun _ -> (Name (id_of_string "Fcofix"))) in
+  let k = nb_rel env in
+  let vb = bodies_of_cofix k cf in 
+  let env = push_rec_types (name,cft,cft) env in 
+  let cfb = Util.array_map2 (fun v t -> nf_val env v t) vb cft in
+  mkCoFix (init,(name,cft,cfb))
+  
+let cbv_vm env c t  =
+  if not (transp_values ()) then swap_global_transp ();
+  let v = val_of_constr env c in
+  let c = nf_val env v t in
+  if not (transp_values ()) then swap_global_transp ();
+  c
+  
+
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
new file mode 100644
index 0000000000..21fd4601b1
--- /dev/null
+++ b/kernel/vconv.mli
@@ -0,0 +1,14 @@
+(*i*)
+open Names
+open Term
+open Environ
+open Reduction
+(*i*)
+
+(***********************************************************************)
+(*s conversion functions *)
+val vconv : conv_pb -> types conversion_function
+
+(***********************************************************************)
+(*s Reduction functions *)
+val cbv_vm : env -> constr -> types -> constr
diff --git a/kernel/vm.ml b/kernel/vm.ml
new file mode 100644
index 0000000000..80ecdf369b
--- /dev/null
+++ b/kernel/vm.ml
@@ -0,0 +1,593 @@
+open Obj
+open Names
+open Term
+open Conv_oracle
+open Cbytecodes
+
+(* use transparant constant or not *)
+
+external swap_global_transp : unit -> unit = "swap_coq_global_transp"
+
+let transp_values = ref false
+
+let set_transp_values b =
+  if b = !transp_values then ()
+  else (
+    transp_values := not !(transp_values);
+    swap_global_transp ())
+ 
+let transp_values _ = !transp_values
+
+
+
+(******************************************)
+(* Fonctions en plus du module Obj ********)
+(******************************************)
+
+
+
+external offset_closure : t -> int -> t = "coq_offset_closure"
+external offset : t -> int = "coq_offset"
+let first o = (offset_closure o (offset o))
+let last o = (field o (size o - 1))
+
+let accu_tag = 0
+
+(*******************************************)
+(* Initalisation de la machine abstraite ***)
+(*******************************************)
+
+external init_vm : unit -> unit = "init_coq_vm"
+
+let _ = init_vm ()
+
+(*******************************************)
+(* Le code machine  ************************)
+(*******************************************)
+
+type tcode 
+let tcode_of_obj v = ((obj v):tcode)
+let fun_code v = tcode_of_obj (field (repr v) 0)
+
+external mkAccuCode : int -> tcode = "coq_makeaccu"
+external mkPopStopCode : int -> tcode = "coq_pushpop"
+
+external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode"
+external int_tcode : tcode -> int -> int = "coq_int_tcode"
+
+external accumulate : unit -> tcode = "accumulate_code"
+let accumulate = accumulate ()
+
+let popstop_tbl =  ref (Array.init 30 mkPopStopCode) 
+
+let popstop_code i =
+  let len = Array.length !popstop_tbl in
+  if i < len then !popstop_tbl.(i) 
+  else
+    begin
+      popstop_tbl :=
+	Array.init (i+10)
+	  (fun j -> if j < len then !popstop_tbl.(j) else mkPopStopCode j);
+      !popstop_tbl.(i) 
+    end
+
+let stop = popstop_code 0
+  
+(******************************************************)
+(* Types de donnees abstraites et fonctions associees *)
+(******************************************************)
+
+(* Values of the abstract machine *)
+let val_of_obj v = ((obj v):values)
+let crasy_val = (val_of_obj (repr 0))
+
+
+(* Functions *)
+type vfun  
+(* v = [Tc | c | fv1 | ... | fvn ] *)
+(*                  ^                       *)
+(* [Tc | (Restart : c) | v | a1 | ... an] *)
+(*              ^                                  *)
+
+(* Products *)
+type vprod 
+(* [0 | dom : codom] *) 
+(*     ^              *)
+let dom : vprod -> values = fun p -> val_of_obj (field (repr p) 0) 
+let codom : vprod -> vfun = fun p -> (obj (field (repr p) 1))
+
+(* Arguments *)
+type arguments 
+(* arguments = [_ | _ | _ | a1 | ... | an] *)
+(*                ^                        *)
+let nargs : arguments -> int = fun args -> (size (repr args)) - 2
+
+let unsafe_arg : arguments -> int -> values =
+     fun args i ->  val_of_obj (field (repr args) (i+2))
+
+let arg args i = 
+  if  0 <= i && i < (nargs args) then unsafe_arg args i 
+  else raise (Invalid_argument 
+		("Vm.arg size = "^(string_of_int (nargs args))^
+		 " acces "^(string_of_int i)))
+
+(* Fixpoints *)
+type vfix
+
+(* [Tc|c0|Ti|c1|...|Ti|cn|fv1|...|fvn| [ct0|...|ctn]] *)
+(*          ^                                         *)
+type vfix_block 
+
+let fix_init : vfix -> int = fun vf -> (offset (repr vf)/2)
+
+let block_of_fix : vfix -> vfix_block = fun vf -> obj (first (repr vf))
+
+let fix_block_type : vfix_block -> tcode array =
+  fun fb -> (obj (last (repr fb)))
+
+let fix_block_ndef : vfix_block -> int = 
+  fun fb -> size (last (repr fb))
+
+let fix_ndef vf = fix_block_ndef (block_of_fix vf)
+
+let unsafe_fb_code : vfix_block -> int -> tcode =
+  fun fb i -> tcode_of_obj (field (repr fb) (2 * i))
+
+let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
+  
+let rec_args vf =
+  let fb = block_of_fix vf in
+  let size = fix_block_ndef fb in
+  Array.init size (unsafe_rec_arg fb)
+
+exception FALSE
+
+let check_fix f1 f2 = 
+  let i1, i2 = fix_init f1, fix_init f2 in
+  (* Verification du point de depart *)
+    if i1 = i2 then
+      let fb1,fb2 = block_of_fix f1, block_of_fix f2 in
+      let n = fix_block_ndef fb1 in
+    (* Verification du nombre de definition *)
+      if n = fix_block_ndef fb2 then
+      (* Verification des arguments recursifs *)
+	try
+	  for i = 0 to n - 1 do
+	    if not (unsafe_rec_arg fb1 i = unsafe_rec_arg fb2 i) then
+	      raise FALSE
+	  done;
+	  true
+	with FALSE -> false
+      else false 
+    else false
+
+(* Partials applications of Fixpoints *)
+type vfix_app
+let fix : vfix_app -> vfix = 
+  fun vfa -> ((obj (field (repr vfa) 1)):vfix)
+let args_of_fix : vfix_app -> arguments =
+  fun vfa -> ((magic  vfa) : arguments)
+
+(* CoFixpoints *)
+type vcofix 
+type vcofix_block
+let cofix_init : vcofix -> int = fun vcf -> (offset (repr vcf)/2)
+
+let block_of_cofix : vcofix -> vcofix_block = fun vcf -> obj (first (repr vcf))
+
+let cofix_block_ndef : vcofix_block -> int = 
+  fun fb -> size (last (repr fb))
+
+let cofix_ndef vcf= cofix_block_ndef (block_of_cofix vcf)
+
+let cofix_block_type : vcofix_block -> tcode array =
+  fun cfb -> (obj (last (repr cfb)))
+
+let check_cofix cf1 cf2 = 
+  cofix_init cf1 = cofix_init cf2 &&
+  cofix_ndef cf1 = cofix_ndef cf2 
+
+let cofix_arity c = int_tcode c 1
+
+let unsafe_cfb_code : vcofix_block -> int -> tcode =
+  fun cfb i -> tcode_of_obj (field (repr cfb) (2 * i))
+
+(* Partials applications of CoFixpoints *)
+type vcofix_app 
+let cofix : vcofix_app -> vcofix = 
+  fun vcfa -> ((obj (field (repr vcfa) 1)):vcofix)
+let args_of_cofix : vcofix_app -> arguments = 
+  fun vcfa -> ((magic  vcfa) : arguments)
+
+(* Blocks *)
+type vblock (* la representation Ocaml *)
+let btag : vblock -> int = fun b -> tag (repr b)
+let bsize : vblock -> int = fun b -> size (repr b)
+let bfield b i =
+  if 0 <= i && i < (bsize b) then
+    val_of_obj (field (repr b) i)
+  else raise (Invalid_argument "Vm.bfield")
+
+(* Accumulators and atoms *)
+
+type accumulator 
+(* [Ta | accumulate | at | a1 | ... | an ] *)
+
+type inv_rel_key = int
+
+type id_key = inv_rel_key tableKey
+
+type vstack = values array
+
+type vm_env 
+
+type vswitch = {
+    sw_type_code : tcode; 
+    sw_code : tcode; 
+    sw_annot : annot_switch;
+    sw_stk : vstack;
+    sw_env : vm_env
+  } 
+
+type atom = 
+  | Aid of id_key
+  | Aiddef of id_key * values
+  | Aind of inductive
+  | Afix_app of accumulator * vfix_app
+  | Aswitch of accumulator * vswitch
+
+let atom_of_accu : accumulator -> atom =
+  fun a -> ((obj (field (repr a) 1)) : atom)
+
+let args_of_accu : accumulator -> arguments = 
+  fun a -> ((magic a) : arguments)
+
+let nargs_of_accu a = nargs (args_of_accu a)
+
+(* Les zippers *)
+
+type zipper =
+  | Zapp of arguments
+  | Zfix of vfix_app
+  | Zswitch of vswitch
+
+type stack = zipper list
+
+type whd =
+  | Vsort of sorts
+  | Vprod of vprod 
+  | Vfun of vfun
+  | Vfix of vfix
+  | Vfix_app of vfix_app
+  | Vcofix of vcofix
+  | Vcofix_app of vcofix_app
+  | Vconstr_const of int
+  | Vconstr_block of vblock
+  | Vatom_stk of atom * stack
+(* Les atomes sont forcement Aid Aiddef Aind *)
+
+(**********************************************)
+(* Constructeurs ******************************)
+(**********************************************)
+(* obj_of_atom : atom -> t *)
+let obj_of_atom : atom -> t =
+  fun a -> 
+    let res = Obj.new_block accu_tag 2 in
+    set_field res 0 (repr accumulate);
+    set_field res 1 (repr a);
+    res 
+
+(* obj_of_str_const : structured_constant -> t *)
+let rec obj_of_str_const str =
+  match str with 
+  | Const_sorts s -> repr (Vsort s)
+  | Const_ind ind -> obj_of_atom (Aind ind)
+  | Const_b0 tag -> repr tag
+  | Const_bn(tag, args) ->
+      let len = Array.length args in
+      let res = new_block tag len in
+      for i = 0 to len - 1 do 
+	set_field res i (obj_of_str_const args.(i)) 
+      done;
+      res
+
+let val_of_obj o = ((obj o) : values)
+
+let val_of_str_const str = val_of_obj (obj_of_str_const str)
+
+let val_of_atom a = val_of_obj (obj_of_atom a)
+
+let idkey_tbl = Hashtbl.create 31
+
+let val_of_idkey key =
+  try Hashtbl.find idkey_tbl key 
+  with Not_found -> 
+    let v = val_of_atom (Aid key) in
+    Hashtbl.add idkey_tbl key v;
+    v
+
+let val_of_rel k = val_of_idkey (RelKey k)
+let val_of_rel_def k v = val_of_atom(Aiddef(RelKey k, v))
+
+let val_of_named id = val_of_idkey (VarKey id)
+let val_of_named_def id v = val_of_atom(Aiddef(VarKey id, v))
+  
+let val_of_constant c = val_of_idkey (ConstKey c)
+let val_of_constant_def c v = val_of_atom(Aiddef(ConstKey c, v))
+
+
+(*************************************************)
+(* Destructors ***********************************)
+(*************************************************)
+
+
+let rec whd_accu a stk =
+  let n = nargs_of_accu a in
+  let stk = 
+    if nargs_of_accu a = 0 then stk
+    else Zapp (args_of_accu a) :: stk in
+  
+  let at = atom_of_accu a in
+  match at with
+  | Aid _ | Aiddef _ | Aind _ -> Vatom_stk(at, stk)
+  | Afix_app(a,fa) -> whd_accu a (Zfix fa :: stk)
+  | Aswitch(a,sw) -> whd_accu a (Zswitch sw :: stk)
+
+external kind_of_closure : t -> int = "coq_kind_of_closure"
+
+
+let whd_val : values -> whd =
+  fun v -> 
+    let o = repr v in 
+    if is_int o then Vconstr_const (obj o)
+    else 
+      let tag = tag o in
+      if tag = accu_tag then
+	if fun_code o == accumulate then whd_accu (obj o) []
+	else 
+	  if size o = 1 then Vsort(obj (field o 0))
+	  else Vprod(obj o)
+      else 
+	if tag = closure_tag || tag = infix_tag then
+	  match kind_of_closure o with
+	  | 0 -> Vfun(obj o)
+	  | 1 -> Vfix(obj o)
+	  | 2 -> Vfix_app(obj o) 
+	  | 3 -> Vcofix(obj o)
+	  | 4 -> Vcofix_app(obj o)
+	  | 5 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
+	  | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work"
+	else Vconstr_block(obj o)
+	
+
+
+(************************************************)
+(* La machine abstraite *************************)
+(************************************************)
+
+
+(* gestion de la pile *)
+external push_ra : tcode -> unit = "coq_push_ra"
+external push_val : values -> unit = "coq_push_val"
+external push_arguments : arguments -> unit = "coq_push_arguments"
+external push_vstack : vstack -> unit = "coq_push_vstack"
+
+
+(* interpreteur *)
+external interprete : tcode -> values -> vm_env -> int -> values =
+  "coq_interprete_ml"
+
+let apply_arguments vf vargs =
+  let n = nargs vargs in
+  if n = 0 then vf 
+  else
+   begin
+     push_ra stop;
+     push_arguments vargs;
+     interprete (fun_code vf) vf (magic vf) (n - 1)
+   end
+
+let apply_vstack vf vstk =
+  let n = Array.length vstk in
+  if n = 0 then vf
+  else 
+    begin
+      push_ra stop;
+      push_vstack vstk;
+      interprete (fun_code vf) vf (magic vf) (n - 1)
+    end
+
+let apply_fix_app vfa arg =
+  let vf = fix vfa in
+  let vargs = args_of_fix vfa in
+  push_ra stop;
+  push_val arg;
+  push_arguments vargs;
+  interprete (fun_code vf) (magic vf) (magic vf) (nargs vargs)
+
+let apply_switch sw arg =
+  
+  let tc = sw.sw_annot.tailcall in
+  if tc then 
+    (push_ra stop;push_vstack sw.sw_stk)
+  else 
+    (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk)));
+  interprete sw.sw_code arg sw.sw_env 0
+
+let is_accu v = 
+  is_block (repr v) && tag (repr v) = accu_tag && 
+  fun_code v == accumulate 
+
+let rec whd_stack v stk =  
+  match stk with
+  | [] -> whd_val v
+  | Zapp a :: stkt -> whd_stack (apply_arguments v a) stkt
+  | Zfix fa :: stkt -> 
+      if is_accu v then whd_accu (magic v) stk
+      else whd_stack (apply_fix_app fa v) stkt
+  | Zswitch sw :: stkt -> 
+      if is_accu v then whd_accu (magic v) stk 
+      else whd_stack (apply_switch sw v) stkt 
+
+	  
+
+(* Function *)
+external closure_arity : vfun -> int = "coq_closure_arity"
+
+(* [apply_rel v k arity] applique la valeurs [v] aux arguments 
+   [k],[k+1], ... , [k+arity-1] *)
+let mkrel_vstack k arity =
+  let max = k + arity - 1 in
+  Array.init arity (fun i -> val_of_rel (max - i))
+
+let body_of_vfun k vf =
+  let vargs = mkrel_vstack k 1 in
+  apply_vstack (magic vf) vargs
+
+let decompose_vfun2 k vf1 vf2 =
+  let arity = min (closure_arity vf1) (closure_arity vf2) in
+  assert (0 <= arity && arity < Sys.max_array_length);
+  let vargs = mkrel_vstack k arity in
+  let v1 = apply_vstack (magic vf1) vargs in
+  let v2 = apply_vstack (magic vf2) vargs in
+  arity, v1, v2
+    
+  
+(* Fix *)
+external atom_rel : unit -> atom array = "get_coq_atom_tbl"
+external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl"
+
+let relaccu_tbl =  
+  let atom_rel = atom_rel() in
+  let len = Array.length atom_rel in
+  for i = 0 to len - 1 do atom_rel.(i) <- Aid (RelKey i) done;
+  ref (Array.init len mkAccuCode) 
+
+let relaccu_code i =
+  let len = Array.length !relaccu_tbl in
+  if i < len then !relaccu_tbl.(i) 
+  else
+    begin
+      realloc_atom_rel i;
+      let atom_rel = atom_rel () in
+      let nl = Array.length atom_rel in
+      for j = len to nl - 1 do atom_rel.(j) <- Aid(RelKey j) done;
+      relaccu_tbl :=
+	Array.init nl
+	  (fun j -> if j < len then !relaccu_tbl.(j) else mkAccuCode j);
+      !relaccu_tbl.(i) 
+    end
+
+let jump_grabrec c = offset_tcode c 2
+let jump_grabrecrestart c = offset_tcode c 3
+
+let bodies_of_fix k vf = 
+  let fb = block_of_fix vf in
+  let ndef = fix_block_ndef fb in
+  (* Construction de l' environnement des corps des points fixes *)
+  let e = dup (repr fb) in
+  for i = 0 to ndef - 1 do
+    set_field e (2 * i) (repr (relaccu_code (k + i)))
+  done;
+  let fix_body i =
+    let c = jump_grabrec (unsafe_fb_code fb i)  in
+    let res = Obj.new_block closure_tag 2 in
+    set_field res 0 (repr c);
+    set_field res 1 (offset_closure e (2*i));
+    ((obj res) : vfun)
+  in Array.init ndef fix_body
+ 
+let types_of_fix vf =
+  let fb = block_of_fix vf in
+  let type_code = fix_block_type fb in
+  let type_val c = interprete c crasy_val (magic fb) 0 in
+  Array.map type_val type_code
+
+ 
+(* CoFix *)
+let jump_cograb c = offset_tcode c 2
+let jump_cograbrestart c = offset_tcode c 3 
+
+let bodies_of_cofix k vcf =
+  let cfb = block_of_cofix vcf in
+  let ndef = cofix_block_ndef cfb in
+  (* Construction de l' environnement des corps des cofix *)
+  let e = dup (repr cfb) in
+  for i = 0 to ndef - 1 do
+    set_field e (2 * i) (repr (relaccu_code (k + i)))
+  done;
+  let cofix_body i =
+    let c = unsafe_cfb_code cfb i in 
+    let arity = int_tcode c 1 in
+    if arity = 0 then 
+      begin
+	push_ra stop;
+	interprete (jump_cograbrestart c) crasy_val 
+	  (obj (offset_closure e (2*i))) 0
+      end
+    else 
+      let res = Obj.new_block closure_tag 2 in
+      set_field res 0 (repr (jump_cograb c));
+      set_field res 1 (offset_closure e (2*i));
+      ((obj res) : values)
+  in Array.init ndef cofix_body
+
+let types_of_cofix vcf =
+  let cfb = block_of_cofix vcf in
+  let type_code = cofix_block_type cfb in
+  let type_val c = interprete c crasy_val (magic cfb) 0 in
+  Array.map type_val type_code
+
+(* Switch *)
+      
+let eq_tbl sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl 
+    
+let case_info sw = sw.sw_annot.ci
+    
+let type_of_switch sw = 
+  push_vstack sw.sw_stk;
+  interprete sw.sw_type_code crasy_val sw.sw_env 0 
+    
+let branch_arg k (tag,arity) = 
+  if arity = 0 then  ((magic tag):values)
+  else
+    let b = new_block tag arity in
+    for i = 0 to arity - 1 do
+      set_field b i (repr (val_of_rel (k+i)))
+    done;
+    val_of_obj b
+  
+      
+let branch_of_switch k sw =
+  let eval_branch (_,arity as ta) =
+    let arg = branch_arg k ta in
+    let v = apply_switch sw arg in
+    (arity, v)
+  in 
+  Array.map eval_branch sw.sw_annot.rtbl
+    
+
+    
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/kernel/vm.mli b/kernel/vm.mli
new file mode 100644
index 0000000000..d6e7f6eee6
--- /dev/null
+++ b/kernel/vm.mli
@@ -0,0 +1,108 @@
+open Names
+open Term
+open Cbytecodes
+open Cemitcodes
+
+(* option for virtual machine *)
+val transp_values : unit -> bool
+val set_transp_values : bool -> unit
+val swap_global_transp : unit -> unit
+(* le code machine *)
+type tcode 
+
+(* Les valeurs ***********)
+
+type accumulator
+type vprod 
+type vfun
+type vfix
+type vfix_app
+type vcofix
+type vcofix_app 
+type vblock
+type vswitch
+type arguments
+
+type zipper =
+  | Zapp of arguments
+  | Zfix of vfix_app
+  | Zswitch of vswitch
+
+type stack = zipper list
+
+
+type atom = 
+  | Aid of id_key
+  | Aiddef of id_key * values
+  | Aind of inductive
+  | Afix_app of accumulator * vfix_app
+  | Aswitch of accumulator * vswitch
+
+type whd =
+  | Vsort of sorts
+  | Vprod of vprod 
+  | Vfun of vfun
+  | Vfix of vfix
+  | Vfix_app of vfix_app
+  | Vcofix of vcofix
+  | Vcofix_app of vcofix_app
+  | Vconstr_const of int
+  | Vconstr_block of vblock
+  | Vatom_stk of atom * stack
+
+(* Constructors *)
+val val_of_str_const : structured_constant -> values
+
+val val_of_rel : int -> values 
+val val_of_rel_def : int -> values -> values 
+
+val val_of_named : identifier -> values
+val val_of_named_def : identifier -> values -> values
+
+val val_of_constant : constant -> values 
+val val_of_constant_def : constant -> values -> values
+
+(* Destructors *)
+val whd_val : values -> whd
+
+(* Product *)
+val dom : vprod -> values
+val codom : vprod -> vfun
+(* Function *)
+val body_of_vfun : int -> vfun -> values 
+val decompose_vfun2  : int -> vfun -> vfun -> int * values * values
+(* Fix *)
+val fix : vfix_app -> vfix
+val args_of_fix : vfix_app -> arguments
+val fix_init : vfix -> int
+val fix_ndef : vfix -> int 
+val rec_args : vfix -> int array 
+val check_fix : vfix -> vfix -> bool
+val bodies_of_fix : int -> vfix -> vfun array
+val types_of_fix : vfix -> values array
+(* CoFix *)
+val cofix : vcofix_app -> vcofix
+val args_of_cofix : vcofix_app -> arguments
+val cofix_init : vcofix -> int 
+val cofix_ndef : vcofix -> int
+val check_cofix : vcofix -> vcofix -> bool
+val bodies_of_cofix : int -> vcofix -> values array
+val types_of_cofix : vcofix -> values array
+(* Block *)
+val btag : vblock -> int
+val bsize : vblock -> int
+val bfield : vblock -> int -> values
+(* Switch *)
+val eq_tbl : vswitch -> vswitch -> bool
+val case_info : vswitch -> case_info
+val type_of_switch : vswitch -> values
+val branch_of_switch : int -> vswitch -> (int * values) array
+(* Arguments *)  
+val nargs : arguments -> int
+val arg : arguments -> int -> values
+
+(* Evaluation *)
+val whd_stack : values -> stack -> whd
+
+
+