Imported Upstream version 8.1~gammaupstream/8.1.gamma

40 files changed, 1405 insertions, 1239 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_ */
 
 
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 49955474..a9b16f29 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -3,6 +3,14 @@ open Term
 
 type tag = int 
 
+let id_tag = 0
+let iddef_tag = 1
+let ind_tag = 2
+let fix_tag = 3
+let switch_tag = 4
+let cofix_tag = 5
+let cofix_evaluated_tag = 6
+
 type structured_constant =
   | Const_sorts of sorts
   | Const_ind of inductive
@@ -39,18 +47,20 @@ type instruction =
   | Krestart
   | Kgrab of int                        (* number of arguments *)
   | Kgrabrec of int                     (* rec arg *)
-  | Kcograb of int                      (* number of arguments *)
   | Kclosure of Label.t * int           (* label, number of free variables *)
   | Kclosurerec of int * int * Label.t array * Label.t array 
                    (* nb fv, init, lbl types, lbl bodies *)
+  | Kclosurecofix of int * int * Label.t array * Label.t array 
+                   (* nb fv, init, lbl types, lbl bodies *)
   | Kgetglobal of constant
   | Kconst of structured_constant
   | Kmakeblock of int * tag             (* size, tag *)
   | Kmakeprod 
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
-  | Kforce
   | Kswitch of Label.t array * Label.t array (* consts,blocks *)
-  | Kpushfield of int 
+  | Kpushfields of int 
+  | Kfield of int
+  | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
 
@@ -79,7 +89,6 @@ let rec instruction ppf = function
   | 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) ->
@@ -89,7 +98,13 @@ let rec instruction ppf = function
       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 *)
+  | Kclosurecofix (fv,init,lblt,lblb) ->
+      fprintf ppf "\tclosurecofix";
+      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;
   | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
   | Kconst cst ->
       fprintf ppf "\tconst"
@@ -98,13 +113,13 @@ let rec instruction ppf = function
   | 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
+  | Kpushfields n -> fprintf ppf "\tpushfields %i" n
+  | Ksetfield n -> fprintf ppf "\tsetfield %i" n
+  | Kfield  n -> fprintf ppf "\tgetfield %i" n
   | Kstop -> fprintf ppf "\tstop"
   | Ksequence (c1,c2) ->
       fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2 
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index a996f750..215b6ad4 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -3,6 +3,14 @@ open Term
 
 type tag = int 
 
+val id_tag : tag
+val iddef_tag : tag
+val ind_tag : tag
+val fix_tag : tag
+val switch_tag : tag
+val cofix_tag : tag
+val cofix_evaluated_tag : tag
+
 type structured_constant =
   | Const_sorts of sorts
   | Const_ind of inductive
@@ -37,21 +45,24 @@ type instruction =
   | Krestart
   | Kgrab of int                        (* number of arguments *)
   | Kgrabrec of int                     (* rec arg *)
-  | Kcograb of int                      (* number of arguments *)
   | Kclosure of Label.t * int           (* label, number of free variables *)
   | Kclosurerec of int * int * Label.t array * Label.t array 
                    (* nb fv, init, lbl types, lbl bodies *)
+  | Kclosurecofix of int * int * Label.t array * Label.t array 
+                   (* nb fv, init, lbl types, lbl bodies *)
   | Kgetglobal of constant
   | Kconst of structured_constant
   | Kmakeblock of int * tag             (* size, tag *)
   | Kmakeprod 
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
-  | Kforce
   | Kswitch of Label.t array * Label.t array (* consts,blocks *)
-  | Kpushfield of int 
+  | Kpushfields of int 
+  | Kfield of int
+  | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
 
+
 and bytecodes = instruction list
 
 type fv_elem = FVnamed of identifier | FVrel of int
@@ -59,3 +70,4 @@ type fv_elem = FVnamed of identifier | FVrel of int
 type fv = fv_elem array
 
 val draw_instr : bytecodes -> unit
+
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 041e0795..e1f89fad 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -6,35 +6,161 @@ open Term
 open Declarations
 open Pre_env
 
-(*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 = []}
+(* Compilation des variables + calcul des variables libres               *)
+
+(* Dans la machine virtuel il n'y a pas de difference entre les           *)
+(* fonctions et leur environnement                                        *)
+
+(* Representation de l'environnements des fonctions :                     *)
+(*        [clos_t | code | fv1 | fv2 | ... | fvn ]                        *)
+(*                ^                                                       *)
+(*  l'offset pour l'acces au variable libre est 1 (il faut passer le      *)
+(*  pointeur de code).                                                    *)
+(*  Lors de la compilation, les variables libres sont stock'ees dans      *)
+(*  [in_env] dans l'ordre inverse de la representation machine, ceci      *)
+(* permet de rajouter des nouvelles variables dans l'environnememt        *)
+(* facilement.                                                            *)
+(* Les arguments de la fonction arrive sur la pile dans l'ordre de        *)
+(* l'application :  f arg1 ... argn                                       *)
+(*   - la pile est alors :                                                *)
+(*        arg1 : ... argn : extra args : return addr : ...                *)
+(* Dans le corps de la fonction [arg1] est repr'esent'e par le de Bruijn  *)
+(*  [n], [argn] par le de Bruijn [1]                                      *)
+
+(* Representation des environnements des points fix mutuels :             *)
+(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
+(*                ^<----------offset--------->                            *)
+(* type = [Ct1 | .... | Ctn]                                              *)
+(* Ci est le code correspondant au corps du ieme point fix                *)
+(* Lors de l'evaluation d'un point fix l'environnement est un pointeur    *)
+(* sur la position correspondante a son code.                             *)
+(* Dans le corps de chaque point fix le de Bruijn [nbr] represente,       *)
+(* le 1er point fix de la declaration mutuelle, le de Bruijn [1] le       *)
+(* nbr-ieme.                                                              *)
+(* L'acces a ces variables se fait par l'instruction [Koffsetclosure]     *)
+(*  (decalage de l'environnement)                                         *)
+
+(* Ceci permet de representer tout les point fix mutuels en un seul bloc  *)
+(* [Ct1 | ... | Ctn] est un tableau contant le code d'evaluation des      *)
+(* types des points fixes, ils sont utilises pour tester la conversion    *)
+(* Leur environnement d'execution est celui du dernier point fix :        *)
+(* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
+(*                                ^                                       *)
+
+
+(* Representation des cofix mutuels :                                     *)
+(*  a1 =   [A_t | accumulate | [Cfx_t | fcofix1 ] ]                       *)
+(*                ...                                                     *)
+(*  anbr = [A_t | accumulate | [Cfx_t | fcofixnbr ] ]                     *)
+(*                                                                        *)
+(*  fcofix1 = [clos_t   | code1   | a1 |...| anbr | fv1 |...| fvn | type] *)
+(*                      ^                                                 *)
+(*                ...                                                     *)
+(*  fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *)
+(*                      ^                                                 *)
+(*  Les block [ai] sont des fonctions qui accumulent leurs arguments :    *)
+(*           ai arg1  argp --->                                           *)
+(*    ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ]   *)
+(* Si un tel bloc arrive sur un [match] il faut forcer l'evaluation,      *)
+(* la fonction [fcofixi] est alors appliqu'ee a [ai'] [arg1] ... [argp]   *)
+(* A la fin de l'evaluation [ai'] est mis a jour avec le resultat de      *)
+(* l'evaluation :                                                         *)
+(*  ai' <--                                                               *)
+(*   [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ]   *)
+(* L'avantage de cette representation est qu'elle permet d'evaluer qu'une *)
+(* fois l'application d'un cofix (evaluation lazy)                        *)
+(* De plus elle permet de creer facilement des cycles quand les cofix ne  *)
+(* n'ont pas d'aruments, ex:                                              *)
+(*   cofix one := cons 1 one                                              *)
+(*   a1 = [A_t | accumulate | [Cfx_t|fcofix1] ]                           *)
+(*   fcofix1 = [clos_t | code | a1]                                       *)
+(*  Quand on force l'evaluation de [a1] le resultat est                   *)
+(*    [cons_t | 1 | a1]                                                   *)
+(*  [a1] est mis a jour :                                                 *)
+(*  a1 = [A_t | accumulate | [Cfxe_t | fcofix1 | [cons_t | 1 | a1]] ]     *)
+(* Le cycle est cree ...                                                  *)
+   
+(* On conserve la fct de cofix pour la conversion                         *)
+   
+type vm_env = {
+    size : int;              (* longueur de la liste [n] *)
+    fv_rev : fv_elem list    (* [fvn; ... ;fv1] *)
+  }    
+   
+let empty_fv = { size= 0;  fv_rev = [] }
+   
+type comp_env = { 
+    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  : instruction list; (* instruction d'acces pour les variables *)
+                                 (*  de point fix ou de cofix              *)
+    offset : int;                 
+    in_env : vm_env ref 
+  } 
 
 let fv r = !(r.in_env)
+   
+let empty_comp_env ()= 
+  { nb_stack = 0; 
+    in_stack = [];
+    nb_rec = 0;
+    pos_rec = [];
+    offset = 0; 
+    in_env = ref empty_fv;
+  } 
+
+(*i Creation functions for comp_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) 
+   
+let comp_env_fun arity = 
+  { nb_stack = arity; 
+    in_stack = add_param arity 0 [];
+    nb_rec = 0;
+    pos_rec = [];
+    offset = 1; 
+    in_env = ref empty_fv 
+  } 
+    
+
+let comp_env_type rfv = 
+  { nb_stack = 0; 
+    in_stack = [];
+    nb_rec = 0;
+    pos_rec = [];
+    offset = 1; 
+    in_env = rfv 
+  }
+   
+let comp_env_fix ndef curr_pos arity rfv =
+   let prec = ref [] in
+   for i = ndef downto 1 do
+     prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec 
+   done;
+   { nb_stack = arity; 
+     in_stack = add_param arity 0 [];
+     nb_rec = ndef; 
+     pos_rec = !prec;
+     offset = 2 * (ndef - curr_pos - 1)+1;
+     in_env = rfv 
+   } 
+
+let comp_env_cofix ndef arity rfv =
+   let prec = ref [] in
+   for i = 1 to ndef do
+     prec := Kenvacc i :: !prec
+   done;
+   { nb_stack = arity; 
+     in_stack = add_param arity 0 [];
+     nb_rec = ndef; 
+     pos_rec = !prec;
+     offset = ndef+1;
+     in_env = rfv 
+   }
 
 (* [push_param ] ajoute les parametres de fonction dans la pile *)
 let push_param n sz r =
@@ -42,33 +168,16 @@ let push_param n sz r =
     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 *)
+(* [push_local e sz] ajoute une nouvelle variable dans la pile a la *)
+(* position [sz]                                                    *)
 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} 
 
+(*i Compilation of variables *)
 let find_at el l = 
   let rec aux n = function
     | [] -> raise Not_found
@@ -87,24 +196,27 @@ let pos_named id r =
 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)
-
+  else
+    let i = i - r.nb_stack in
+    if i <= r.nb_rec then 
+      try List.nth r.pos_rec (i-1)
+      with _ -> assert false
+    else
+      let i = i - r.nb_rec in
+      let db = FVrel(i) 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. *)
+(* 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
@@ -113,9 +225,9 @@ let rec discard_dead_code 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. *)
+(* 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)
@@ -138,7 +250,7 @@ let rec is_tailcall = function
   | Klabel _ :: c -> is_tailcall c
   | _ -> None
 
-(* Extention of the continuation ****)
+(* Extention of the continuation *)
 	
 (* Add a Kpop n instruction in front of a continuation *)
 let rec add_pop n = function
@@ -150,15 +262,41 @@ let add_grab arity lbl cont =
   if arity = 1 then Klabel lbl :: cont
   else Krestart :: Klabel lbl :: Kgrab (arity - 1) :: cont
  
-
-(* Environnement global *****)
+let add_grabrec rec_arg arity lbl cont =
+  if arity = 1 then 
+    Klabel lbl :: Kgrabrec 0 :: Krestart :: cont
+  else
+    Krestart :: Klabel lbl :: Kgrabrec rec_arg ::
+    Krestart :: Kgrab (arity - 1) :: cont
+
+(* continuation of a cofix *)
+
+let cont_cofix arity =
+    (* accu = res                                                         *)
+    (* stk  = ai::args::ra::...                                           *)
+    (* ai   = [At|accumulate|[Cfx_t|fcofix]|args]                         *)
+  [ Kpush;
+    Kpush;        (*                 stk = res::res::ai::args::ra::...    *)
+    Kacc 2;
+    Kfield 1;
+    Kfield 0;
+    Kmakeblock(2, cofix_evaluated_tag); 
+    Kpush;        (*  stk = [Cfxe_t|fcofix|res]::res::ai::args::ra::...*)
+    Kacc 2;
+    Ksetfield 1;  (*   ai = [At|accumulate|[Cfxe_t|fcofix|res]|args]      *)
+                  (*  stk = res::ai::args::ra::...                        *)   
+    Kacc 0;       (* accu = res                                           *)
+    Kreturn (arity+2) ]
+
+
+(*i Global environment global *)
 
 let global_env = ref empty_env
 
 let set_global_env env = global_env := env
 
 
-(* Code des fermetures ****)
+(* Code des fermetures *)
 let fun_code = ref []
 
 let init_fun_code () = fun_code := []
@@ -259,6 +397,14 @@ let compile_fv_elem reloc fv sz cont =
   | FVrel i -> pos_rel i reloc sz :: cont
   | FVnamed id -> pos_named id reloc :: cont
 
+let rec 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)
+
 (* compilation des constantes *)
 
 let rec get_allias env kn =
@@ -271,8 +417,8 @@ let rec get_allias env kn =
  
 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")
+  | Meta _ -> raise (Invalid_argument "Cbytegen.compile_constr : Meta")
+  | Evar _ -> raise (Invalid_argument "Cbytegen.compile_constr : Evar")
  
   | Cast(c,_,_) -> compile_constr reloc c sz cont
 
@@ -294,7 +440,7 @@ let rec compile_constr reloc c sz cont =
   | Lambda _ ->
       let params, body = decompose_lam c in
       let arity = List.length params in
-      let r_fun = init_fun arity in
+      let r_fun = comp_env_fun arity in
       let lbl_fun = Label.create() in
       let cont_fun = 
 	compile_constr r_fun body arity [Kreturn arity] in
@@ -314,11 +460,11 @@ let rec compile_constr reloc c sz cont =
       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
+      let env_type = comp_env_type rfv in
       for i = 0 to ndef - 1 do
 	let lbl,fcode = 
 	  label_code 
-	    (compile_constr rtype type_bodies.(i) 0 [Kstop]) in 
+	    (compile_constr env_type type_bodies.(i) 0 [Kstop]) in 
 	lbl_types.(i) <- lbl; 
 	fun_code := [Ksequence(fcode,!fun_code)]
       done;
@@ -326,18 +472,12 @@ let rec compile_constr reloc c sz cont =
       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 env_body = comp_env_fix ndef i arity rfv in
 	let cont1 = 
-	  compile_constr rbody body arity [Kreturn arity] in
+	  compile_constr env_body 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
+	let fcode =  add_grabrec rec_args.(i) arity lbl cont1 in
 	fun_code := [Ksequence(fcode,!fun_code)]
       done;
       let fv = !rfv in
@@ -346,15 +486,15 @@ let rec compile_constr reloc c sz 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
+      let rfv = ref empty_fv in
+      let env_type = comp_env_type rfv in
       for i = 0 to ndef - 1 do
 	let lbl,fcode = 
 	  label_code 
-	    (compile_constr rtype type_bodies.(i) 0 [Kstop]) in
+	    (compile_constr env_type type_bodies.(i) 0 [Kstop]) in
 	lbl_types.(i) <- lbl; 
 	fun_code := [Ksequence(fcode,!fun_code)]
       done;
@@ -362,21 +502,18 @@ let rec compile_constr reloc c sz cont =
       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 env_body = comp_env_cofix ndef arity rfv in
 	let lbl = Label.create () in
-
 	let cont1 = 
-	  compile_constr rbody body arity [Kreturn(arity)] in
+	  compile_constr env_body body (arity+1) (cont_cofix 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
+	  add_grab (arity+1) lbl cont1 in
+	lbl_bodies.(i) <- lbl;
+	fun_code := [Ksequence(cont2,!fun_code)];
       done;
       let fv = !rfv in
       compile_fv reloc fv.fv_rev sz 
-	(Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont)
+	(Kclosurecofix(fv.size, init, lbl_types, lbl_bodies) :: cont)
   
   | Case(ci,t,a,branchs) ->
       let ind = ci.ci_ind in
@@ -418,12 +555,12 @@ let rec compile_constr reloc c sz cont =
 	  let lbl_b,code_b = 
 	    label_code(
 	    if nargs = arity then
-	      Kpushfield arity ::
+	      Kpushfields 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 :: 
+	      Kpushfields arity :: 
 	      compile_constr reloc branchs.(i) (sz_b+arity)
 		(Kappterm(arity,sz_appterm) :: !c))
 	  in
@@ -436,17 +573,8 @@ let rec compile_constr reloc c sz cont =
 	| 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)
-      
+      compile_constr reloc a sz code_sw
+       
 and compile_str_cst reloc sc sz cont =
   match sc with
   | Bconstr c -> compile_constr reloc c sz cont
@@ -465,9 +593,18 @@ let compile env c =
   set_global_env env;
   init_fun_code ();
   Label.reset_label_counter ();
-  let reloc = empty () in
+  let reloc = empty_comp_env () in
   let init_code = compile_constr reloc c 0 [Kstop] in
   let fv = List.rev (!(reloc.in_env).fv_rev) in
+(*  draw_instr init_code;
+  draw_instr !fun_code;
+  Format.print_string "fv = ";
+  List.iter (fun v ->
+    match v with
+    | FVnamed id -> Format.print_string ((string_of_id id)^"; ")
+    | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv;  Format
+    .print_string "\n";
+  Format.print_flush();  *)
   init_code,!fun_code, Array.of_list fv
 
 let compile_constant_body env body opaque boxed =
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index cccb1844..71a9aa0e 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -149,8 +149,6 @@ let emit_instr = function
       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) ->
@@ -160,6 +158,13 @@ let emit_instr = function
       Array.iter (out_label_with_orig org) lbl_types;
       let org = !out_position in
       Array.iter (out_label_with_orig org) lbl_bodies
+  | Kclosurecofix(nfv,init,lbl_types,lbl_bodies) ->
+      out opCLOSURECOFIX;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)) -> 
@@ -178,16 +183,20 @@ let emit_instr = function
       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
+  | Kpushfields n ->
+      out opPUSHFIELDS;out_int n
+  | Kfield n ->
+      if n <= 1 then out (opGETFIELD0+n)
+      else (out opGETFIELD;out_int n)
+  | Ksetfield n ->
+      if n <= 1 then out (opSETFIELD0+n) 
+      else (out opSETFIELD;out_int n)
   | Kstop -> 
       out opSTOP
   | Ksequence _ -> raise (Invalid_argument "Cemitcodes.emit_instr")
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 617611bf..41fe8750 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: closure.ml 8802 2006-05-10 20:47:28Z barras $ *)
+(* $Id: closure.ml 9215 2006-10-05 15:40:31Z herbelin $ *)
 
 open Util
 open Pp
@@ -375,14 +375,17 @@ let defined_rels flags env =
       (rel_context env) ~init:(0,[])
 (*  else (0,[])*)
 
-
-let rec mind_equiv info kn1 kn2 = 
-  kn1 = kn2 ||
-	match (lookup_mind kn1 info.i_env).mind_equiv with
-	    Some kn1' -> mind_equiv info kn2 kn1'
-	  | None -> match (lookup_mind kn2 info.i_env).mind_equiv with
-		Some kn2' -> mind_equiv info kn2' kn1
-	      | None -> false
+let rec mind_equiv env (kn1,i1) (kn2,i2) =
+  let rec equiv kn1 kn2 =
+    kn1 = kn2 ||
+      match (lookup_mind kn1 env).mind_equiv with
+	  Some kn1' -> equiv kn2 kn1'
+	| None -> match (lookup_mind kn2 env).mind_equiv with
+	      Some kn2' -> equiv kn2' kn1
+	    | None -> false in
+  i1 = i2 && equiv kn1 kn2
+
+let mind_equiv_infos info = mind_equiv info.i_env
 
 let create mk_cl flgs env =
   { i_flags = flgs;
diff --git a/kernel/closure.mli b/kernel/closure.mli
index feec8395..924da0a5 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: closure.mli 8793 2006-05-05 17:41:41Z barras $ i*)
+(*i $Id: closure.mli 9215 2006-10-05 15:40:31Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -179,8 +179,9 @@ val whd_stack :
 (* [unfold_reference] unfolds references in a [fconstr] *)
 val unfold_reference : clos_infos -> table_key -> fconstr option
 
-(* [mind_equiv] checks whether two mutual inductives are intentionally equal *)
-val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool
+(* [mind_equiv] checks whether two inductive types are intentionally equal *)
+val mind_equiv : env -> inductive -> inductive -> bool
+val mind_equiv_infos : clos_infos -> inductive -> inductive -> bool
 
 (************************************************************************)
 (*i This is for lazy debug *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 58c21d9f..6b2a6245 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cooking.ml 8752 2006-04-27 19:37:33Z herbelin $ i*)
+(*i $Id: cooking.ml 9320 2006-10-30 16:53:43Z barras $ i*)
 
 open Pp
 open Util
@@ -122,7 +122,13 @@ let cook_constant env r =
     on_body (fun c ->
       abstract_constant_body (expmod_constr r.d_modlist c) hyps) 
       cb.const_body in
-  let typ =
-    abstract_constant_type (expmod_constr r.d_modlist cb.const_type) hyps in
+  let typ = match cb.const_type with
+    | NonPolymorphicType t ->
+	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
+	NonPolymorphicType typ
+    | PolymorphicArity (ctx,s) ->
+	let t = mkArity (ctx,Type s.poly_level) in
+	let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
+	Typeops.make_polymorphic_if_arity env typ in
   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 7b51ac0c..93c2ccc9 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cooking.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
+(*i $Id: cooking.mli 9310 2006-10-28 19:35:09Z herbelin $ i*)
 
 open Names
 open Term
@@ -25,7 +25,7 @@ type recipe = {
 
 val cook_constant :
   env -> recipe -> 
-    constr_substituted option * constr * constraints * bool * bool
+    constr_substituted option * constant_type * constraints * bool * bool
 
 (*s Utility functions used in module [Discharge]. *)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index c52b5c48..e5e05eb3 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declarations.ml 8845 2006-05-23 07:41:58Z herbelin $ i*)
+(*i $Id: declarations.ml 9310 2006-10-28 19:35:09Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -25,6 +25,15 @@ type engagement = ImpredicativeSet
 
 (*s Constants (internal representation) (Definition/Axiom) *)
 
+type polymorphic_arity = {
+  poly_param_levels : universe option list;
+  poly_level : universe;
+}
+
+type constant_type =
+  | NonPolymorphicType of types
+  | PolymorphicArity of rel_context * polymorphic_arity
+
 type constr_substituted = constr substituted
 
 let from_val = from_val
@@ -36,7 +45,7 @@ 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_type : constant_type;
     const_body_code : Cemitcodes.to_patch_substituted;
    (* const_type_code : Cemitcodes.to_patch; *)
     const_constraints : constraints;
@@ -90,11 +99,6 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p
    with      In (params) : Un := cn1 : Tn1 | ... | cnpn : Tnpn
 *)
 
-type polymorphic_inductive_arity = {
-  mind_param_levels : universe option list;
-  mind_level : universe;
-}
-
 type monomorphic_inductive_arity = {
   mind_user_arity : constr;
   mind_sort : sorts;
@@ -102,7 +106,7 @@ type monomorphic_inductive_arity = {
 
 type inductive_arity = 
 | Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_inductive_arity
+| Polymorphic of polymorphic_arity
 
 type one_inductive_body = {
 
@@ -186,11 +190,15 @@ type mutual_inductive_body = {
     mind_equiv : kernel_name option
   }
 
+let subst_arity sub = function
+| NonPolymorphicType s -> NonPolymorphicType (subst_mps sub s)
+| PolymorphicArity (ctx,s) -> PolymorphicArity (subst_rel_context sub ctx,s)
+
 (* TODO: should be changed to non-coping after Term.subst_mps *)
 let subst_const_body sub cb = {
     const_hyps = (assert (cb.const_hyps=[]); []);
     const_body = option_map (subst_constr_subst sub) cb.const_body;
-    const_type = subst_mps sub cb.const_type;
+    const_type = subst_arity 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;
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index c96d2131..1eaeecb9 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: declarations.mli 8845 2006-05-23 07:41:58Z herbelin $ i*)
+(*i $Id: declarations.mli 9310 2006-10-28 19:35:09Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -26,6 +26,15 @@ type engagement = ImpredicativeSet
 (**********************************************************************)
 (*s Representation of constants (Definition/Axiom)                    *)
 
+type polymorphic_arity = {
+  poly_param_levels : universe option list;
+  poly_level : universe;
+}
+
+type constant_type =
+  | NonPolymorphicType of types
+  | PolymorphicArity of rel_context * polymorphic_arity
+
 type constr_substituted
 
 val from_val : constr -> constr_substituted
@@ -34,7 +43,7 @@ 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_type : constant_type;
     const_body_code : to_patch_substituted;
    (*i const_type_code : to_patch;i*)
     const_constraints : constraints;
@@ -70,11 +79,6 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
 \end{verbatim}
 *)
 
-type polymorphic_inductive_arity = {
-  mind_param_levels : universe option list;
-  mind_level : universe;
-}
-
 type monomorphic_inductive_arity = {
   mind_user_arity : constr;
   mind_sort : sorts;
@@ -82,7 +86,7 @@ type monomorphic_inductive_arity = {
 
 type inductive_arity = 
 | Monomorphic of monomorphic_inductive_arity
-| Polymorphic of polymorphic_inductive_arity
+| Polymorphic of polymorphic_arity
 
 type one_inductive_body = {
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a1e19815..e73f5848 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: environ.ml 8810 2006-05-12 18:50:21Z barras $ *)
+(* $Id: environ.ml 9201 2006-10-03 16:47:40Z notin $ *)
 
 open Util
 open Names
@@ -245,6 +245,31 @@ let global_vars_set env constr =
   in 
   filtrec Idset.empty constr
 
+(* like [global_vars] but don't get through evars *)
+let global_vars_set_drop_evar env constr = 
+  let fold_constr_drop_evar f acc c = match kind_of_term c with
+    | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+      | Construct _) -> acc
+    | Cast (c,_,t) -> f (f acc c) t
+    | Prod (_,t,c) -> f (f acc t) c
+    | Lambda (_,t,c) -> f (f acc t) c
+    | LetIn (_,b,t,c) -> f (f (f acc b) t) c
+    | App (c,l) -> Array.fold_left f (f acc c) l
+    | Evar (_,l) -> acc
+    | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
+    | Fix (_,(lna,tl,bl)) ->
+	let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in
+	  Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd
+    | CoFix (_,(lna,tl,bl)) ->
+	let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in
+	  Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd in
+  let rec filtrec acc c =
+    let vl = vars_of_global env c in
+    let acc = List.fold_right Idset.add vl acc in
+      fold_constr_drop_evar filtrec acc c
+  in 
+    filtrec Idset.empty constr
+
 (* [keep_hyps env ids] keeps the part of the section context of [env] which 
    contains the variables of the set [ids], and recursively the variables 
    contained in the types of the needed variables. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index cfc23651..3728eea3 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: environ.mli 8810 2006-05-12 18:50:21Z barras $ i*)
+(*i $Id: environ.mli 9310 2006-10-28 19:35:09Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -129,7 +129,7 @@ type const_evaluation_result = NoBody | Opaque
 exception NotEvaluableConst of const_evaluation_result
 
 val constant_value     : env -> constant -> constr
-val constant_type      : env -> constant -> types
+val constant_type      : env -> constant -> constant_type
 val constant_opt_value : env -> constant -> constr option
 
 (************************************************************************)
@@ -165,6 +165,7 @@ val set_engagement : engagement -> env -> env
 (* [global_vars_set env c] returns the list of [id]'s occurring as
    [VAR id] in [c] *)
 val global_vars_set : env -> constr -> Idset.t
+val global_vars_set_drop_evar : env -> constr -> Idset.t
 (* the constr must be an atomic construction *)
 val vars_of_global : env -> constr -> identifier list
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index e7dc09ee..1520e009 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indtypes.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
+(* $Id: indtypes.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
 
 open Util
 open Names
@@ -163,9 +163,13 @@ let small_unit constrsinfos =
    w1,w2,w3 <= u3
 *)   
 
+let extract_level (_,_,_,lc,lev) =
+  (* Enforce that the level is not in Prop if more than two constructors *)
+  if Array.length lc >= 2 then sup base_univ lev else lev
+
 let inductive_levels arities inds =
   let levels = Array.map pi3 arities in
-  let cstrs_levels = Array.map (fun (_,_,_,_,lev) -> lev) inds in
+  let cstrs_levels = Array.map extract_level inds in
   (* Take the transitive closure of the system of constructors *)
   (* level constraints and remove the recursive dependencies *)
   solve_constraints_system levels cstrs_levels
@@ -388,7 +392,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) =
   let specif = lookup_mind_specif env mi in
   let env' =
     push_rel (Anonymous,None,
-              hnf_prod_applist env (type_of_inductive specif) lpar) env in
+              hnf_prod_applist env (type_of_inductive env specif) lpar) env in
   let ra_env' = 
     (Imbr mi,Rtree.mk_param 0) ::
     List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in
@@ -597,8 +601,8 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst =
     let arkind,kelim = match ar_kind with
     | Inr (param_levels,lev) ->
 	Polymorphic {
-	  mind_param_levels = param_levels;
-	  mind_level = lev; 
+	  poly_param_levels = param_levels;
+	  poly_level = lev; 
 	}, all_sorts
     | Inl ((issmall,isunit),ar,s) ->
 	let isunit = isunit && ntypes = 1 && not (is_recursive recargs.(0)) in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 76553237..b7265e8c 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: inductive.ml 8972 2006-06-22 22:17:43Z herbelin $ *)
+(* $Id: inductive.ml 9323 2006-10-30 23:05:29Z herbelin $ *)
 
 open Util
 open Names
@@ -30,8 +30,8 @@ let lookup_mind_specif env (kn,tyi) =
 let find_rectype env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
   match kind_of_term t with
-    | Ind ind -> (ind, l)
-    | _ -> raise Not_found
+  | Ind ind -> (ind, l)
+  | _ -> raise Not_found
 
 let find_inductive env c =
   let (t, l) = decompose_app (whd_betadeltaiota env c) in
@@ -122,14 +122,6 @@ where
 Remark: Set (predicative) is encoded as Type(0)
 *)
 
-let set_inductive_level env s t = 
-  let sign,s' = dest_prod_assum env t in
-  if family_of_sort s <> family_of_sort (destSort s') then
-    (* This induces reductions if user_arity <> nf_arity *)
-    mkArity (sign,s)
-  else
-    t
-
 let sort_as_univ = function
 | Type u -> u
 | Prop Null -> neutral_univ
@@ -139,44 +131,71 @@ let cons_subst u su subst =
   try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst
   with Not_found -> (u, su) :: subst
 
-let rec make_subst env exp act =
-  match exp, act with
-  (* Bind expected levels of parameters to actual levels *)
-  | None :: exp, _ :: act ->
-      make_subst env exp act
-  | Some u :: exp, t :: act ->
-      let su = sort_as_univ (snd (dest_arity env t)) in
-      cons_subst u su (make_subst env exp act)
-  (* Not enough parameters, create a fresh univ *)
-  | Some u :: exp, [] ->
-      let su = fresh_local_univ () in
-      cons_subst u su (make_subst env exp [])
-  | None :: exp, [] ->
-      make_subst env exp []
-  (* Uniform parameters are exhausted *)
-  | [], _ -> []
-
-let sort_of_instantiated_universe mip subst level =
-  let level = subst_large_constraints subst level in
-  let nci = number_of_constructors mip in
-  if nci = 0 then mk_Prop
-  else
-    if is_empty_univ level then if nci = 1 then mk_Prop else mk_Set 
-    else if is_base_univ level then mk_Set
-    else Type level
-
-let instantiate_inductive_with_param_levels env ar mip paramtyps =
-  let args = Array.to_list paramtyps in
-  let subst = make_subst env ar.mind_param_levels args in
-  sort_of_instantiated_universe mip subst ar.mind_level
+let actualize_decl_level env lev t =
+  let sign,s = dest_arity env t in
+  mkArity (sign,lev)
+
+let polymorphism_on_non_applied_parameters = false
+
+(* Bind expected levels of parameters to actual levels *)
+(* Propagate the new levels in the signature *)
+let rec make_subst env = function
+  | (_,Some _,_ as t)::sign, exp, args ->
+      let ctx,subst = make_subst env (sign, exp, args) in
+      t::ctx, subst
+  | d::sign, None::exp, args ->
+      let args = match args with _::args -> args | [] -> [] in
+      let ctx,subst = make_subst env (sign, exp, args) in
+      d::ctx, subst
+  | d::sign, Some u::exp, a::args ->
+      (* We recover the level of the argument, but we don't change the *)
+      (* level in the corresponding type in the arity; this level in the *)
+      (* arity is a global level which, at typing time, will be enforce *)
+      (* to be greater than the level of the argument; this is probably *)
+      (* a useless extra constraint *)
+      let s = sort_as_univ (snd (dest_arity env a)) in
+      let ctx,subst = make_subst env (sign, exp, args) in
+      d::ctx, cons_subst u s subst
+  | (na,None,t as d)::sign, Some u::exp, [] ->
+      (* No more argument here: we instantiate the type with a fresh level *)
+      (* which is first propagated to the corresponding premise in the arity *)
+      (* (actualize_decl_level), then to the conclusion of the arity (via *)
+      (* the substitution) *)
+      let ctx,subst = make_subst env (sign, exp, []) in
+      if polymorphism_on_non_applied_parameters then
+	let s = fresh_local_univ () in
+	let t = actualize_decl_level env (Type s) t in
+	(na,None,t)::ctx, cons_subst u s subst
+      else
+	d::ctx, subst
+  | sign, [], _ ->
+      (* Uniform parameters are exhausted *)
+      sign,[]
+  | [], _, _ ->
+      assert false
+
+let instantiate_universes env ctx ar argsorts =
+  let args = Array.to_list argsorts in
+  let ctx,subst = make_subst env (ctx,ar.poly_param_levels,args) in
+  let level = subst_large_constraints subst ar.poly_level in
+  ctx,
+  if is_empty_univ level then mk_Prop
+  else if is_base_univ level then mk_Set
+  else Type level
 
 let type_of_inductive_knowing_parameters env mip paramtyps =
   match mip.mind_arity with
   | Monomorphic s ->
       s.mind_user_arity
   | Polymorphic ar ->
-      let s = instantiate_inductive_with_param_levels env ar mip paramtyps in
-      mkArity (mip.mind_arity_ctxt,s)
+      let ctx = List.rev mip.mind_arity_ctxt in
+      let ctx,s = instantiate_universes env ctx ar paramtyps in
+      mkArity (List.rev ctx,s)
+
+(* Type of a (non applied) inductive type *)
+
+let type_of_inductive env (_,mip) =
+  type_of_inductive_knowing_parameters env mip [||]
 
 (* The max of an array of universes *)
 
@@ -188,18 +207,6 @@ let cumulate_constructor_univ u = function
 let max_inductive_sort =
   Array.fold_left cumulate_constructor_univ neutral_univ
 
-(* Type of a (non applied) inductive type *)
-
-let type_of_inductive (_,mip) =
-  match mip.mind_arity with
-  | Monomorphic s -> s.mind_user_arity
-  | Polymorphic s ->
-      let subst = map_succeed (function
-	| Some u -> (u, fresh_local_univ ())
-	| None -> failwith "") s.mind_param_levels in
-      let s = mkSort (sort_of_instantiated_universe mip subst s.mind_level) in
-      it_mkProd_or_LetIn s mip.mind_arity_ctxt
-
 (************************************************************************)
 (* Type of a constructor *)
 
@@ -364,7 +371,7 @@ let inductive_equiv env (kn1,i1) (kn2,i2) =
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
-    (indsp <> ci.ci_ind) or
+    not (Closure.mind_equiv env indsp ci.ci_ind) or
     (mib.mind_nparams <> ci.ci_npar) or
     (mip.mind_consnrealdecls <> ci.ci_cstr_nargs)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index d81904cc..b9d0f984 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: inductive.mli 8871 2006-05-28 16:46:48Z herbelin $ i*)
+(*i $Id: inductive.mli 9314 2006-10-29 20:11:08Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -35,8 +35,9 @@ type mind_specif = mutual_inductive_body * one_inductive_body
 val lookup_mind_specif : env -> inductive -> mind_specif
 
 (*s Functions to build standard types related to inductive *)
+val ind_subst : mutual_inductive -> mutual_inductive_body -> constr list
 
-val type_of_inductive : mind_specif -> types
+val type_of_inductive : env -> mind_specif -> types
 
 val elim_sorts : mind_specif -> sorts_family list
 
@@ -49,6 +50,7 @@ val arities_of_constructors : inductive -> mind_specif -> types array
 (* Transforms inductive specification into types (in nf) *)
 val arities_of_specif : mutual_inductive -> mind_specif -> types array 
 
+
 (* [type_case_branches env (I,args) (p:A) c] computes useful types
    about the following Cases expression:
       <p>Cases (c :: (I args)) of b1..bn end
@@ -78,10 +80,11 @@ val check_cofix : env -> cofixpoint -> unit
 val type_of_inductive_knowing_parameters :
   env -> one_inductive_body -> types array -> types
 
-val set_inductive_level : env -> sorts -> types -> types
-
 val max_inductive_sort : sorts array -> universe
 
+val instantiate_universes : env -> Sign.rel_context ->
+    polymorphic_arity -> types array -> Sign.rel_context * sorts
+
 (***************************************************************)
 (* Debug *)
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index a8aff184..663434ec 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mod_typing.ml 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: mod_typing.ml 9310 2006-10-28 19:35:09Z herbelin $ i*)
 
 open Util
 open Names
@@ -87,8 +87,8 @@ and merge_with env mtb with_decl =
 		match cb.const_body with
 		  | None -> 
 		      let (j,cst1) = Typeops.infer env' c in
-		      let cst2 = 
-			Reduction.conv_leq env' j.uj_type cb.const_type in
+		      let typ = Typeops.type_of_constant_type env' cb.const_type in
+		      let cst2 = Reduction.conv_leq env' j.uj_type typ in
 		      let cst = 
 			Constraint.union 
 			  (Constraint.union cb.const_constraints cst1)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index b2f02a5f..5cc2a84d 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 8879 2006-05-30 21:32:10Z letouzey $ i*)
+(*i $Id: modops.ml 9138 2006-09-14 15:20:45Z jforest $ i*)
 
 (*i*)
 open Util
@@ -170,34 +170,6 @@ and subst_module sub mb =
 let subst_signature_msid msid mp = 
   subst_signature (map_msid msid mp)
 
-let rec constants_of_specification env mp sign =
- let aux res (l,elem) =
-  match elem with
-   | SPBconst cb -> ((make_con mp empty_dirpath l),cb)::res
-   | SPBmind _ -> res
-   | SPBmodule mb ->
-      (constants_of_modtype env (MPdot (mp,l))
-        (module_body_of_spec mb).mod_type) @ res
-   | SPBmodtype mtb -> res (* ???? *)
- in
-  List.fold_left aux [] sign
-
-and constants_of_modtype env mp modtype =
- match scrape_modtype env modtype with
-    MTBident _ -> anomaly "scrape_modtype does not work!"
-  | MTBsig (msid,sign) ->
-     constants_of_specification env mp
-      (subst_signature_msid msid mp sign)
-  | MTBfunsig _ -> []
-
-(* returns a resolver for kn that maps mbid to mp *)
-(* Nota: Some delta-expansions used to happen here. 
-    Browse SVN if you want to know more. *)
-let resolver_of_environment mbid modtype mp env =
- let constants = constants_of_modtype env (MPbound mbid) modtype in
- let resolve = List.map (fun (con,_) -> con,None) constants in 
- Mod_subst.make_resolver resolve
-
 (* we assume that the substitution of "mp" into "msid" is already done
 (or unnecessary) *)
 let rec add_signature mp sign env = 
@@ -224,6 +196,53 @@ and add_module mp mb env =
       | MTBfunsig _ -> env
 
 
+let rec constants_of_specification env mp sign =
+ let aux (env,res) (l,elem) =
+  match elem with
+   | SPBconst cb -> env,((make_con mp empty_dirpath l),cb)::res
+   | SPBmind _ -> env,res
+   | SPBmodule mb ->
+       let new_env =  add_module (MPdot (mp,l)) (module_body_of_spec mb) env in 
+       new_env,(constants_of_modtype env (MPdot (mp,l))
+		  (module_body_of_spec mb).mod_type) @ res
+   | SPBmodtype mtb -> 
+       (* module type dans un module type. 
+	  Il faut au moins mettre mtb dans l'environnement (avec le bon 
+	  kn pour pouvoir continuer aller deplier les modules utilisant ce 
+	  mtb
+	  ex: 
+	  Module Type T1. 
+	  Module Type T2.
+	     ....
+    	    End T2.
+	  .....
+            Declare Module M : T2.
+         End T2 
+	  si on ne rajoute pas T2 dans l'environement de typage 
+	  on va exploser au moment du Declare Module
+       *)
+       let new_env = Environ.add_modtype (make_kn mp empty_dirpath l) mtb env in 
+       new_env, constants_of_modtype env (MPdot(mp,l)) mtb @ res
+ in
+ snd (List.fold_left aux (env,[]) sign)
+
+and constants_of_modtype env mp modtype =
+ match scrape_modtype env modtype with
+    MTBident _ -> anomaly "scrape_modtype does not work!"
+  | MTBsig (msid,sign) ->
+     constants_of_specification env mp
+      (subst_signature_msid msid mp sign)
+  | MTBfunsig _ -> []
+
+(* returns a resolver for kn that maps mbid to mp *)
+(* Nota: Some delta-expansions used to happen here. 
+    Browse SVN if you want to know more. *)
+let resolver_of_environment mbid modtype mp env =
+ let constants = constants_of_modtype env (MPbound mbid) modtype in
+ let resolve = List.map (fun (con,_) -> con,None) constants in 
+ Mod_subst.make_resolver resolve
+
+
 let strengthen_const env mp l cb = 
   match cb.const_opaque, cb.const_body with
   | false, Some _ -> cb
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index bd849dad..701020d0 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: reduction.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: reduction.ml 9215 2006-10-05 15:40:31Z herbelin $ *)
 
 open Util
 open Names
@@ -257,14 +257,14 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
 
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
-     | (FInd (kn1,i1), FInd (kn2,i2)) ->
-         if i1 = i2 && mind_equiv infos kn1 kn2
+     | (FInd ind1, FInd ind2) ->
+         if mind_equiv_infos infos ind1 ind2
 	 then
            convert_stacks infos lft1 lft2 v1 v2 cuniv
          else raise NotConvertible
 
-     | (FConstruct ((kn1,i1),j1), FConstruct ((kn2,i2),j2)) ->
-	 if i1 = i2 && j1 = j2 && mind_equiv infos kn1 kn2
+     | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
+	 if j1 = j2 && mind_equiv_infos infos ind1 ind2
 	 then
            convert_stacks infos lft1 lft2 v1 v2 cuniv
          else raise NotConvertible
@@ -317,7 +317,7 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
 and convert_stacks infos lft1 lft2 stk1 stk2 cuniv =
   compare_stacks
     (fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c)
-    (fun (mind1,i1) (mind2,i2) -> i1=i2 && mind_equiv infos mind1 mind2)
+    (mind_equiv_infos infos)
     lft1 stk1 lft2 stk2 cuniv
 
 and convert_vect infos lft1 lft2 v1 v2 cuniv =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 95092814..c4d9c991 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: safe_typing.ml 8898 2006-06-05 23:15:51Z letouzey $ *)
+(* $Id: safe_typing.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
 
 open Util
 open Names
@@ -119,6 +119,12 @@ type global_declaration =
   | ConstantEntry of constant_entry
   | GlobalRecipe of Cooking.recipe
 
+let hcons_constant_type = function
+  | NonPolymorphicType t ->
+      NonPolymorphicType (hcons1_constr t)
+  | PolymorphicArity (ctx,s) ->
+      PolymorphicArity (map_rel_context hcons1_constr ctx,s)
+
 let hcons_constant_body cb =
   let body = match cb.const_body with
       None -> None
@@ -127,28 +133,28 @@ let hcons_constant_body cb =
   in
     { cb with
 	const_body = body;
-	const_type = hcons1_constr cb.const_type }
+	const_type = hcons_constant_type cb.const_type }
 
 let add_constant dir l decl senv =
   check_label l senv.labset;
-  let kn = make_con senv.modinfo.modpath dir l in 
+  let kn = make_con 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 kn r in
-	if dir = empty_dirpath then hcons_constant_body cb else cb
+      | ConstantEntry ce -> translate_constant senv.env kn ce
+      | GlobalRecipe r ->
+	  let cb = translate_recipe senv.env kn r in
+	    if dir = empty_dirpath then hcons_constant_body cb else cb
   in
   let env' = Environ.add_constraints cb.const_constraints senv.env in
   let env'' = Environ.add_constant kn cb env' in
-  kn, { old = senv.old;
-	env = env'';
-	modinfo = senv.modinfo;
-	labset = Labset.add l senv.labset;
-	revsign = (l,SPBconst cb)::senv.revsign;
-	revstruct = (l,SEBconst cb)::senv.revstruct;
-	imports = senv.imports;
-	loads = senv.loads }
+    kn, { old = senv.old;
+	  env = env'';
+	  modinfo = senv.modinfo;
+	  labset = Labset.add l senv.labset;
+	  revsign = (l,SPBconst cb)::senv.revsign;
+	  revstruct = (l,SEBconst cb)::senv.revstruct;
+	  imports = senv.imports;
+	  loads = senv.loads }
     
 
 (* Insertion of inductive types. *)
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 75342f2c..b42ca581 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: sign.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: sign.ml 9103 2006-09-01 11:02:52Z herbelin $ *)
 
 open Names
 open Util
@@ -83,6 +83,9 @@ let map_context f l =
 let map_rel_context = map_context
 let map_named_context = map_context
 
+let iter_rel_context f = List.iter (fun (_,b,t) -> f t; option_iter f b)
+let iter_named_context f = List.iter (fun (_,b,t) -> f t; option_iter f b)
+
 (* Push named declarations on top of a rel context *)
 (* Bizarre. Should be avoided. *)
 let push_named_to_rel_context hyps ctxt =
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 4a90302b..88e9dbf0 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: sign.mli 6737 2005-02-18 20:49:43Z herbelin $ i*)
+(*i $Id: sign.mli 9103 2006-09-01 11:02:52Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -65,6 +65,12 @@ val map_rel_context : (constr -> constr) -> rel_context -> rel_context
 (*s Map function of [named_context] *)
 val map_named_context : (constr -> constr) -> named_context -> named_context
 
+(*s Map function of [rel_context] *)
+val iter_rel_context : (constr -> unit) -> rel_context -> unit
+
+(*s Map function of [named_context] *)
+val iter_named_context : (constr -> unit) -> named_context -> unit
+
 (*s Term constructors *)
 
 val it_mkLambda_or_LetIn : constr -> rel_context -> constr
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index bbc89e39..9a8de5a9 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtyping.ml 8845 2006-05-23 07:41:58Z herbelin $ i*)
+(*i $Id: subtyping.ml 9310 2006-10-28 19:35:09Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -94,9 +94,9 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
       (* listrec ignored *)
       (* finite done *)
       (* nparams done *)
-      (* params_ctxt done *)
+      (* params_ctxt done because part of the inductive types *)
       (* Don't check the sort of the type if polymorphic *)
-      let cst = check_conv cst conv env (type_of_inductive (mib1,p1)) (type_of_inductive (mib2,p2))
+      let cst = check_conv cst conv env (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2))
       in
 	cst
   in
@@ -114,9 +114,12 @@ let check_inductive cst env msid1 l info1 mib2 spec2 =
   assert (Array.length mib1.mind_packets >= 1 
 	    && Array.length mib2.mind_packets >= 1);
 
-       (* TODO: we should allow renaming of parameters at least ! *)
+  (* Check that the expected numbers of uniform parameters are the same *)
+  (* No need to check the contexts of parameters: it is checked *)
+  (* at the time of checking the inductive arities in check_packet. *)
+  (* Notice that we don't expect the local definitions to match: only *)
+  (* the inductive types and constructors types have to be convertible *)
   check (fun mib -> mib.mind_nparams);
-  check (fun mib -> mib.mind_params_ctxt); 
 
   begin 
     match mib2.mind_equiv with
@@ -161,7 +164,9 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
    | Constant cb1 ->
       assert (cb1.const_hyps=[] && cb2.const_hyps=[]) ;
       (*Start by checking types*)
-      let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in
+      let typ1 = Typeops.type_of_constant_type env cb1.const_type in
+      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+      let cst = check_conv cst conv_leq env typ1 typ2 in
       let con = make_con (MPself msid1) empty_dirpath l in
       let cst =
        match cb2.const_body with
@@ -176,23 +181,27 @@ let check_constant cst env msid1 l info1 cb2 spec2 =
       in
        cst
    | IndType ((kn,i),mind1) ->
-      Util.error ("The kernel does not recognize yet that a parameter can be " ^
+      ignore (Util.error (
+       "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by an inductive type. Hint: you can rename the " ^
        "inductive type and give a definition to map the old name to the new " ^
-       "name.") ;
+       "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
       if cb2.const_body <> None then error () ;
-      let arity1 = type_of_inductive (mind1,mind1.mind_packets.(i)) in
-       check_conv cst conv_leq env arity1 cb2.const_type
+      let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in
+      let typ2 = Typeops.type_of_constant_type env cb2.const_type in
+       check_conv cst conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
-      Util.error ("The kernel does not recognize yet that a parameter can be " ^
+      ignore (Util.error (
+       "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
-       "name.") ;
+       "name."));
       assert (mind1.mind_hyps=[] && cb2.const_hyps=[]) ;
       if cb2.const_body <> None then error () ;
       let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in
-       check_conv cst conv env ty1 cb2.const_type
+      let ty2 = Typeops.type_of_constant_type env cb2.const_type in
+       check_conv cst conv env ty1 ty2
    | _ -> error ()
 	      
 let rec check_modules cst env msid1 l msb1 msb2 =
diff --git a/kernel/term.ml b/kernel/term.ml
index 228ae48a..456a29e4 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term.ml 8850 2006-05-23 16:11:31Z herbelin $ *)
+(* $Id: term.ml 9303 2006-10-27 21:50:17Z herbelin $ *)
 
 (* This module instantiates the structure of generic deBruijn terms to Coq *)
 
@@ -646,6 +646,9 @@ type rel_declaration = name * constr option * types
 let map_named_declaration f (id, v, ty) = (id, option_map f v, f ty)
 let map_rel_declaration = map_named_declaration
 
+let fold_named_declaration f (_, v, ty) a = f ty (option_fold_right f v a)
+let fold_rel_declaration = fold_named_declaration
+
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
 (****************************************************************************)
@@ -659,17 +662,16 @@ exception LocalOccur
 (* (closedn n M) raises FreeVar if a variable of height greater than n
    occurs in M, returns () otherwise *)
 
-let closedn = 
+let closedn n c = 
   let rec closed_rec n c = match kind_of_term c with
     | Rel m -> if m>n then raise LocalOccur
     | _ -> iter_constr_with_binders succ closed_rec n c
   in 
-  closed_rec
+  try closed_rec n c; true with LocalOccur -> false
 
 (* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
 
-let closed0 term =
-  try closedn 0 term; true with LocalOccur -> false
+let closed0 = closedn 0
 
 (* (noccurn n M) returns true iff (Rel n) does NOT occur in term M  *)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index 8d72e0d8..d6244f5b 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: term.mli 8850 2006-05-23 16:11:31Z herbelin $ i*)
+(*i $Id: term.mli 9303 2006-10-27 21:50:17Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -327,6 +327,11 @@ val map_named_declaration :
 val map_rel_declaration :
   (constr -> constr) -> rel_declaration -> rel_declaration
 
+val fold_named_declaration :
+  (constr -> 'a -> 'a) -> named_declaration -> 'a -> 'a
+val fold_rel_declaration :
+  (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
+
 (* Constructs either [(x:t)c] or [[x=b:t]c] *)
 val mkProd_or_LetIn : rel_declaration -> types -> types
 val mkNamedProd_or_LetIn : named_declaration -> types -> types
@@ -426,6 +431,9 @@ val under_outer_cast : (constr -> constr) -> constr -> constr
 
 (*s Occur checks *)
 
+(* [closedn n M] is true iff [M] is a (deBruijn) closed term under n binders *)
+val closedn : int -> constr -> bool
+
 (* [closed0 M] is true iff [M] is a (deBruijn) closed term *)
 val closed0 : constr -> bool
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index fde5fa25..575330a4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: term_typing.ml 7639 2005-12-02 10:01:15Z gregoire $ *)
+(* $Id: term_typing.ml 9323 2006-10-30 23:05:29Z herbelin $ *)
 
 open Util
 open Names
@@ -23,7 +23,20 @@ open Indtypes
 open Typeops
 
 let constrain_type env j cst1 = function
-  | None -> j.uj_type, cst1
+  | None ->
+(* To have definitions in Type polymorphic
+      make_polymorphic_if_arity env j.uj_type, cst1
+*) 
+      NonPolymorphicType j.uj_type, cst1
+  | Some t -> 
+      let (tj,cst2) = infer_type env t in
+      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
+      assert (t = tj.utj_val);
+      NonPolymorphicType t, Constraint.union (Constraint.union cst1 cst2) cst3
+
+let local_constrain_type env j cst1 = function
+  | None ->
+      j.uj_type, cst1
   | Some t -> 
       let (tj,cst2) = infer_type env t in
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
@@ -32,7 +45,7 @@ let constrain_type env j cst1 = function
 
 let translate_local_def env (b,topt) =
   let (j,cst) = infer env b in
-  let (typ,cst) = constrain_type env j cst topt in
+  let (typ,cst) = local_constrain_type env j cst topt in
     (j.uj_val,typ,cst)
 
 let translate_local_assum env t =
@@ -83,16 +96,25 @@ let infer_declaration env dcl =
         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, false
+      None, NonPolymorphicType (Typeops.assumption_of_judgment env j), cst,
+        false, false
+
+let global_vars_set_constant_type env = function
+  | NonPolymorphicType t -> global_vars_set env t
+  | PolymorphicArity (ctx,_) ->
+      Sign.fold_rel_context 
+        (fold_rel_declaration
+	  (fun t c -> Idset.union (global_vars_set env t) c))
+      ctx ~init:Idset.empty
 
 let build_constant_declaration env kn (body,typ,cst,op,boxed) =
   let ids =
     match body with 
-    | None -> global_vars_set env typ
+    | None -> global_vars_set_constant_type env typ
     | Some b ->
         Idset.union 
 	  (global_vars_set env (Declarations.force b)) 
-	  (global_vars_set env typ)
+	  (global_vars_set_constant_type env typ)
   in
   let tps = Cemitcodes.from_val (compile_constant_body env body op boxed) in
   let hyps = keep_hyps env ids in
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index cf111b6b..c102d01b 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: term_typing.mli 6245 2004-10-20 13:50:08Z barras $ i*)
+(*i $Id: term_typing.mli 9310 2006-10-28 19:35:09Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -24,7 +24,14 @@ val translate_local_def : env -> constr * types option ->
 
 val translate_local_assum : env -> types ->
   types * Univ.constraints
- 
+
+val infer_declaration : env -> constant_entry -> 
+   constr_substituted option * constant_type * constraints * bool * bool
+
+val build_constant_declaration : env -> 'a ->
+    constr_substituted option * constant_type * constraints * bool * bool ->
+      constant_body
+
 val translate_constant : env -> constant -> constant_entry -> constant_body
 
 val translate_mind : 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 8299a3c9..2a0dd526 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: typeops.ml 8871 2006-05-28 16:46:48Z herbelin $ *)
+(* $Id: typeops.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
 
 open Util
 open Names
@@ -49,8 +49,6 @@ let assumption_of_judgment env j =
 
 let sort_judgment env j = (type_judgment env j).utj_type
 
-let on_judgment_type f j = { j with uj_type = f j.uj_type }
-
 (************************************************)
 (* Incremental typing rules: builds a typing judgement given the *)
 (* judgements for the subterms. *)
@@ -127,13 +125,52 @@ let check_hyps id env hyps =
 *)
 (* Instantiation of terms on real arguments. *)
 
+(* Make a type polymorphic if an arity *)
+
+let extract_level env p =
+  let _,c = dest_prod_assum env p in
+  match kind_of_term c with Sort (Type u) -> Some u | _ -> None
+
+let extract_context_levels env =
+  List.fold_left
+    (fun l (_,b,p) -> if b=None then extract_level env p::l else l) []
+
+let make_polymorphic_if_arity env t =
+  let params, ccl = dest_prod_assum env t in
+  match kind_of_term ccl with
+  | Sort (Type u) -> 
+      let param_ccls = extract_context_levels env params in
+      let s = { poly_param_levels = param_ccls; poly_level = u} in
+      PolymorphicArity (params,s)
+  | _ ->
+      NonPolymorphicType t
+
 (* Type of constants *)
+
+let type_of_constant_knowing_parameters env t paramtyps =
+  match t with
+  | NonPolymorphicType t -> t
+  | PolymorphicArity (sign,ar) ->
+      let ctx = List.rev sign in
+      let ctx,s = instantiate_universes env ctx ar paramtyps in
+      mkArity (List.rev ctx,s)
+
+let type_of_constant_type env t =
+  type_of_constant_knowing_parameters env t [||]
+
+let type_of_constant env cst =
+  type_of_constant_type env (constant_type env cst)
+
+let judge_of_constant_knowing_parameters env cst jl =
+  let c = mkConst cst in
+  let cb = lookup_constant cst env in
+  let _ = check_args env c cb.const_hyps in 
+  let paramstyp = Array.map (fun j -> j.uj_type) jl in
+  let t = type_of_constant_knowing_parameters env cb.const_type paramstyp in
+  make_judge c t
+
 let judge_of_constant env cst =
-  let constr = mkConst cst in
-  let _ =
-    let ce = lookup_constant cst env in
-    check_args env constr ce.const_hyps in 
-  make_judge constr (constant_type env cst)
+  judge_of_constant_knowing_parameters env cst [||]
 
 (* Type of a lambda-abstraction. *)
 
@@ -350,11 +387,16 @@ let rec execute env cstr cu =
     | App (f,args) ->
         let (jl,cu1) = execute_array env args cu in
 	let (j,cu2) =
-	  if isInd f then
-	    (* Sort-polymorphism of inductive types *)
-	    judge_of_inductive_knowing_parameters env (destInd f) jl, cu1
-	  else
-	    execute env f cu1
+	  match kind_of_term f with
+	    | Ind ind ->
+		(* Sort-polymorphism of inductive types *)
+		judge_of_inductive_knowing_parameters env ind jl, cu1
+	    | Const cst -> 
+		(* Sort-polymorphism of constant *)
+		judge_of_constant_knowing_parameters env cst jl, cu1
+	    | _ -> 
+		(* No sort-polymorphism *)
+		execute env f cu1
 	in
 	univ_combinator cu2 (judge_of_apply env j jl)
 	    
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 86a795b5..64a2f650 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: typeops.mli 8871 2006-05-28 16:46:48Z herbelin $ i*)
+(*i $Id: typeops.mli 9314 2006-10-29 20:11:08Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -14,6 +14,7 @@ open Univ
 open Term
 open Environ
 open Entries
+open Declarations
 (*i*)
 
 (*s Typing functions (not yet tagged as safe) *)
@@ -33,8 +34,6 @@ val infer_local_decls :
 
 val assumption_of_judgment :  env -> unsafe_judgment -> types
 val type_judgment          :  env -> unsafe_judgment -> unsafe_type_judgment
-val on_judgment_type       :  
-  (types -> types) -> unsafe_judgment -> unsafe_judgment
 
 (*s Type of sorts. *)
 val judge_of_prop_contents : contents -> unsafe_judgment
@@ -49,6 +48,9 @@ val judge_of_variable : env -> variable -> unsafe_judgment
 (*s type of a constant *)
 val judge_of_constant : env -> constant -> unsafe_judgment
 
+val judge_of_constant_knowing_parameters :
+  env -> constant -> unsafe_judgment array -> unsafe_judgment
+
 (*s Type of application. *)
 val judge_of_apply : 
   env -> unsafe_judgment -> unsafe_judgment array
@@ -95,3 +97,12 @@ val type_fixpoint : env -> name array -> types array
 (* Kernel safe typing but applicable to partial proofs *)
 val typing : env -> constr -> unsafe_judgment
 
+val type_of_constant : env -> constant -> types
+
+val type_of_constant_type : env -> constant_type -> types
+
+val type_of_constant_knowing_parameters : 
+  env -> constant_type -> constr array -> types
+
+(* Make a type polymorphic if an arity *)
+val make_polymorphic_if_arity : env -> types -> constant_type
diff --git a/kernel/univ.ml b/kernel/univ.ml
index e76b7b02..775e505f 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: univ.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: univ.ml 9314 2006-10-29 20:11:08Z herbelin $ *)
 
 (* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
 (* Extension with algebraic universes by HH [Sep 2001] *)
@@ -63,8 +63,8 @@ let pr_uni_level u = str (string_of_univ_level u)
 let pr_uni = function
   | Atom u -> 
       pr_uni_level u
-  | Max ([],[Base]) ->
-      int 1
+  | Max ([],[u]) ->
+      str "(" ++ pr_uni_level u ++ str ")+1"
   | Max (gel,gtl) ->
       str "max(" ++ hov 0
        (prlist_with_sep pr_coma pr_uni_level gel ++
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 653f8978..7c515735 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -17,7 +17,7 @@ let val_of_constr env c =
 let compare_zipper z1 z2 =
   match z1, z2 with
   | Zapp args1, Zapp args2 -> nargs args1 = nargs args2
-  | Zfix _, Zfix _ -> true 
+  | Zfix(f1,args1), Zfix(f2,args2) ->  nargs args1 = nargs args2
   | Zswitch _, Zswitch _ -> true
   | _ , _ -> false
 
@@ -42,8 +42,9 @@ let conv_vect fconv vect1 vect2 cu =
 
 let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
 
-let rec conv_val pb k v1 v2 cu =
-  if v1 == v2 then cu else conv_whd pb k (whd_val v1) (whd_val v2) cu 
+let rec conv_val pb k v1 v2 cu = 
+  if v1 == v2 then cu 
+  else conv_whd pb k (whd_val v1) (whd_val v2) cu
     
 and conv_whd pb k whd1 whd2 cu =  
   match whd1, whd2 with
@@ -52,21 +53,14 @@ and conv_whd pb k whd1 whd2 cu =
       let cu = conv_val CONV k (dom p1) (dom p2) cu in
       conv_fun pb k (codom p1) (codom p2) cu
   | Vfun f1, Vfun f2 -> conv_fun CONV k f1 f2 cu
-  | Vfix f1, Vfix f2 -> conv_fix 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 k args1 args2 (conv_fix k f1 f2 cu)
-  | Vcofix cf1, Vcofix cf2 -> 
-      conv_cofix 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 k args1 args2 (conv_cofix k cf1 cf2 cu)
+  | Vfix (f1,None), Vfix (f2,None) -> conv_fix k f1 f2 cu
+  | Vfix (f1,Some args1), Vfix(f2,Some args2) ->
+      if nargs args1 <> nargs args2 then raise NotConvertible
+      else conv_arguments k args1 args2 (conv_fix k f1 f2 cu)
+  | Vcofix (cf1,_,None), Vcofix (cf2,_,None) -> conv_cofix k cf1 cf2 cu
+  | Vcofix (cf1,_,Some args1), Vcofix (cf2,_,Some args2) ->	
+      if nargs args1 <> nargs args2 then raise NotConvertible
+      else conv_arguments k args1 args2 (conv_cofix k cf1 cf2 cu)
   | Vconstr_const i1, Vconstr_const i2 -> 
       if i1 = i2 then cu else raise NotConvertible 
   | Vconstr_block b1, Vconstr_block b2 ->
@@ -89,7 +83,8 @@ and conv_whd pb k whd1 whd2 cu =
 and conv_atom 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 && compare_stack stk1 stk2 then
+      if mind_equiv_infos !infos (kn1,i1) (kn2,i2) && compare_stack stk1 stk2
+      then
 	conv_stack k stk1 stk2 cu
       else raise NotConvertible
   | Aid ik1, Aid ik2 -> 
@@ -111,8 +106,6 @@ and conv_atom pb k a1 stk1 a2 stk2 cu =
       conv_whd pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
   | _, Aiddef(ik2,v2) ->
       conv_whd pb k (Vatom_stk(a1,stk1)) (force_whd 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 k stk1 stk2 cu =
@@ -120,22 +113,17 @@ and conv_stack k stk1 stk2 cu =
   | [], [] -> cu
   | Zapp args1 :: stk1, Zapp args2 :: stk2 ->
       conv_stack k stk1 stk2 (conv_arguments 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
+  | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 ->
       conv_stack k stk1 stk2 
 	(conv_arguments k args1 args2 (conv_fix k f1 f2 cu))
   | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
-      if eq_tbl sw1 sw2 then
+      if check_switch sw1 sw2 then
 	let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
 	let rcu = ref (conv_val 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 CONV (k + fst b1.(i)) 
-	      (snd b1.(i)) (snd b2.(i)) !rcu
+	    conv_val CONV (k + fst b1.(i)) (snd b1.(i)) (snd b2.(i)) !rcu
 	done;
 	conv_stack k stk1 stk2 !rcu
       else raise NotConvertible
@@ -151,24 +139,20 @@ and conv_fix 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 bf1, tf1 = reduce_fix k f1 in
+      let bf2, tf2 = reduce_fix k f2 in
       let cu = conv_vect (conv_val 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 CONV (k + (fix_ndef f1))) bf1 bf2 cu
+      conv_vect (conv_fun CONV (k + Array.length tf1)) bf1 bf2 cu
     else raise NotConvertible
 
 and conv_cofix 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 bcf1, tcf1 = reduce_cofix k cf1 in
+      let bcf2, tcf2 = reduce_cofix k cf2 in
       let cu = conv_vect (conv_val 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 CONV (k + (cofix_ndef cf1))) bcf1 bcf2 cu
+      conv_vect (conv_val CONV (k + Array.length tcf1)) bcf1 bcf2 cu
     else raise NotConvertible
 
 and conv_arguments k args1 args2 cu =
@@ -255,302 +239,4 @@ let set_use_vm b =
       
 let use_vm _ = !use_vm
 
-(*******************************************)
-(* 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 = List.rev (Array.to_list params) in substl sp ctyp2
-  
-let destApplication t =
-  try destApp 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 = mib.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 specif = Inductive.lookup_mind_specif env ind in
-  Inductive.type_of_inductive specif
-
-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,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
-
-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 = mib.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) 
-	    (hnf_prod_applist env (type_of_ind env ind) (Array.to_list params))
-	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
-  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) *) 
-
-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  =
-  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 then set_transp_values false; 
-  c
-  
 
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 4aed5d05..551615aa 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -19,28 +19,5 @@ val use_vm : unit -> bool
 val set_use_vm : bool -> unit
 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
+val val_of_constr : env -> constr -> values
 
-  
diff --git a/kernel/vm.ml b/kernel/vm.ml
index c8be979e..de9bd753 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -1,20 +1,16 @@
-open Obj
 open Names
 open Term
 open Conv_oracle
 open Cbytecodes
 
-
 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))
-let last o = (field o (size o - 1))
+external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
+external offset : Obj.t -> int = "coq_offset"
 
 let accu_tag = 0
 
@@ -34,8 +30,10 @@ external set_transp_values : bool -> unit = "coq_set_transp_value"
 (*******************************************)
 
 type tcode 
-let tcode_of_obj v = ((obj v):tcode)
-let fun_code v = tcode_of_obj (field (repr v) 0)
+let tcode_of_obj v = ((Obj.obj v):tcode)
+let fun_code v = tcode_of_obj (Obj.field (Obj.repr v) 0) 
+
+  
 
 external mkAccuCode : int -> tcode = "coq_makeaccu"
 external mkPopStopCode : int -> tcode = "coq_pushpop"
@@ -63,155 +61,26 @@ let popstop_code 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] *)
-(*              ^                         *)
+let val_of_obj v = ((Obj.obj v):values)
+let crasy_val = (val_of_obj (Obj.repr 0))
 
-(* Products *)
+(* Abstract data *)
 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 vfun
 type vfix
+type vcofix
+type vblock
+type arguments
 
-(* [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 vm_env      
 type vstack = values array
 
-type vm_env 
-
 type vswitch = {
     sw_type_code : tcode; 
     sw_code : tcode; 
@@ -220,138 +89,148 @@ type vswitch = {
     sw_env : vm_env
   } 
 
-(* Ne pas changer ce type sans modifier le code C *)
+(* Representation des types abstraits:                                    *)
+(* + Les produits :                                                       *)
+(*   -   vprod = 0_[ dom | codom]                                         *)
+(*             dom : values, codom : vfun                                 *)
+(*                                                                        *)
+(* + Les fonctions ont deux representations possibles :                   *)
+(*   - fonction non applique :  vf = Ct_[ C | fv1 | ... | fvn]            *) 
+(*                                       C:tcode, fvi : values            *)
+(*     Remarque : il n'y a pas de difference entre la fct et son          *)
+(*                environnement.                                          *) 
+(*   - Application partielle  : Ct_[Restart:C| vf | arg1 | ... argn]      *)
+(*                                                                        *)
+(* + Les points fixes :                                                   *)
+(*   -        Ct_[C1|Infix_t|C2|...|Infix_t|Cn|fv1|...|fvn]               *)
+(*     Remarque il n'y a qu'un seul block pour representer tout les       *)
+(*     points fixes d'une declaration mutuelle, chaque point fixe         *)
+(*     pointe sur la position de son code dans le block.                  *)
+(*   - L'application partielle d'un point fixe suit le meme schema        *)
+(*     que celui des fonctions                                            *)
+(*     Remarque seul les points fixes qui n'ont pas encore recu leur      *)
+(*     argument recursif sont encode de cette maniere (si l'argument      *)
+(*     recursif etait un constructeur le point fixe se serait reduit      *)
+(*     sinon il est represente par un accumulateur)                       *)
+(*                                                                        *)
+(* + Les cofix sont expliques dans cbytegen.ml                            *)
+(*                                                                        *)
+(* + Les vblock encodent les constructeurs (non constant) de caml,        *)
+(*   la difference est que leur tag commence a 1 (0 est reserve pour les  *)
+(*   accumulateurs : accu_tag)                                            *)
+(*                                                                        *)
+(* + vm_env est le type des environnement machine (une fct ou un pt fixe) *)
+(*                                                                        *)
+(* + Les accumulateurs : At_[accumulate| accu | arg1 | ... | argn ]       *)
+(*   - representation des [accu] : tag_[....]                             *)
+(*     -- tag <= 2 : encodage du type atom                                *)
+(*     -- 3_[accu|fix_app] : un point fixe bloque par un accu             *)
+(*     -- 4_[accu|vswitch] : un case bloque par un accu                   *)
+(*     -- 5_[fcofix]       : une fonction de cofix                        *)
+(*     -- 6_[fcofix|val]   : une fonction de cofix, val represente        *)
+(*        la valeur de la reduction de la fct applique a arg1 ... argn    *) 
+(* Le type [arguments] est utiliser de maniere abstraite comme un         *)
+(* tableau, il represente la structure de donnee suivante :               *)
+(*          tag[ _ | _ |v1|... | vn]                                      *)
+(* Generalement le 1er champs est un pointeur de code                     *)
+
+(* Ne pas changer ce type sans modifier le code C, *)
+(* en particulier le fichier "coq_values.h"        *)
 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
+  | Zfix of vfix*arguments  (* Peut-etre vide *)
   | Zswitch of vswitch
 
 type stack = zipper list
 
+type to_up = values
+
 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
+  | Vfix of vfix * arguments option
+  | Vcofix of vcofix * to_up * arguments option
   | 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 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 
-
-
 
 (*************************************************)
 (* Destructors ***********************************)
 (*************************************************)
 
-
 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 
-  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)
+    if Obj.size a = 2 then stk
+    else Zapp (Obj.obj a) :: stk in
+  let at = Obj.field a 1 in
+  match Obj.tag at with
+  | i when i <= 2 -> 
+      Vatom_stk(Obj.magic at, stk)
+  | 3 (* fix_app tag *) ->
+      let fa = Obj.field at 1 in
+      let zfix  = 
+	Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
+      whd_accu (Obj.field at 0) (zfix :: stk)
+  | 4 (* switch tag  *) ->
+      let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
+      whd_accu (Obj.field at 0) (zswitch :: stk)
+  | 5 (* cofix_tag *) ->
+      begin match stk with
+      | [] -> 
+	  let vcfx = Obj.obj (Obj.field at 0) in
+	  let to_up = Obj.obj a in
+	  Vcofix(vcfx, to_up, None)
+      | [Zapp args] ->
+	  let vcfx = Obj.obj (Obj.field at 0) in
+	  let to_up = Obj.obj a in
+	  Vcofix(vcfx, to_up, Some args)
+      | _           -> assert false
+      end
+  | 6 (* cofix_evaluated_tag *) ->
+      begin match stk with
+      | [] ->
+	  let vcofix = Obj.obj (Obj.field at 0) in
+	  let res = Obj.obj a in
+	  Vcofix(vcofix, res, None)
+      | [Zapp args] -> 
+	  let vcofix = Obj.obj (Obj.field at 0) in
+	  let res = Obj.obj a in
+	  Vcofix(vcofix, res, Some args)
+      | _ -> assert false
+      end
+  | _ -> assert false
 
-external kind_of_closure : t -> int = "coq_kind_of_closure"
+external kind_of_closure : Obj.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)
+    let o = Obj.repr v in 
+    if Obj.is_int o then Vconstr_const (Obj.obj o)
     else 
-      let tag = tag o in
+      let tag = Obj.tag o in
       if tag = accu_tag then
-	if is_accumulate (fun_code o) then whd_accu (obj o) []
+	(
+	if Obj.size o = 1 then Obj.obj o (* sort *)
 	else 
-	  if size o = 1 then Vsort(obj (field o 0))
-	  else Vprod(obj o)
+	  if is_accumulate (fun_code o) then whd_accu o []
+	  else (Vprod(Obj.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)
+	if tag = Obj.closure_tag || tag = Obj.infix_tag then
+	  (	   match kind_of_closure o with
+	   | 0 -> Vfun(Obj.obj o)
+	   | 1 -> Vfix(Obj.obj o, None)
+	   | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
+	   | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
+	   | _ -> Util.anomaly "Vm.whd : kind_of_closure does not work")
+	else Vconstr_block(Obj.obj o)
 	
 
 
@@ -359,7 +238,6 @@ let whd_val : values -> whd =
 (* La machine abstraite *************************)
 (************************************************)
 
-
 (* gestion de la pile *)
 external push_ra : tcode -> unit = "coq_push_ra"
 external push_val : values -> unit = "coq_push_val"
@@ -371,6 +249,17 @@ external push_vstack : vstack -> unit = "coq_push_vstack"
 external interprete : tcode -> values -> vm_env -> int -> values =
   "coq_interprete_ml"
 
+
+
+(* Functions over arguments *)
+let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
+let arg args i = 
+  if  0 <= i && i < (nargs args) then 
+    val_of_obj (Obj.field (Obj.repr args) (i+2))
+  else raise (Invalid_argument 
+		("Vm.arg size = "^(string_of_int (nargs args))^
+		 " acces "^(string_of_int i)))
+
 let apply_arguments vf vargs =
   let n = nargs vargs in
   if n = 0 then vf 
@@ -378,7 +267,7 @@ let apply_arguments vf vargs =
    begin
      push_ra stop;
      push_arguments vargs;
-     interprete (fun_code vf) vf (magic vf) (n - 1)
+     interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
    end
 
 let apply_vstack vf vstk =
@@ -388,80 +277,130 @@ let apply_vstack vf vstk =
     begin
       push_ra stop;
       push_vstack vstk;
-      interprete (fun_code vf) vf (magic vf) (n - 1)
+      interprete (fun_code vf) vf (Obj.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)
-
-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)
-  else 
-    (push_vstack sw.sw_stk; push_ra (popstop_code (Array.length sw.sw_stk)));
-  interprete sw.sw_code arg sw.sw_env 0
+(**********************************************)
+(* Constructeurs ******************************)
+(**********************************************)
 
-let is_accu v = 
-  is_block (repr v) && tag (repr v) = accu_tag && 
-  fun_code v == accumulate 
+let obj_of_atom : atom -> Obj.t =
+  fun a -> 
+    let res = Obj.new_block accu_tag 2 in
+    Obj.set_field res 0 (Obj.repr accumulate);
+    Obj.set_field res 1 (Obj.repr a);
+    res 
 
-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 
+(* obj_of_str_const : structured_constant -> Obj.t *)
+let rec obj_of_str_const str =
+  match str with 
+  | Const_sorts s -> Obj.repr (Vsort s)
+  | Const_ind ind -> obj_of_atom (Aind ind)
+  | Const_b0 tag -> Obj.repr tag
+  | Const_bn(tag, args) ->
+      let len = Array.length args in
+      let res = Obj.new_block tag len in
+      for i = 0 to len - 1 do 
+	Obj.set_field res i (obj_of_str_const args.(i)) 
+      done;
+      res
 
-let rec force_whd v stk =
-  match whd_stack v stk with
-  | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk
-  | res -> res
+let val_of_obj o = ((Obj.obj o) : values)
 
-	  
+let val_of_str_const str = val_of_obj (obj_of_str_const str)
 
-(* Function *)
-external closure_arity : vfun -> int = "coq_closure_arity"
+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 n c v = 
+  let res = Obj.new_block accu_tag 2 in
+  Obj.set_field res 0 (Obj.repr (mkAccuCond n));
+  Obj.set_field res 1 (Obj.repr (Aiddef(ConstKey c, v)));
+  val_of_obj res
 
-(* [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))
 
+(*************************************************)
+(** Operations pour la manipulation des donnees **)
+(*************************************************)
+
+
+(* Functions over products *)
+
+let dom : vprod -> values = fun p -> val_of_obj (Obj.field (Obj.repr p) 0) 
+let codom : vprod -> vfun = fun p -> (Obj.obj (Obj.field (Obj.repr p) 1))
+
+(* Functions over vfun *)
+
+external closure_arity : vfun -> int = "coq_closure_arity"
+
 let body_of_vfun k vf =
   let vargs = mkrel_vstack k 1 in
-  apply_vstack (magic vf) vargs
+  apply_vstack (Obj.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);
+  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
+  let v1 = apply_vstack (Obj.magic vf1) vargs in
+  let v2 = apply_vstack (Obj.magic vf2) vargs in
   arity, v1, v2
-    
+
+(* Functions over fixpoint *)
+
+let first o = (offset_closure o (offset o))
+let last o = (Obj.field o (Obj.size o - 1))
+
+let current_fix vf = - (offset (Obj.repr vf) / 2)
+
+let unsafe_fb_code fb i = tcode_of_obj (Obj.field (Obj.repr fb) (2 * i))
+
+let unsafe_rec_arg fb i = int_tcode (unsafe_fb_code fb i) 1
   
-(* Fix *)
+let rec_args vf =
+  let fb = first (Obj.repr vf) in
+  let size = Obj.size (last fb) in
+  Array.init size (unsafe_rec_arg fb)
+
+exception FALSE
+
+let check_fix f1 f2 = 
+  let i1, i2 = current_fix f1, current_fix f2 in
+  (* Verification du point de depart *)
+  if i1 = i2 then
+    let fb1,fb2 = first (Obj.repr f1), first (Obj.repr f2) in
+    let n = Obj.size (last fb1) in
+    (* Verification du nombre de definition *)
+    if n = Obj.size (last fb2) then
+      (* Verification des arguments recursifs *)
+      try
+	for i = 0 to n - 1 do
+	  if unsafe_rec_arg fb1 i <> unsafe_rec_arg fb2 i
+	  then raise FALSE
+	done;
+	true
+      with FALSE -> false
+    else false 
+  else false
+
+(* Functions over vfix *)
 external atom_rel : unit -> atom array = "get_coq_atom_tbl"
 external realloc_atom_rel : int -> unit = "realloc_coq_atom_tbl"
 
@@ -486,69 +425,89 @@ let relaccu_code i =
       !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
+let reduce_fix k vf =
+  let fb = first (Obj.repr vf) in
+  (* calcul des types *)
+  let fc_typ = ((Obj.obj (last fb)) : tcode array) in
+  let ndef = Array.length fc_typ in
+  let et = offset_closure fb (2*(ndef - 1)) in
+  let ftyp =  
+    Array.map 
+      (fun c -> interprete c crasy_val (Obj.magic et) 0) fc_typ in
   (* Construction de l' environnement des corps des points fixes *)
-  let e = dup (repr fb) in
+  let e = Obj.dup fb in
   for i = 0 to ndef - 1 do
-    set_field e (2 * i) (repr (relaccu_code (k + i)))
+    Obj.set_field e (2 * i) (Obj.repr (relaccu_code (k + i)))
   done;
   let fix_body i =
+    let jump_grabrec c = offset_tcode c 2 in
     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
-
+    let res = Obj.new_block Obj.closure_tag 2 in
+    Obj.set_field res 0 (Obj.repr c);
+    Obj.set_field res 1 (offset_closure e (2*i));
+    ((Obj.obj res) : vfun)  in 
+  (Array.init ndef fix_body, ftyp)
  
-(* 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
+(* Functions over vcofix *)
+
+let get_fcofix vcf i = 
+  match whd_val (Obj.obj (Obj.field (Obj.repr vcf) (i+1))) with
+  | Vcofix(vcfi, _, _) -> vcfi
+  | _ -> assert false
+
+let current_cofix vcf =
+  let ndef = Obj.size (last (Obj.repr vcf)) in
+  let rec find_cofix pos =
+    if pos < ndef then
+      if get_fcofix vcf pos == vcf then pos
+      else find_cofix (pos+1)
+    else raise Not_found in
+  try find_cofix 0
+  with _ -> assert false
+
+let check_cofix vcf1 vcf2 =
+  (current_cofix vcf1 = current_cofix vcf2) &&
+  (Obj.size (last (Obj.repr vcf1)) = Obj.size (last (Obj.repr vcf2)))
+
+external print_point : Obj.t -> unit = "coq_print_pointer"
+
+let reduce_cofix k vcf =
+  let fc_typ = ((Obj.obj (last (Obj.repr vcf))) : tcode array) in
+  let ndef = Array.length fc_typ in
+  let ftyp =  
+    Array.map (fun c -> interprete c crasy_val (Obj.magic vcf) 0) fc_typ in
+  (* Construction de l'environnement des corps des cofix *)
+
+  let max = k + ndef - 1 in 
+  let e = Obj.dup (Obj.repr vcf) in 
   for i = 0 to ndef - 1 do
-    set_field e (2 * i) (repr (relaccu_code (k + i)))
+    Obj.set_field e (i+1) (Obj.repr (val_of_rel (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 vcfi = get_fcofix vcf i in
+    let c = Obj.field (Obj.repr vcfi) 0 in
+    Obj.set_field e 0 c; 
+    let atom = Obj.new_block cofix_tag 1 in
+    let self = Obj.new_block accu_tag 2 in
+    Obj.set_field self 0 (Obj.repr accumulate);
+    Obj.set_field self 1 (Obj.repr atom);
+    apply_vstack (Obj.obj e) [|Obj.obj self|] in  
+  (Array.init ndef cofix_body, ftyp)
+
+
+(* Functions over vblock *)
+  
+let btag : vblock -> int = fun b -> Obj.tag (Obj.repr b)
+let bsize : vblock -> int = fun b -> Obj.size (Obj.repr b)
+let bfield b i =
+  if 0 <= i && i < (bsize b) then val_of_obj (Obj.field (Obj.repr b) i)
+  else raise (Invalid_argument "Vm.bfield")
+
+
+(* Functions over vswitch *)
+
+let check_switch sw1 sw2 = sw1.sw_annot.rtbl = sw2.sw_annot.rtbl 
     
 let case_info sw = sw.sw_annot.ci
     
@@ -557,15 +516,22 @@ let type_of_switch sw =
   interprete sw.sw_type_code crasy_val sw.sw_env 0 
     
 let branch_arg k (tag,arity) = 
-  if arity = 0 then  ((magic tag):values)
+  if arity = 0 then  ((Obj.magic tag):values)
   else
-    let b = new_block tag arity in
+    let b = Obj.new_block tag arity in
     for i = 0 to arity - 1 do
-      set_field b i (repr (val_of_rel (k+i)))
+      Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
     done;
     val_of_obj b
-  
-      
+
+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 branch_of_switch k sw =
   let eval_branch (_,arity as ta) =
     let arg = branch_arg k ta in
@@ -573,27 +539,62 @@ let branch_of_switch k sw =
     (arity, v)
   in 
   Array.map eval_branch sw.sw_annot.rtbl
-    
-
-    
-
-
-
-
-
-
-
-
-
-
-
-
-
+	
 
+(* Evaluation *)
 
 
+let is_accu v = 
+  let o = Obj.repr v in
+  Obj.is_block o && Obj.tag o = accu_tag && 
+  fun_code v == accumulate && Obj.tag (Obj.field o 1) < cofix_tag 
 
+let rec whd_stack v stk =  
+  match stk with
+  | [] -> whd_val v
+  | Zapp args :: stkt -> whd_stack (apply_arguments v args) stkt
+  | Zfix (f,args) :: stkt -> 
+      let o = Obj.repr v in
+      if Obj.is_block o && Obj.tag o = accu_tag then
+	whd_accu (Obj.repr v) stk
+      else 
+	let v', stkt =
+	  match stkt with
+	  | Zapp args' :: stkt ->
+	      push_ra stop;
+	      push_arguments args';
+	      push_val v;
+	      push_arguments args;
+	      let v' =
+		interprete (fun_code f) (Obj.magic f) (Obj.magic f) 
+		  (nargs args+ nargs args') in
+	      v', stkt
+	  | _ -> 
+	      push_ra stop;
+	      push_val v;
+	      push_arguments args;
+	      let v' =
+		interprete (fun_code f) (Obj.magic f) (Obj.magic f) 
+		  (nargs args) in
+	      v', stkt
+	in
+	whd_stack v' stkt
+  | Zswitch sw :: stkt -> 
+      let o = Obj.repr v in
+      if Obj.is_block o && Obj.tag o = accu_tag then
+	if Obj.tag (Obj.field o 1) < cofix_tag then whd_accu (Obj.repr v) stk
+	else
+	  let to_up = 
+	    match whd_accu (Obj.repr v) [] with
+	    | Vcofix (_, to_up, _) -> to_up
+	    | _ -> assert false in
+	  whd_stack (apply_switch sw to_up) stkt
+      else whd_stack (apply_switch sw v) stkt 
 
+let rec force_whd v stk =
+  match whd_stack v stk with
+  | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk
+  | res -> res
 
 
 
diff --git a/kernel/vm.mli b/kernel/vm.mli
index b5fd9b9d..279ac937 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -13,45 +13,41 @@ 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 atom = 
+  | Aid of id_key
+  | Aiddef of id_key * values
+  | Aind of inductive
+
+(* Les zippers *)
+
 type zipper =
   | Zapp of arguments
-  | Zfix of vfix_app
+  | Zfix of vfix*arguments  (* Peut-etre vide *)
   | 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 to_up
 
 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
+  | Vfix of vfix * arguments option
+  | Vcofix of vcofix * to_up * arguments option
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vatom_stk of atom * stack
-
-(* Constructors *)
+ 
+(** Constructors *)
 val val_of_str_const : structured_constant -> values
 
 val val_of_rel : int -> values 
@@ -63,44 +59,43 @@ val val_of_named_def : identifier -> values -> values
 val val_of_constant : constant -> values 
 val val_of_constant_def : int -> constant -> values -> values
 
-(* Destructors *)
+(** Destructors *)
 val whd_val : values -> whd
 
+(* Arguments *)  
+val nargs : arguments -> int
+val arg : arguments -> int -> values
+
 (* 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 current_fix : vfix -> int
 val check_fix : vfix -> vfix -> bool
-val bodies_of_fix : int -> vfix -> vfun array
-val types_of_fix : vfix -> values array
+val rec_args : vfix -> int array 
+val reduce_fix : int -> vfix -> vfun array * values array
+                              (* bodies ,  types *)
+
 (* CoFix *)
-val cofix : vcofix_app -> vcofix
-val args_of_cofix : vcofix_app -> arguments
-val cofix_init : vcofix -> int 
-val cofix_ndef : vcofix -> int
+val current_cofix : vcofix -> int 
 val check_cofix : vcofix -> vcofix -> bool
-val bodies_of_cofix : int -> vcofix -> values array
-val types_of_cofix : vcofix -> values array
+val reduce_cofix : int -> vcofix -> values array * values array
+                                      (* bodies , types *)
 (* Block *)
 val btag : vblock -> int
 val bsize : vblock -> int
 val bfield : vblock -> int -> values
+
 (* Switch *)
-val eq_tbl : vswitch -> vswitch -> bool
+val check_switch : 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