Changement dans les boxed values .

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

20 files changed, 402 insertions, 145 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 55ad3aa5e..446c76498 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -39,6 +39,26 @@ value coq_makeaccu (value i) {
   return (value)res;
 }
 
+value coq_accucond (value i) {
+  code_t q;
+  code_t res = coq_stat_alloc(8);
+  q = res;
+  *q++ = (opcode_t)(coq_instr_table[ACCUMULATECOND] - coq_instr_base);
+  *q = (opcode_t)Int_val(i);
+  return (value)res;
+}
+
+value coq_is_accumulate_code(value code){
+  code_t q;
+  int res;
+  q = (code_t)code;
+  res = 
+    (*q == (opcode_t)(coq_instr_table[ACCUMULATECOND] - coq_instr_base))
+    || 
+    (*q == (opcode_t)(coq_instr_table[ACCUMULATE] - coq_instr_base));
+  return Val_bool(res);
+}
+
 value coq_pushpop (value i) {
   code_t res;
   int n;
@@ -91,9 +111,10 @@ code_t coq_thread_code (code_t code, asize_t len){
     case GRAB: case COGRAB: 
     case OFFSETCLOSURE: case PUSHOFFSETCLOSURE: 
     case GETGLOBAL: case PUSHGETGLOBAL: 
-    case GETGLOBALBOXED: case PUSHGETGLOBALBOXED: 
+      /*    case GETGLOBALBOXED: case PUSHGETGLOBALBOXED: */
     case MAKEBLOCK1: case MAKEBLOCK2: case MAKEBLOCK3: case MAKEACCU:
     case CONSTINT: case PUSHCONSTINT: case GRABREC: case PUSHFIELD:
+    case ACCUMULATECOND:
     *q++ = *p++;
     break;
     
@@ -148,6 +169,25 @@ value coq_makeaccu (value i) {
   return (value)res;
 }
 
+value coq_accucond (value i) {
+  code_t q;
+  code_t res = coq_stat_alloc(8);
+  q = res;
+  *q++ = (opcode_t)ACCUMULATECOND;
+  *q = (opcode_t)Int_val(i);
+  return (value)res;
+}
+
+value coq_is_accumulate_code(value code){
+  code_t q;
+  int res;
+  q = (code_t)code;
+  res = 
+    (*q == ACCUMULATECOND) || 
+    (*q == ACCUMULATE);
+  return Val_bool(res);
+}
+
 value coq_pushpop (value i) {
   code_t res;
   int n;
diff --git a/kernel/byterun/coq_fix_code.h b/kernel/byterun/coq_fix_code.h
index bceb104e9..e3296c0da 100644
--- a/kernel/byterun/coq_fix_code.h
+++ b/kernel/byterun/coq_fix_code.h
@@ -27,4 +27,6 @@ extern char * coq_instr_base;
 value coq_tcode_of_code(value code, value len);
 value coq_makeaccu (value i);
 value coq_pushpop (value i);
+value coq_accucond (value i);
+value coq_is_accumulate_code(value code);
 #endif /* _COQ_FIX_CODE_ */
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 2c23a4c89..d3b07526f 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -28,13 +28,12 @@ enum instructions {
   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
+  ACCUMULATE, ACCUMULATECOND, STOP
 };
 
 #endif /* _COQ_INSTRUCT_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index a5f6f01d7..692baa7e7 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -51,10 +51,20 @@ sp is a local copy of the global variable extern_sp. */
 #    endif
 #  endif
 #else 
-#  define Instruct(name) case name: print_instr(name);
+#  define Instruct(name) case name:
 #  define Next break
 #endif 
 
+/*#define _COQ_DEBUG_*/
+
+#ifdef _COQ_DEBUG_ 
+#   define print_instr(s) if (drawinstr) printf("%s\n",s)
+#   define print_int(i)   if (drawinstr) printf("%d\n",i)
+# else 
+#   define print_instr(s) 
+#   define print_int(i) 
+#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; }
@@ -154,8 +164,6 @@ value coq_interprete
 #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;
@@ -168,8 +176,6 @@ value coq_interprete
 #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;
@@ -183,107 +189,138 @@ value coq_interprete
 /* Basic stack operations */
       
       Instruct(ACC0){
+	print_instr("ACC0");
 	accu = sp[0]; Next;
       }
       Instruct(ACC1){
+	print_instr("ACC1");
 	accu = sp[1]; Next;
       }
       Instruct(ACC2){
+	print_instr("ACC2");
 	accu = sp[2]; Next;
       }
       Instruct(ACC3){
+	print_instr("ACC3");
 	accu = sp[3]; Next;
       }
       Instruct(ACC4){
+	print_instr("ACC4");
 	accu = sp[4]; Next;
       }
       Instruct(ACC5){
+	print_instr("ACC5");
 	accu = sp[5]; Next;
       }
       Instruct(ACC6){
+	print_instr("ACC6");
 	accu = sp[6]; Next;
       }
       Instruct(ACC7){
+	print_instr("ACC7");
         accu = sp[7]; Next;
       }      
       Instruct(PUSH){
+	print_instr("PUSH");
 	*--sp = accu; Next;
       }
       Instruct(PUSHACC0) {
+	print_instr("PUSHACC0");
         *--sp = accu; Next;
       }
       Instruct(PUSHACC1){
+	print_instr("PUSHACC1");
         *--sp = accu; accu = sp[1]; Next;
       }
       Instruct(PUSHACC2){
+	print_instr("PUSHACC2");
         *--sp = accu; accu = sp[2]; Next;
       }
       Instruct(PUSHACC3){
+	print_instr("PUSHACC3");
 	*--sp = accu; accu = sp[3]; Next;
       }
       Instruct(PUSHACC4){
+	print_instr("PUSHACC4");
 	*--sp = accu; accu = sp[4]; Next;
       }
       Instruct(PUSHACC5){
+	print_instr("PUSHACC5");
 	*--sp = accu; accu = sp[5]; Next;
       }
       Instruct(PUSHACC6){
+	print_instr("PUSHACC5");
 	*--sp = accu; accu = sp[6]; Next;
       }
       Instruct(PUSHACC7){
+	print_instr("PUSHACC7");
 	*--sp = accu; accu = sp[7]; Next;
       }
       Instruct(PUSHACC){
+	print_instr("PUSHACC");
 	*--sp = accu;
       }
       /* Fallthrough */
       
       Instruct(ACC){
+	print_instr("ACC");
 	accu = sp[*pc++];
         Next;
       }
       
       Instruct(POP){
+	print_instr("POP");
 	sp += *pc++;
 	Next;
       }
       /* Access in heap-allocated environment */
       
       Instruct(ENVACC1){
+	print_instr("ENVACC1");
 	accu = Field(coq_env, 1); Next;
       }
       Instruct(ENVACC2){
+	print_instr("ENVACC2");
 	accu = Field(coq_env, 2); Next;
       }
       Instruct(ENVACC3){
+	print_instr("ENVACC3");
 	accu = Field(coq_env, 3); Next;
       }
       Instruct(ENVACC4){
+	print_instr("ENVACC4");
 	accu = Field(coq_env, 4); Next;
       }
       Instruct(PUSHENVACC1){
+	print_instr("PUSHENVACC1");
 	*--sp = accu; accu = Field(coq_env, 1); Next;
       }
       Instruct(PUSHENVACC2){
+	print_instr("PUSHENVACC2");
 	*--sp = accu; accu = Field(coq_env, 2); Next;
       }
       Instruct(PUSHENVACC3){
+	print_instr("PUSHENVACC3");
 	*--sp = accu; accu = Field(coq_env, 3); Next;
       }
       Instruct(PUSHENVACC4){
+	print_instr("PUSHENVACC4");
 	*--sp = accu; accu = Field(coq_env, 4); Next;
       }
       Instruct(PUSHENVACC){
+	print_instr("PUSHENVACC");
 	*--sp = accu;
       }
       /* Fallthrough */
       Instruct(ENVACC){
+	print_instr("ENVACC");
 	accu = Field(coq_env, *pc++);
         Next;
       }
       /* Function application */
       
       Instruct(PUSH_RETADDR) {
+	print_instr("PUSH_RETADDR");
 	sp -= 3;
 	sp[0] = (value) (pc + *pc);
 	sp[1] = coq_env;
@@ -293,6 +330,7 @@ value coq_interprete
 	Next;
       }
       Instruct(APPLY) {
+	print_instr("APPLY");
 	coq_extra_args = *pc - 1;
 	pc = Code_val(accu);
 	coq_env = accu;
@@ -300,6 +338,7 @@ value coq_interprete
       }
       Instruct(APPLY1) {
 	value arg1 = sp[0];
+	print_instr("APPLY1");
 	sp -= 3;
 	sp[0] = arg1;
 	sp[1] = (value)pc;
@@ -313,6 +352,7 @@ value coq_interprete
       Instruct(APPLY2) {
 	value arg1 = sp[0];
 	value arg2 = sp[1];
+	print_instr("APPLY2");
 	sp -= 3;
 	sp[0] = arg1;
 	sp[1] = arg2;
@@ -328,6 +368,7 @@ value coq_interprete
 	value arg1 = sp[0];
 	value arg2 = sp[1];
 	value arg3 = sp[2];
+	print_instr("APPLY3");
 	sp -= 3;
 	sp[0] = arg1;
 	sp[1] = arg2;
@@ -346,6 +387,7 @@ value coq_interprete
 	int slotsize = *pc;
 	value * newsp;
 	int i;
+	print_instr("APPTERM");
 	/* 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;
@@ -358,6 +400,7 @@ value coq_interprete
       }
       Instruct(APPTERM1) {
 	value arg1 = sp[0];
+	print_instr("APPTERM1");
 	sp = sp + *pc - 1;
 	sp[0] = arg1;
 	pc = Code_val(accu);
@@ -367,6 +410,7 @@ value coq_interprete
       Instruct(APPTERM2) {
 	value arg1 = sp[0];
 	value arg2 = sp[1];
+	print_instr("APPTERM2");
 	sp = sp + *pc - 2;
 	sp[0] = arg1;
 	sp[1] = arg2;
@@ -379,6 +423,7 @@ value coq_interprete
 	value arg1 = sp[0];
 	value arg2 = sp[1];
 	value arg3 = sp[2];
+	print_instr("APPTERM3");
 	sp = sp + *pc - 3;
 	sp[0] = arg1;
 	sp[1] = arg2;
@@ -390,6 +435,7 @@ value coq_interprete
       }
       
       Instruct(RETURN) {
+	print_instr("RETURN");
 	sp += *pc++;
 	if (coq_extra_args > 0) {
 	  coq_extra_args--;
@@ -407,6 +453,7 @@ value coq_interprete
       Instruct(RESTART) {
 	int num_args = Wosize_val(coq_env) - 2;
 	int i;
+	print_instr("RESTART");
 	sp -= num_args;
 	for (i = 0; i < num_args; i++) sp[i] = Field(coq_env, i + 2);
 	coq_env = Field(coq_env, 1);
@@ -416,6 +463,8 @@ value coq_interprete
       
       Instruct(GRAB) {
 	int required = *pc++;
+	print_instr("GRAB");
+	/*	printf("GRAB %d\n",required); */
 	if (coq_extra_args >= required) {
 	  coq_extra_args -= required;
 	} else {
@@ -436,10 +485,13 @@ value coq_interprete
 
       Instruct(COGRAB){
 	int required = *pc++;
+	print_instr("COGRAB");
 	if(forcable == Val_true) {
+	  print_instr("true");
 	  /* L'instruction précédante est FORCE */
 	  if (coq_extra_args > 0) coq_extra_args--;
 	  pc++;
+	  forcable = Val_false;
 	} else { /* L'instruction précédante est APPLY */
 	  mlsize_t num_args, i;
 	  num_args = 1 + coq_extra_args; /* arg1 + extra args */
@@ -457,6 +509,7 @@ value coq_interprete
       }
       Instruct(GRABREC) { 
 	int rec_pos = *pc++; /* commence a zero */
+	print_instr("GRABREC");
 	if (rec_pos <= coq_extra_args && !Is_accu(sp[rec_pos])) {
 	  pc++;/* On saute le Restart */
 	} else {
@@ -506,6 +559,8 @@ value coq_interprete
       Instruct(CLOSURE) {
 	int nvars = *pc++;
 	int i;
+	print_instr("CLOSURE");
+	print_int(nvars);
 	if (nvars > 0) *--sp = accu;
 	Alloc_small(accu, 1 + nvars, Closure_tag);
 	Code_val(accu) = pc + *pc;
@@ -521,6 +576,7 @@ value coq_interprete
 	int start = *pc++;
 	int i;
 	value * p;
+	print_instr("CLOSUREREC");
 	if (nvars > 0) *--sp = accu;
 	/* construction du vecteur de type */
 	Alloc_small(accu, nfuncs, 0);
@@ -551,51 +607,52 @@ value coq_interprete
       }
      
       Instruct(PUSHOFFSETCLOSURE) {
+	print_instr("PUSHOFFSETCLOSURE");
 	*--sp = accu;
       } /* fallthrough */
       Instruct(OFFSETCLOSURE) {
+	print_instr("OFFSETCLOSURE");
 	accu = coq_env + *pc++ * sizeof(value); Next;
       }
       Instruct(PUSHOFFSETCLOSUREM2) {
+	print_instr("PUSHOFFSETCLOSUREM2");
 	*--sp = accu;
       } /* fallthrough */
       Instruct(OFFSETCLOSUREM2) {
+	print_instr("OFFSETCLOSUREM2");
 	accu = coq_env - 2 * sizeof(value); Next;
       }
       Instruct(PUSHOFFSETCLOSURE0) {
+	print_instr("PUSHOFFSETCLOSURE0");
 	*--sp = accu; 
       }/* fallthrough */
       Instruct(OFFSETCLOSURE0) {
+	print_instr("OFFSETCLOSURE0");
 	accu = coq_env; Next;
       }
       Instruct(PUSHOFFSETCLOSURE2){
+	print_instr("PUSHOFFSETCLOSURE2");
 	*--sp = accu; /* fallthrough */
       }
       Instruct(OFFSETCLOSURE2) {
+	print_instr("OFFSETCLOSURE2");
 	accu = coq_env + 2 * sizeof(value); Next;
       }
 
 /* Access to global variables */
 
       Instruct(PUSHGETGLOBAL) {
+	print_instr("PUSHGETGLOBAL");
 	*--sp = accu;
       }
       /* Fallthrough */
       Instruct(GETGLOBAL){
+	print_instr("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) {
@@ -603,6 +660,7 @@ value coq_interprete
 	tag_t tag = *pc++;
 	mlsize_t i;
 	value block;
+	print_instr("MAKEBLOCK");
 	Alloc_small(block, wosize, tag);
 	Field(block, 0) = accu;
 	for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
@@ -613,6 +671,7 @@ value coq_interprete
 	
 	tag_t tag = *pc++;
 	value block;
+	print_instr("MAKEBLOCK1");
 	Alloc_small(block, 1, tag);
 	Field(block, 0) = accu;
 	accu = block;
@@ -622,6 +681,7 @@ value coq_interprete
 	
 	tag_t tag = *pc++;
 	value block;
+	print_instr("MAKEBLOCK2");
 	Alloc_small(block, 2, tag);
 	Field(block, 0) = accu;
 	Field(block, 1) = sp[0];
@@ -632,6 +692,7 @@ value coq_interprete
       Instruct(MAKEBLOCK3) {
 	tag_t tag = *pc++;
 	value block;
+	print_instr("MAKEBLOCK3");
 	Alloc_small(block, 3, tag);
 	Field(block, 0) = accu;
 	Field(block, 1) = sp[0];
@@ -647,7 +708,9 @@ value coq_interprete
 	
 /* Branches and conditional branches */
       Instruct(FORCE) {
+	print_instr("FORCE");
 	if (Is_block(accu) && Tag_val(accu) == Closure_tag) {
+	  forcable = Val_true;
 	  /* On pousse l'addresse de retour et l'argument */
 	  sp -= 3;
 	  sp[0] = (value) (pc);
@@ -658,6 +721,9 @@ value coq_interprete
 	  pc = Code_val(accu);
 	  coq_env = accu;
 	  goto check_stacks;
+	} else {
+	  if (Is_block(accu)) print_int(Tag_val(accu));
+	  else print_instr("Not a block");
 	}
 	Next;
       }
@@ -665,11 +731,17 @@ value coq_interprete
     
       Instruct(SWITCH) {
 	uint32 sizes = *pc++;
+	print_instr("SWITCH");
+	print_int(sizes);
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
+	  print_instr("block");
+	  print_int(index);
 	  pc += pc[(sizes & 0xFFFF) + index];
 	} else {
 	  long index = Long_val(accu);
+	  print_instr("constant");
+	  print_int(index);
 	  pc += pc[index];
 	}
 	  Next;
@@ -677,6 +749,7 @@ value coq_interprete
       Instruct(PUSHFIELD){
 	int i;
 	int size = *pc++;
+	print_instr("PUSHFIELD");
 	sp -= size;
 	for(i=0;i<size;i++)sp[i] = Field(accu,i);
 	Next;
@@ -686,6 +759,7 @@ value coq_interprete
 	mlsize_t sz;
 	int i, annot;
 	code_t typlbl,swlbl;
+	print_instr("MAKESWITCHBLOCK");
 	typlbl = (code_t)pc + *pc; 
 	pc++;
 	swlbl = (code_t)pc + *pc; 
@@ -725,6 +799,7 @@ value coq_interprete
       /* Stack checks */
       
     check_stacks:
+      print_instr("check_stacks");
       if (sp < coq_stack_threshold) {
 	coq_sp = sp;
 	realloc_coq_stack(Coq_stack_threshold);
@@ -736,32 +811,42 @@ value coq_interprete
 /* Integer constants */
 
       Instruct(CONST0){
+	print_instr("CONST0");
 	accu = Val_int(0); Next;}
       Instruct(CONST1){
+	print_instr("CONST1");
 	accu = Val_int(1); Next;}
       Instruct(CONST2){
+	print_instr("CONST2");
 	accu = Val_int(2); Next;}
       Instruct(CONST3){
+	print_instr("CONST3");
 	accu = Val_int(3); Next;}
       
       Instruct(PUSHCONST0){
+	print_instr("PUSHCONST0");
 	*--sp = accu; accu = Val_int(0); Next;
       }
       Instruct(PUSHCONST1){
+	print_instr("PUSHCONST1");
 	*--sp = accu; accu = Val_int(1); Next;
       }
       Instruct(PUSHCONST2){
+	print_instr("PUSHCONST2");
 	*--sp = accu; accu = Val_int(2); Next;
       }
       Instruct(PUSHCONST3){
+	print_instr("PUSHCONST3");
 	*--sp = accu; accu = Val_int(3); Next;
       }
 
       Instruct(PUSHCONSTINT){
+	print_instr("PUSHCONSTINT");
 	*--sp = accu;
       }
       /* Fallthrough */
       Instruct(CONSTINT) {
+	print_instr("CONSTINT");
 	accu = Val_int(*pc);
 	pc++;
 	Next;
@@ -770,12 +855,34 @@ value coq_interprete
 /* Debugging and machine control */
 
       Instruct(STOP){
+	print_instr("STOP");
 	coq_sp = sp;
 	return accu;
       }
       
+      Instruct(ACCUMULATECOND) {
+	int i, num;
+	print_instr("ACCUMULATECOND");
+	num = *pc;
+	pc++;
+	if (Field(coq_global_boxed, num) == Val_false || coq_all_transp) {
+	  /*	  printf ("false\n");
+	    printf ("tag = %d", Tag_val(Field(accu,1))); */
+	  num = Wosize_val(coq_env);
+	  for(i = 2; i < num; i++) *--sp = Field(accu,i);
+	  coq_extra_args = coq_extra_args + (num - 2);
+	  coq_env = Field(Field(accu,1),1);
+	  pc = Code_val(coq_env);
+	  accu = coq_env;
+	  /*	  printf ("end\n"); */
+	  Next;
+	};
+	/*	printf ("true\n"); */
+      }
+
       Instruct(ACCUMULATE) {
 	mlsize_t i, size;
+	print_instr("ACCUMULATE");
 	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);
@@ -786,10 +893,11 @@ value coq_interprete
 	coq_extra_args = Long_val(sp[2]);
 	sp += 3;
 	Next;
-      }
-      
+      }  
+            
       Instruct(MAKEACCU) {
 	int i;
+	print_instr("MAKEACCU");
 	Alloc_small(accu, coq_extra_args + 3, Accu_tag);
 	Code_val(accu) = accumulate;
 	Field(accu,1) = Field(coq_atom_tbl, *pc);
@@ -802,6 +910,7 @@ value coq_interprete
       }
      
       Instruct(MAKEPROD) {
+	print_instr("MAKEPROD");
 	*--sp=accu;
 	Alloc_small(accu,2,0);
 	Field(accu, 0) = sp[0];
@@ -820,6 +929,7 @@ value coq_interprete
 }
 
 value coq_push_ra(value tcode) { 
+  print_instr("push_ra");
   coq_sp -= 3;
   coq_sp[0] = (value) tcode;
   coq_sp[1] = Val_unit;
@@ -828,6 +938,7 @@ value coq_push_ra(value tcode) {
 }
 
 value coq_push_val(value v) {
+  print_instr("push_val");
   *--coq_sp = v;
   return Val_unit;
 }
@@ -836,6 +947,7 @@ value coq_push_arguments(value args) {
   int nargs,i;
   nargs = Wosize_val(args) - 2;
   coq_sp -= nargs;
+  print_instr("push_args");print_int(nargs);
   for(i = 0; i < nargs; i++) coq_sp[i] = Field(args, i+2);
   return Val_unit;
 }
@@ -844,11 +956,13 @@ 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);
+  print_instr("push_vstack");print_int(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) {
+  print_instr("coq_interprete");
   return coq_interprete((code_t)tcode, a, e, Long_val(ea));
 }
 
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 233397b02..f94d2fb9e 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -25,11 +25,11 @@ asize_t coq_max_stack_size = Coq_max_stack_size;
 
 
 value coq_global_data;
-value coq_global_transp;
 value coq_global_boxed;
-int default_transp;
+int coq_all_transp;
 value coq_atom_tbl;
 
+int drawinstr;
 /* interp state */
 
 long coq_saved_sp_offset;
@@ -68,7 +68,6 @@ 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 */
@@ -92,20 +91,17 @@ void init_coq_stack()
 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;
-  
+void init_coq_global_boxed(long requested_size)
+{
+  int i;
   coq_global_boxed = alloc_shr(requested_size, 0);
   for (i = 0; i < requested_size; i++) 
-    Field (coq_global_boxed, i) = Val_unit;
+    Field (coq_global_boxed, i) = Val_true;
 }
 
 void init_coq_atom_tbl(long requested_size){
@@ -130,11 +126,14 @@ value init_coq_vm(value unit) /* ML */
   else {
 
     /* Allocate the table of global and the stack */
+    drawinstr=0;
     init_coq_stack();
     init_coq_global_data(Coq_global_data_Size);
+    init_coq_global_boxed(40);
     init_coq_atom_tbl(40);
     /* Initialing the interpreter */
-    forcable = Val_true;
+    coq_all_transp = 0;
+    forcable = Val_false;
     init_coq_interpreter();
     
     /* Some predefined pointer code */
@@ -189,11 +188,6 @@ 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;
@@ -221,23 +215,16 @@ value realloc_coq_global_data(value size)           /* ML */
 value realloc_coq_global_boxed(value size)           /* ML */
 {
   mlsize_t requested_size, actual_size, i;
-  value new_global_transp, new_global_boxed;
+  value new_global_boxed;
   requested_size = Long_val(size);
-  actual_size = Wosize_val(coq_global_transp);
+  actual_size = Wosize_val(coq_global_boxed);
   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);
+    for (i = 0; i < actual_size; i++)
+      initialize(&Field(new_global_boxed, i), Field(coq_global_boxed, i));
+    for (i = actual_size; i < requested_size; i++)
       Field (new_global_boxed, i) = Val_long (0);
-    }
-    coq_global_transp = new_global_transp;
     coq_global_boxed = new_global_boxed;
   }
   return Val_unit;
@@ -254,17 +241,33 @@ value realloc_coq_atom_tbl(value size)            /* ML */
     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++){
+    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;
+
+value coq_set_transp_value(value transp)
+{
+  coq_all_transp = (transp == Val_true);
+  return Val_unit;
+}
+
+value get_coq_transp_value(value unit)
+{
+  return Val_bool(coq_all_transp);
+}
+
+value coq_set_drawinstr(value unit)
+{
+  drawinstr = 1;
   return Val_unit;
 }
 
+value coq_set_forcable (value unit)
+{
+  forcable = Val_true;
+  return Val_unit;
+}
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 0884f06a8..7c96e684e 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -35,10 +35,11 @@ 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 int coq_all_transp;
 extern value coq_atom_tbl;
+
+extern int drawinstr;
 /* interp state */
 
 extern value * coq_sp;
@@ -57,12 +58,13 @@ 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 */
-
+value coq_set_transp_value(value transp); /* ML */
+value get_coq_transp_value(value unit); /* ML */
 #endif /* _COQ_MEMORY_ */
 
 
+value coq_set_drawinstr(value unit);
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 48331a687..0d4a246a0 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -61,4 +61,60 @@ type fv_elem = FVnamed of identifier | FVrel of int
 type fv = fv_elem array
 
 
+(* --- Pretty print *)
+open Format
+let rec instruction ppf = function
+  | Klabel lbl -> fprintf ppf "L%i:" lbl
+  | Kacc n -> fprintf ppf "\tacc %i" n
+  | Kenvacc n -> fprintf ppf "\tenvacc %i" n
+  | Koffsetclosure n -> fprintf ppf "\toffsetclosure %i" n
+  | Kpush -> fprintf ppf "\tpush"
+  | Kpop n -> fprintf ppf "\tpop %i" n
+  | Kpush_retaddr lbl -> fprintf ppf "\tpush_retaddr L%i" lbl
+  | Kapply n -> fprintf ppf "\tapply %i" n
+  | Kappterm(n, m) ->
+      fprintf ppf "\tappterm %i, %i" n m
+  | Kreturn n -> fprintf ppf "\treturn %i" n
+  | Kjump -> fprintf ppf "\tjump"
+  | Krestart -> fprintf ppf "\trestart"
+  | Kgrab n -> fprintf ppf "\tgrab %i" n
+  | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n
+  | Kcograb n -> fprintf ppf "\tcograb %i" n
+  | Kclosure(lbl, n) ->
+      fprintf ppf "\tclosure L%i, %i" lbl n
+  | Kclosurerec(fv,init,lblt,lblb) ->
+      fprintf ppf "\tclosurerec";
+      fprintf ppf "%i , %i, " fv init;
+      print_string "types = ";
+      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
+      print_string " bodies = ";
+      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
+                   (* nb fv, init, lbl types, lbl bodies *)
+  | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_kn id)
+  | Kconst cst ->
+      fprintf ppf "\tconst"
+  | Kmakeblock(n, m) ->
+      fprintf ppf "\tmakeblock %i, %i" n m
+  | Kmakeprod -> fprintf ppf "\tmakeprod"
+  | Kmakeswitchblock(lblt,lbls,_,sz) ->
+      fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz
+  | Kforce -> fprintf ppf "\tforce"
+  | Kswitch(lblc,lblb) -> 
+      fprintf ppf "\tswitch";
+      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc;
+      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
+  | Kpushfield n -> 
+      fprintf ppf "\tpushfield %i" n
+  | Kstop -> fprintf ppf "\tstop"
+  | Ksequence (c1,c2) ->
+      fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2 
 
+and instruction_list ppf = function
+    [] -> ()
+  | Klabel lbl :: il ->
+      fprintf ppf "L%i:%a" lbl instruction_list il
+  | instr :: il ->
+      fprintf ppf "%a@ %a" instruction instr instruction_list il
+ 
+let draw_instr c =
+  fprintf std_formatter "@[<v 0>%a@]" instruction_list c
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 84882358a..a996f7505 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -58,3 +58,4 @@ type fv_elem = FVnamed of identifier | FVrel of int
 
 type fv = fv_elem array
 
+val draw_instr : bytecodes -> unit
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 033f07319..022f913ba 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -48,7 +48,6 @@ let push_local sz r =
     nb_stack = r.nb_stack + 1;
     in_stack = (sz + 1) :: r.in_stack }
 
-
 (* Table de relocation initiale *)
 let empty () = 
   { nb_stack = 0; in_stack = [];
@@ -128,7 +127,7 @@ let label_code = function
 
 let make_branch cont =
   match cont with
-  | (Kreturn _ as return) :: _ -> return, cont
+  | (Kreturn _ as return) :: cont' -> return, cont'
   | Klabel lbl as b :: _ -> b, cont
   | _ -> let b = Klabel(Label.create()) in b,b::cont
 
@@ -467,8 +466,11 @@ let compile env c =
   let reloc = empty () in
   let init_code = compile_constr reloc c 0 [Kstop] in
   let fv = List.rev (!(reloc.in_env).fv_rev) in
+  if Options.print_bytecodes() then 
+    (draw_instr init_code; draw_instr !fun_code);
   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
@@ -477,7 +479,16 @@ let compile_constant_body env kn body opaque boxed =
       let body = Declarations.force sb in
       match kind_of_term body with
       | Const kn' -> BCallias (get_allias env kn')
+      | Construct _ ->
+	  let res = compile env body in
+	  let to_patch = to_memory res in
+	  BCdefined (false,to_patch)
+
       | _ -> 
-	  let to_patch = to_memory (compile env body) in
-	  BCdefined (boxed,to_patch)
+	  let res = compile env body in
+	  let to_patch = to_memory res in
+	  (*if Options.print_bytecodes() then 
+	    (let init,fun_code,_= res in
+	    draw_instr init; draw_instr fun_code);*)
+	  BCdefined (boxed && Options.boxed_definitions (),to_patch)
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index ab1f00d11..421949163 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -17,26 +17,7 @@ let patch_int buff pos n =
   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)
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index fed577158..438da15dd 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -15,7 +15,6 @@ 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
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 3cc6f49d5..402a0fb97 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -43,8 +43,7 @@ let set_global v =
    [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"
+external global_boxed : unit -> bool 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"
@@ -54,14 +53,19 @@ let check_global_boxed n =
   
 let num_boxed = ref 0
 
-let set_boxed kn v = 
+let boxed_tbl = Hashtbl.create 53
+
+let cst_opaque = ref KNpred.full
+
+let is_opaque kn = KNpred.mem kn !cst_opaque
+
+let set_global_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;
+  (global_boxed()).(n) <- (is_opaque kn);
+  Hashtbl.add boxed_tbl kn n ;
   incr num_boxed;
-  n
+  set_global (val_of_constant_def n kn v)
 
 (* table pour les structured_constant et les annotations des switchs *)
 
@@ -99,21 +103,19 @@ let rec slot_for_getglobal env kn =
     | BCdefined(boxed,(code,pl,fv)) -> 
 	let v = eval_to_patch env (code,pl,fv) in
    	let pos = 
-	  if boxed then set_boxed kn v 
+	  if boxed then set_global_boxed kn v 
 	  else set_global v in
-	let bpos = boxed,pos in
-	set_pos_constant ck bpos;
-	bpos
+	set_pos_constant ck pos;
+	pos
     | BCallias kn' ->
-	let bpos = slot_for_getglobal env kn' in
-	set_pos_constant ck bpos;
-	bpos
+	let pos = slot_for_getglobal env kn' in
+	set_pos_constant ck pos;
+	pos
     | 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  
+	set_pos_constant ck pos;
+	pos  
 
 and slot_for_fv env fv=
   match fv with
@@ -148,7 +150,7 @@ and eval_to_patch env (buff,pl,fv) =
     | 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)
+	patch_int buff pos (slot_for_getglobal env kn)
   in 
   List.iter patch pl;
   let nfv = Array.length fv in
@@ -160,4 +162,14 @@ and val_of_constr env c =
   let (_,fun_code,_ as ccfv) = compile env c in
   eval_to_patch env (to_memory ccfv)
  
-  
+let set_transparent_const kn =
+  cst_opaque := KNpred.remove kn !cst_opaque;
+  List.iter (fun n -> (global_boxed()).(n) <- false) 
+    (Hashtbl.find_all boxed_tbl kn)
+
+let set_opaque_const kn =
+  cst_opaque := KNpred.add kn !cst_opaque;
+  List.iter (fun n -> (global_boxed()).(n) <- true) 
+    (Hashtbl.find_all boxed_tbl kn)
+
+
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 8bb0b890c..5fafbac49 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -4,3 +4,5 @@ open Environ
 
 val val_of_constr : env -> constr -> values 
 
+val set_opaque_const      : kernel_name -> unit
+val set_transparent_const : kernel_name -> unit
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 3563a1340..d9569bca6 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -23,7 +23,7 @@ type compilation_unit_name = dir_path * checksum
 
 type global = Constant | Inductive
 
-type key = (bool*int) option ref 
+type key = int option ref 
 type constant_key = constant_body * key
  
 type engagement = ImpredicativeSet
diff --git a/kernel/environ.mli b/kernel/environ.mli
index d570655ee..5be23b490 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -112,9 +112,9 @@ type constant_key
 exception NotEvaluated
 exception AllReadyEvaluated
 
-val constant_key_pos : constant_key -> bool*int  
+val constant_key_pos : constant_key -> int  
 val constant_key_body : constant_key -> constant_body
-val set_pos_constant : constant_key -> (bool*int) -> unit
+val set_pos_constant : constant_key -> int -> unit
 
 val lookup_constant_key : constant -> env -> constant_key
 val lookup_constant    : constant -> env -> constant_body
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1ca0fec4a..7e5e91944 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -514,7 +514,7 @@ let import (dp,mb,depends,engmt) digest senv =
 	  loads = (mp,mb)::senv.loads }
 
 
-(** Remove the body of opaque constants in modules *)
+(* Remove the body of opaque constants in modules *)
  
 let rec lighten_module mb =
   { mb with
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 41817c3e0..841bed98f 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -12,7 +12,7 @@ open Univ
 open Cbytecodes
 
 
-(**** Test la structure des piles ****)
+(* Test la structure des piles *)
 
 let compare_zipper z1 z2 =
   match z1, z2 with
@@ -29,7 +29,7 @@ let rec compare_stack stk1 stk2 =
       else false
   | _, _ -> false 
 
-(**** Conversion ****)
+(* Conversion *)
 let conv_vect fconv vect1 vect2 cu =
   let n = Array.length vect1 in
   if n = Array.length vect2 then
@@ -247,7 +247,7 @@ let vconv pb env t1 t2 =
 let _ = Reduction.set_vm_conv_cmp vconv
 
 (*******************************************)
-(**** Calcul de la forme normal d'un terme *)
+(* Calcul de la forme normal d'un terme    *)
 (*******************************************)
 
 let crazy_type = mkSet 
@@ -271,7 +271,7 @@ let invert_tag cst tag reloc_tbl =
       else ()
     done;raise Not_found 
   with Find_at j -> (j+1)   
-             (*** Argggg, ces constructeurs de ... qui commencent a 1*)
+             (* Argggg, ces constructeurs de ... qui commencent a 1*)
 
 (* Build the substitution that replaces Rels by the appropriate 
   inductives *)
@@ -289,7 +289,7 @@ let constructor_instantiate mind mib params ctyp =
   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 sp = List.rev (Array.to_list params) in substl sp ctyp2
   
 let destApplication t =
   try destApplication t 
@@ -358,7 +358,7 @@ let build_branches_type (mind,_ as ind) mib mip params dep p rtbl =
     decl, codom
   in Array.mapi build_one_branch mip.mind_nf_lc
 
-(** La fonction de normalisation *)
+(* La fonction de normalisation *)
 
 let rec nf_val env v t = nf_whd env (whd_val v) t 
 
@@ -398,9 +398,8 @@ and nf_whd env whd typ =
   | 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(Aiddef(idkey,v), stk) ->
+      nf_whd env (whd_stack v stk) typ
   | Vatom_stk(Aind ind, stk) ->
       nf_stk env (mkInd ind) (type_of_ind env ind) stk 
   | Vatom_stk(_,stk) -> assert false
@@ -421,7 +420,6 @@ and nf_stk env c t stk  =
       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
@@ -489,11 +487,19 @@ and nf_args env vargs t =
 and nf_bargs env b t =
   let t = ref t in
   let len = bsize b in
-  Array.init len 
+  let args = Array.create len crazy_type in
+  for i = 0 to len - 1 do
+    let _,dom,codom = decompose_prod env !t in
+    let c = nf_val env (bfield b i) dom in
+    args.(i) <- c;
+    t := subst1 c codom
+  done;
+  args
+(*  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) 
+      t := subst1 c codom; c) *) 
 
 and nf_fun env f typ =
   let k = nb_rel env in
@@ -527,11 +533,14 @@ and nf_cofix env cf =
   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 transp = transp_values () in
+  if not transp then set_transp_values true; 
   let v = val_of_constr env c in
   let c = nf_val env v t in
-  if not (transp_values ()) then swap_global_transp ();
+  if not transp then set_transp_values false; 
   c
   
 
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 21fd4601b..ea84a4ea8 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -12,3 +12,25 @@ val vconv : conv_pb -> types conversion_function
 (***********************************************************************)
 (*s Reduction functions *)
 val cbv_vm : env -> constr -> types -> constr
+
+
+
+
+
+val nf_val : env -> values -> types -> constr
+
+val nf_whd : env -> Vm.whd -> types -> constr
+
+val nf_stk : env -> constr -> types -> Vm.stack  -> constr
+       
+val nf_args : env -> Vm.arguments -> types ->  types * constr array
+
+val nf_bargs : env -> Vm.vblock -> types -> constr array
+
+val nf_fun : env -> Vm.vfun -> types -> constr
+
+val nf_fix : env -> Vm.vfix -> constr 
+  
+val nf_cofix : env -> Vm.vcofix -> constr
+
+  
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 80ecdf369..4482696ae 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -4,28 +4,13 @@ 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
-
 
+external set_drawinstr : unit -> unit = "coq_set_drawinstr"
 
 (******************************************)
 (* 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))
@@ -41,6 +26,9 @@ external init_vm : unit -> unit = "init_coq_vm"
 
 let _ = init_vm ()
 
+external transp_values : unit -> bool = "get_coq_transp_value"
+external set_transp_values : bool -> unit = "coq_set_transp_value"
+
 (*******************************************)
 (* Le code machine  ************************)
 (*******************************************)
@@ -51,6 +39,7 @@ let fun_code v = tcode_of_obj (field (repr v) 0)
 
 external mkAccuCode : int -> tcode = "coq_makeaccu"
 external mkPopStopCode : int -> tcode = "coq_pushpop"
+external mkAccuCond : int -> tcode = "coq_accucond"
 
 external offset_tcode : tcode -> int -> tcode = "coq_offset_tcode"
 external int_tcode : tcode -> int -> int = "coq_int_tcode"
@@ -58,6 +47,8 @@ external int_tcode : tcode -> int -> int = "coq_int_tcode"
 external accumulate : unit -> tcode = "accumulate_code"
 let accumulate = accumulate ()
 
+external is_accumulate : tcode -> bool = "coq_is_accumulate_code"
+
 let popstop_tbl =  ref (Array.init 30 mkPopStopCode) 
 
 let popstop_code i =
@@ -313,7 +304,12 @@ 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))
+let val_of_constant_def n c v = 
+  let res = Obj.new_block accu_tag 2 in
+  set_field res 0 (repr (mkAccuCond n));
+  set_field res 1 (repr (Aiddef(ConstKey c, v)));
+  val_of_obj res 
+
 
 
 (*************************************************)
@@ -326,8 +322,7 @@ let rec whd_accu a stk =
   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
+  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)
@@ -335,7 +330,6 @@ let rec whd_accu a stk =
 
 external kind_of_closure : t -> int = "coq_kind_of_closure"
 
-
 let whd_val : values -> whd =
   fun v -> 
     let o = repr v in 
@@ -343,7 +337,7 @@ let whd_val : values -> whd =
     else 
       let tag = tag o in
       if tag = accu_tag then
-	if fun_code o == accumulate then whd_accu (obj o) []
+	if is_accumulate (fun_code o) then whd_accu (obj o) []
 	else 
 	  if size o = 1 then Vsort(obj (field o 0))
 	  else Vprod(obj o)
@@ -405,8 +399,17 @@ let apply_fix_app vfa arg =
   push_arguments vargs;
   interprete (fun_code vf) (magic vf) (magic vf) (nargs vargs)
 
-let apply_switch sw arg =
+external set_forcable : unit -> unit = "coq_set_forcable"
+let force_cofix v =
+  match whd_val v with
+  | Vcofix _    | Vcofix_app _ ->
+      push_ra stop;
+      set_forcable ();
+      interprete (fun_code v) (magic v) (magic v) 0
+  | _ -> v
   
+let apply_switch sw arg =
+  let arg = force_cofix arg in
   let tc = sw.sw_annot.tailcall in
   if tc then 
     (push_ra stop;push_vstack sw.sw_stk)
diff --git a/kernel/vm.mli b/kernel/vm.mli
index d6e7f6eee..a4651cf7d 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -3,10 +3,11 @@ open Term
 open Cbytecodes
 open Cemitcodes
 
-(* option for virtual machine *)
+
+val set_drawinstr : unit -> unit
+
 val transp_values : unit -> bool
 val set_transp_values : bool -> unit
-val swap_global_transp : unit -> unit
 (* le code machine *)
 type tcode 
 
@@ -60,7 +61,7 @@ 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
+val val_of_constant_def : int -> constant -> values -> values
 
 (* Destructors *)
 val whd_val : values -> whd