Imported Upstream version 8.1~gammaupstream/8.1.gamma

7 files changed, 281 insertions, 144 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 4616580d..70648b44 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -27,31 +27,31 @@ void init_arity () {
   /* instruction with zero operand */
   arity[ACC0]=arity[ACC1]=arity[ACC2]=arity[ACC3]=arity[ACC4]=arity[ACC5]=
     arity[ACC6]=arity[ACC7]=arity[PUSH]=arity[PUSHACC0]=arity[PUSHACC1]=
-    arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=arity[PUSHACC6]=
-    arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]=arity[ENVACC3]=arity[ENVACC4]=
-    arity[PUSHENVACC1]=arity[PUSHENVACC2]=arity[PUSHENVACC3]=arity[PUSHENVACC4]=
-    arity[APPLY1]=arity[APPLY2]=arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
+    arity[PUSHACC2]=arity[PUSHACC3]=arity[PUSHACC4]=arity[PUSHACC5]=
+    arity[PUSHACC6]=arity[PUSHACC7]=arity[ENVACC1]=arity[ENVACC2]=
+    arity[ENVACC3]=arity[ENVACC4]=arity[PUSHENVACC1]=arity[PUSHENVACC2]=
+    arity[PUSHENVACC3]=arity[PUSHENVACC4]=arity[APPLY1]=arity[APPLY2]=
+    arity[APPLY3]=arity[RESTART]=arity[OFFSETCLOSUREM2]=
     arity[OFFSETCLOSURE0]=arity[OFFSETCLOSURE2]=arity[PUSHOFFSETCLOSUREM2]=
     arity[PUSHOFFSETCLOSURE0]=arity[PUSHOFFSETCLOSURE2]=
+    arity[GETFIELD0]=arity[GETFIELD1]=arity[SETFIELD0]=arity[SETFIELD1]=
     arity[CONST0]=arity[CONST1]=arity[CONST2]=arity[CONST3]=
     arity[PUSHCONST0]=arity[PUSHCONST1]=arity[PUSHCONST2]=arity[PUSHCONST3]=
-    arity[ACCUMULATE]=arity[STOP]=arity[FORCE]=arity[MAKEPROD]= 0;
+    arity[ACCUMULATE]=arity[STOP]=arity[MAKEPROD]= 0;
   /* instruction with one operand */
   arity[ACC]=arity[PUSHACC]=arity[POP]=arity[ENVACC]=arity[PUSHENVACC]=
-    arity[PUSH_RETADDR]=
-    arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=arity[APPTERM3]=arity[RETURN]=
-    arity[GRAB]=arity[COGRAB]=
-    arity[OFFSETCLOSURE]=arity[PUSHOFFSETCLOSURE]=
-    arity[GETGLOBAL]=arity[PUSHGETGLOBAL]=
-    arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEACCU]=
-    arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=arity[PUSHFIELD]=
-    arity[ACCUMULATECOND]= 1;
+    arity[PUSH_RETADDR]=arity[APPLY]=arity[APPTERM1]=arity[APPTERM2]=
+    arity[APPTERM3]=arity[RETURN]=arity[GRAB]=arity[OFFSETCLOSURE]=
+    arity[PUSHOFFSETCLOSURE]=arity[GETGLOBAL]=arity[PUSHGETGLOBAL]=
+    arity[MAKEBLOCK1]=arity[MAKEBLOCK2]=arity[MAKEBLOCK3]=arity[MAKEBLOCK4]=
+    arity[MAKEACCU]=arity[CONSTINT]=arity[PUSHCONSTINT]=arity[GRABREC]=
+    arity[PUSHFIELDS]=arity[GETFIELD]=arity[SETFIELD]=arity[ACCUMULATECOND]= 1;
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=2;
   /* instruction with four operands */ 
   arity[MAKESWITCHBLOCK]=4;
   /* instruction with arbitrary operands */
-  arity[CLOSUREREC]=arity[SWITCH]=0;
+  arity[CLOSUREREC]=arity[CLOSURECOFIX]=arity[SWITCH]=0;
 }
 
 #endif /*  THREADED_CODE */
@@ -150,7 +150,7 @@ value coq_tcode_of_code (value code, value size) {
       block_size = sizes >> 16;
       sizes = const_size + block_size;
       for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; };
-    } else if (instr == CLOSUREREC) {
+    } else if (instr == CLOSUREREC || instr==CLOSURECOFIX) {
       uint32 i, n;
       COPY32(q,p); p++; /* ndefs */
       n = 3 + 2*(*q);  /* ndefs, nvars, start, typlbls,lbls*/
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index d3b07526..89616c5f 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -22,18 +22,20 @@ enum instructions {
   PUSH_RETADDR,
   APPLY, APPLY1, APPLY2, APPLY3,
   APPTERM, APPTERM1, APPTERM2, APPTERM3,
-  RETURN, RESTART, GRAB, GRABREC, COGRAB, 
-  CLOSURE, CLOSUREREC, 
+  RETURN, RESTART, GRAB, GRABREC, 
+  CLOSURE, CLOSUREREC, CLOSURECOFIX,
   OFFSETCLOSUREM2, OFFSETCLOSURE0, OFFSETCLOSURE2, OFFSETCLOSURE,
   PUSHOFFSETCLOSUREM2, PUSHOFFSETCLOSURE0, PUSHOFFSETCLOSURE2, 
   PUSHOFFSETCLOSURE,
   GETGLOBAL, PUSHGETGLOBAL,
-  MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, 
-  MAKESWITCHBLOCK, MAKEACCU, MAKEPROD,
-  FORCE, SWITCH, PUSHFIELD,
+  MAKEBLOCK, MAKEBLOCK1, MAKEBLOCK2, MAKEBLOCK3, MAKEBLOCK4,
+  SWITCH, PUSHFIELDS, 
+  GETFIELD0, GETFIELD1, GETFIELD, 
+  SETFIELD0, SETFIELD1, SETFIELD,
   CONST0, CONST1, CONST2, CONST3, CONSTINT,
   PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
-  ACCUMULATE, ACCUMULATECOND, STOP
+  ACCUMULATE, ACCUMULATECOND, 
+  MAKESWITCHBLOCK, MAKEACCU, MAKEPROD, STOP
 };
 
 #endif /* _COQ_INSTRUCT_ */
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 8bfe78eb..0f91a7e3 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -65,6 +65,13 @@ sp is a local copy of the global variable extern_sp. */
 #   define print_int(i) 
 #endif
 
+/* Wrapper pour caml_modify */
+#ifdef OCAML_307
+#define CAML_MODIFY(a,b) modify(a,b)
+#else
+#define CAML_MODIFY(a,b) caml_modify(a,b)
+#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; }
@@ -164,7 +171,7 @@ value coq_interprete
 #else 
   opcode_t curr_instr;
 #endif
-    print_instr("Enter Interpreter");
+  print_instr("Enter Interpreter");
   if (coq_pc == NULL) {           /* Interpreter is initializing */
     print_instr("Interpreter is initializing");
 #ifdef THREADED_CODE
@@ -383,6 +390,17 @@ value coq_interprete
 	coq_extra_args = 2;
 	goto check_stacks;
       }
+      /* Stack checks */
+      
+    check_stacks:
+      print_instr("check_stacks");
+      if (sp < coq_stack_threshold) {
+	coq_sp = sp;
+	realloc_coq_stack(Coq_stack_threshold);
+	sp = coq_sp;
+      }
+      Next;
+      /* Fall through CHECK_SIGNALS */
 
       Instruct(APPTERM) {
 	int nargs = *pc++;
@@ -438,6 +456,7 @@ value coq_interprete
       
       Instruct(RETURN) {
 	print_instr("RETURN");
+	print_int(*pc);
 	sp += *pc++;
 	if (coq_extra_args > 0) {
 	  coq_extra_args--;
@@ -485,30 +504,6 @@ value coq_interprete
 	Next;
       }
 
-      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 */
-	  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 */
 	print_instr("GRABREC");
@@ -607,7 +602,59 @@ value coq_interprete
 	accu = accu + 2 * start * sizeof(value);
 	Next;
       }
-     
+
+      Instruct(CLOSURECOFIX){ 
+	int nfunc = *pc++;
+	int nvars = *pc++;
+	int start = *pc++;
+	int i, j , size;
+	value * p;
+	print_instr("CLOSURECOFIX");
+	if (nvars > 0) *--sp = accu;
+	/* construction du vecteur de type */
+	Alloc_small(accu, nfunc, 0);
+	for(i = 0; i < nfunc; i++) {
+	  Field(accu,i) = (value)(pc+pc[i]);
+	}
+	pc += nfunc;
+	*--sp=accu;
+
+        /* Creation des blocks accumulate */
+        for(i=0; i < nfunc; i++) {
+	  Alloc_small(accu, 2, Accu_tag);
+	  Code_val(accu) = accumulate;
+	  Field(accu,1) = Val_int(1);
+	  *--sp=accu;
+	}
+	/* creation des fonction cofix */
+
+        p = sp;
+	size = nfunc + nvars + 2;
+	for (i=0; i < nfunc; i++) {
+
+	  Alloc_small(accu, size, Closure_tag);
+	  Code_val(accu) = pc+pc[i];
+	  for (j = 0; j < nfunc; j++) Field(accu, j+1) = p[j];
+	  Field(accu, size - 1) = p[nfunc];
+	  for (j = nfunc+1; j <= nfunc+nvars; j++) Field(accu, j) = p[j];
+	  *--sp = accu;
+          /* creation du block contenant le cofix */
+
+	  Alloc_small(accu,1, ATOM_COFIX_TAG);
+	  Field(accu, 0) = sp[0];
+	  *sp = accu;
+	  /* mise a jour du block accumulate */
+	  CAML_MODIFY(&Field(p[i], 1),*sp);
+	  sp++;
+	}
+	pc += nfunc;
+	accu = p[start];
+        sp = p + nfunc + 1 + nvars;
+	print_instr("ici4");
+	Next;
+      }
+
+    
       Instruct(PUSHOFFSETCLOSURE) {
 	print_instr("PUSHOFFSETCLOSURE");
 	*--sp = accu;
@@ -644,7 +691,7 @@ value coq_interprete
 /* Access to global variables */
 
       Instruct(PUSHGETGLOBAL) {
-	print_instr("PUSHGETGLOBAL");
+	print_instr("PUSH");
 	*--sp = accu;
       }
       /* Fallthrough */
@@ -703,38 +750,27 @@ value coq_interprete
 	accu = block;
 	Next;
       }
+      Instruct(MAKEBLOCK4) {
+	tag_t tag = *pc++;
+	value block;
+	print_instr("MAKEBLOCK4");
+	Alloc_small(block, 4, tag);
+	Field(block, 0) = accu;
+	Field(block, 1) = sp[0];
+	Field(block, 2) = sp[1];
+	Field(block, 3) = sp[2];
+	sp += 3;
+	accu = block;
+	Next;
+      }
 
   
 /* Access to components of blocks */
         
-	
-/* 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 - 1);
-	  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;
-	} else {
-	  if (Is_block(accu)) print_int(Tag_val(accu));
-	  else print_instr("Not a block");
-	}
-	Next;
-      }
-           
-    
       Instruct(SWITCH) {
 	uint32 sizes = *pc++;
 	print_instr("SWITCH");
-	print_int(sizes);
+	print_int(sizes & 0xFFFF);
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
 	  print_instr("block");
@@ -748,68 +784,79 @@ value coq_interprete
 	}
 	  Next;
       }
-      Instruct(PUSHFIELD){
+
+      Instruct(PUSHFIELDS){
 	int i;
 	int size = *pc++;
-	print_instr("PUSHFIELD");
+	print_instr("PUSHFIELDS");
 	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;
-	print_instr("MAKESWITCHBLOCK");
-	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++;
+      
+      Instruct(GETFIELD0){
+	print_instr("GETFIELD0");
+	accu = Field(accu, 0); 
 	Next;
       }
 
-      /* Stack checks */
-      
-    check_stacks:
-      print_instr("check_stacks");
-      if (sp < coq_stack_threshold) {
-	coq_sp = sp;
-	realloc_coq_stack(Coq_stack_threshold);
-	sp = coq_sp;
+      Instruct(GETFIELD1){
+	print_instr("GETFIELD1");
+	accu = Field(accu, 1);
+	Next;
       }
-      Next;
-      /* Fall through CHECK_SIGNALS */
 
+      Instruct(GETFIELD){
+	print_instr("GETFIELD");
+	accu = Field(accu, *pc); 
+	pc++; 
+	Next;
+      }
+      
+      Instruct(SETFIELD0){
+	print_instr("SETFIELD0");
+	CAML_MODIFY(&Field(accu, 0),*sp);
+	sp++;
+	Next;
+      }
+	
+      Instruct(SETFIELD1){
+        int i, j, size, size_aux;
+	print_instr("SETFIELD1");
+	CAML_MODIFY(&Field(accu, 1),*sp);
+       	sp++;
+	Next; 
+      }
+  
+      /* *sp = accu;
+	* Netoyage des cofix *
+        size = Wosize_val(accu);
+        for (i = 2; i < size; i++) {
+ 	  accu = Field(*sp, i);
+          if (IS_EVALUATED_COFIX(accu)) {
+            size_aux = Wosize_val(accu);
+            *--sp = accu;
+	    Alloc_small(accu, size_aux, Accu_tag);
+	    for(j = 0; j < size_aux; j++) Field(accu, j) = Field(*sp, j);
+	    *sp = accu;
+	    Alloc_small(accu, 1, ATOM_COFIX_TAG);
+	    Field(accu, 0) = Field(Field(*sp, 1), 0);
+	    CAML_MODIFY(&Field(*sp, 1), accu);
+	    accu = *sp; sp++;
+            CAML_MODIFY(&Field(*sp, i), accu);
+	  }
+	}
+	sp++;
+	Next; 
+	} */
+      
+      Instruct(SETFIELD){
+	print_instr("SETFIELD");
+	CAML_MODIFY(&Field(accu, *pc),*sp);
+	sp++; pc++;
+	Next;
+      }	
+   
 /* Integer constants */
 
       Instruct(CONST0){
@@ -854,14 +901,7 @@ value coq_interprete
 	Next;
       }
 
-/* Debugging and machine control */
-
-      Instruct(STOP){
-	print_instr("STOP");
-	coq_sp = sp;
-	return accu;
-      }
-      
+      /* Special operations for reduction of open term */
       Instruct(ACCUMULATECOND) {
 	int i, num;
 	print_instr("ACCUMULATECOND");
@@ -869,7 +909,7 @@ value coq_interprete
 	pc++;
 	if (Field(coq_global_boxed, num) == Val_false || coq_all_transp) {
 	  /*	  printf ("false\n");
-	    printf ("tag = %d", Tag_val(Field(accu,1))); */
+		  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);
@@ -881,7 +921,7 @@ value coq_interprete
 	};
 	/*	printf ("true\n"); */
       }
-
+      
       Instruct(ACCUMULATE) {
 	mlsize_t i, size;
 	print_instr("ACCUMULATE");
@@ -896,7 +936,86 @@ value coq_interprete
 	sp += 3;
 	Next;
       }  
-            
+      Instruct(MAKESWITCHBLOCK) {
+	print_instr("MAKESWITCHBLOCK");
+	*--sp = accu;
+	accu = Field(accu,1);
+	switch (Tag_val(accu)) {
+	case ATOM_COFIX_TAG: 
+	  {
+	    mlsize_t i, nargs;
+	    print_instr("COFIX_TAG");
+	    sp-=2;
+	    pc++;
+	    sp[0] = (value) (pc + *pc);
+	    sp[1] = coq_env;
+	    coq_env = Field(accu,0);
+	    accu = sp[2];
+	    sp[2] = Val_long(coq_extra_args);
+	    nargs = Wosize_val(accu) - 2;
+	    sp -= nargs;
+	    for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
+	    *--sp = accu;
+	    print_int(nargs);
+	    coq_extra_args = nargs;
+	    pc = Code_val(coq_env);
+	    goto check_stacks;
+	  }
+	case ATOM_COFIXEVALUATED_TAG: 
+	  {
+	    print_instr("COFIX_EVAL_TAG");
+	    accu = Field(accu,1);
+	    pc++;
+	    pc = pc + *pc;
+	    sp++;
+	    Next;
+	  }
+	default: 
+	  {  
+	    mlsize_t sz;
+	    int i, annot;
+	    code_t typlbl,swlbl;
+	    print_instr("MAKESWITCHBLOCK");
+	    
+	    typlbl = (code_t)pc + *pc; 
+	    pc++;
+	    swlbl = (code_t)pc + *pc; 
+	    pc++;
+	    annot = *pc++;
+	    sz = *pc++;
+	    *--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;
+      }
+
+	
+         
       Instruct(MAKEACCU) {
 	int i;
 	print_instr("MAKEACCU");
@@ -921,6 +1040,15 @@ value coq_interprete
 	Next;
       }
       
+/* Debugging and machine control */
+
+      Instruct(STOP){
+	print_instr("STOP");
+	coq_sp = sp;
+	return accu;
+      }
+      
+  
 #ifndef THREADED_CODE
     default:
       /*fprintf(stderr, "%d\n", *pc);*/
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index db6aacb9..bfcb6812 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -34,7 +34,6 @@ int drawinstr;
 
 long coq_saved_sp_offset;
 value * coq_sp;
-value forcable;
 /* Some predefined pointer code */ 
 code_t accumulate;
 
@@ -135,7 +134,6 @@ value init_coq_vm(value unit) /* ML */
     init_coq_atom_tbl(40);
     /* Initialing the interpreter */
     coq_all_transp = 0;
-    forcable = Val_false;
     init_coq_interpreter();
     
     /* Some predefined pointer code */
@@ -266,8 +264,9 @@ value coq_set_drawinstr(value unit)
   return Val_unit;
 }
 
-value coq_set_forcable (value unit)
+
+value coq_print_pointer(value p)
 {
-  forcable = Val_true;
+  printf("pointer = %X\n", p);
   return Val_unit;
 }
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 7c96e684..0d866dc7 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -43,7 +43,6 @@ extern int drawinstr;
 /* interp state */
 
 extern value * coq_sp;
-extern value forcable;
 /* Some predefined pointer code */ 
 extern code_t accumulate;
 
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index baf3ab09..34b885e8 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -27,8 +27,7 @@ value coq_kind_of_closure(value 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);
+  if (Is_instruction(c, MAKEACCU)) return Val_int(3);
   return Val_int(0);
 }
 
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index a186d62a..a5176f3f 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -14,15 +14,25 @@
 #include "alloc.h"
 #include "mlvalues.h"
 
+#define Default_tag 0
+#define Accu_tag 0
+
+
+
+#define ATOM_ID_TAG 0
+#define ATOM_IDDEF_TAG 1
+#define ATOM_INDUCTIVE_TAG 2
 #define ATOM_FIX_TAG 3
 #define ATOM_SWITCH_TAG 4
+#define ATOM_COFIX_TAG 5
+#define ATOM_COFIXEVALUATED_TAG 6
+
 
-#define Accu_tag 0
-#define Default_tag 0
 
 /* Les blocs accumulate */
 #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
 
+#define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
 #endif /* _COQ_VALUES_ */