Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg

42 files changed, 446 insertions, 352 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 3fded663..1be3e651 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -13,6 +13,7 @@
 
 #include <stdio.h>
 #include <stdlib.h> 
+#include <stdint.h>
 #include <caml/config.h>
 #include <caml/misc.h>
 #include <caml/mlvalues.h>
@@ -146,21 +147,21 @@ value coq_tcode_of_code (value code, value size) {
     };
     *q++ = VALINSTR(instr);
     if (instr == SWITCH) {
-      uint32 i, sizes, const_size, block_size;
+      uint32_t i, sizes, const_size, block_size;
       COPY32(q,p); p++;
       sizes=*q++;
-      const_size = sizes & 0xFFFF;
-      block_size = sizes >> 16;
+      const_size = sizes & 0xFFFFFF;
+      block_size = sizes >> 24;
       sizes = const_size + block_size;
       for(i=0; i<sizes; i++) { COPY32(q,p); p++; q++; };
     } else if (instr == CLOSUREREC || instr==CLOSURECOFIX) {
-      uint32 i, n;
+      uint32_t i, n;
       COPY32(q,p); p++; /* ndefs */
       n = 3 + 2*(*q);  /* ndefs, nvars, start, typlbls,lbls*/
       q++;
       for(i=1; i<n; i++) { COPY32(q,p); p++; q++; };
     } else {
-      uint32 i, ar;
+      uint32_t i, ar;
       ar = arity[instr]; 
       for(i=0; i<ar; i++) { COPY32(q,p); p++; q++; };
     }
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index f9e0dc7f..0ab9f89f 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -15,6 +15,7 @@
 
 #include <stdio.h>
 #include <signal.h>
+#include <stdint.h>
 #include "coq_gc.h"
 #include "coq_instruct.h"
 #include "coq_fix_code.h"
@@ -30,9 +31,9 @@
 #endif
 
 /* spiwack: I append here a few macros for value/number manipulation */
-#define uint32_of_value(val) (((uint32)val >> 1))
-#define value_of_uint32(i)   ((value)(((uint32)(i) << 1) | 1))
-#define UI64_of_uint32(lo)  ((uint64)(I64_literal(0,(uint32)(lo))))
+#define uint32_of_value(val) (((uint32_t)val >> 1))
+#define value_of_uint32(i)   ((value)(((uint32_t)(i) << 1) | 1))
+#define UI64_of_uint32(lo)  ((uint64_t)(I64_literal(0,(uint32_t)(lo))))
 #define UI64_of_value(val) (UI64_of_uint32(uint32_of_value(val)))
 /* /spiwack */
 
@@ -788,14 +789,14 @@ value coq_interprete
 /* Access to components of blocks */
         
       Instruct(SWITCH) {
-	uint32 sizes = *pc++;
+	uint32_t sizes = *pc++;
 	print_instr("SWITCH");
-	print_int(sizes & 0xFFFF);
+	print_int(sizes & 0xFFFFFF);
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
 	  print_instr("block");
 	  print_int(index);
-	  pc += pc[(sizes & 0xFFFF) + index];
+	  pc += pc[(sizes & 0xFFFFFF) + index];
 	} else {
 	  long index = Long_val(accu);
 	  print_instr("constant");
@@ -1054,7 +1055,7 @@ value coq_interprete
            the one ontop of the stack (which is poped)*/
         print_instr("ADDINT31");
         accu = 
-           (value)((uint32) accu + (uint32) *sp++ - 1); 
+           (value)((uint32_t) accu + (uint32_t) *sp++ - 1); 
         /* nota,unlike CaML we don't want
            to have a different behavior depending on the 
            architecture. Thus we cast the operand to uint32 */
@@ -1064,9 +1065,9 @@ value coq_interprete
       Instruct (ADDCINT31) {
 	print_instr("ADDCINT31");
 	/* returns the sum with a carry */
-	uint32 s;
-	s = (uint32)accu + (uint32)*sp++ - 1;
-        if( (uint32)s < (uint32)accu ) {
+	uint32_t s;
+	s = (uint32_t)accu + (uint32_t)*sp++ - 1;
+        if( (uint32_t)s < (uint32_t)accu ) {
           /* carry */
 	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
 	}
@@ -1081,10 +1082,10 @@ value coq_interprete
       Instruct (ADDCARRYCINT31) {
 	print_instr("ADDCARRYCINT31");
 	/* returns the sum plus one with a carry */
-	uint32 s;
-	s = (uint32)accu + (uint32)*sp++ + 1;
+	uint32_t s;
+	s = (uint32_t)accu + (uint32_t)*sp++ + 1;
 	value block;
-        if( (uint32)s <= (uint32)accu ) {
+        if( (uint32_t)s <= (uint32_t)accu ) {
           /* carry */
 	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
 	}
@@ -1100,18 +1101,18 @@ value coq_interprete
 	print_instr("SUBINT31");
 	/* returns the subtraction */
 	accu = 
-	  (value)((uint32) accu - (uint32) *sp++ + 1); 
+	  (value)((uint32_t) accu - (uint32_t) *sp++ + 1); 
         Next;
       }
 
       Instruct (SUBCINT31) {
 	print_instr("SUBCINT31");
 	/* returns the subtraction with a carry */
-	uint32 b;
-	uint32 s;
-	b = (uint32)*sp++;
-	s = (uint32)accu - b + 1;
-        if( (uint32)accu < b ) {
+	uint32_t b;
+	uint32_t s;
+	b = (uint32_t)*sp++;
+	s = (uint32_t)accu - b + 1;
+        if( (uint32_t)accu < b ) {
           /* carry */
 	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
 	}
@@ -1126,11 +1127,11 @@ value coq_interprete
       Instruct (SUBCARRYCINT31) {
 	print_instr("SUBCARRYCINT31");
 	/* returns the subtraction minus one with a carry */
-	uint32 b;
-	uint32 s;
-	b = (uint32)*sp++;
-	s = (value)((uint32)accu - b - 1);
-        if( (uint32)accu <= b ) {
+	uint32_t b;
+	uint32_t s;
+	b = (uint32_t)*sp++;
+	s = (value)((uint32_t)accu - b - 1);
+        if( (uint32_t)accu <= b ) {
           /* carry */
 	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
 	}
@@ -1154,7 +1155,7 @@ value coq_interprete
         /*returns the multiplication on a double size word
           (special case for 0) */
         print_instr("MULCINT31");
-	uint64 p;
+	uint64_t p;
         /*accu = 2v+1, *sp=2w+1 ==> p = 2v*w */
         p = I64_mul (UI64_of_value (accu), UI64_of_uint32 ((*sp++)^1));
 	if ( I64_is_zero(p) ) {
@@ -1177,10 +1178,10 @@ value coq_interprete
 	/* spiwack: takes three int31 (the two first ones represent an
                     int62) and performs the euclidian division of the
                     int62 by the int31 */
-        uint64 bigint;
+        uint64_t bigint;
         bigint = UI64_of_value(accu);
         bigint = I64_or(I64_lsl(bigint, 31),UI64_of_value(*sp++));
-        uint64 divisor;
+        uint64_t divisor;
         divisor = UI64_of_value(*sp++);
         Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
         if (I64_is_zero (divisor)) {
@@ -1188,7 +1189,7 @@ value coq_interprete
           Field(accu, 1) = 1; /* 2*0+1 */
 	}
 	else {
-	  uint64 quo, mod;
+	  uint64_t quo, mod;
           I64_udivmod(bigint, divisor, &quo, &mod);
           Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
 	  Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
@@ -1201,7 +1202,7 @@ value coq_interprete
         /* spiwack: a priori no need of the NON_STANDARD_DIV_MOD flag
                     since it probably only concerns negative number.
                     needs to be checked at this point */
-        uint32 divisor;
+        uint32_t divisor;
         divisor = uint32_of_value(*sp++);
         if (divisor == 0) { 
           Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
@@ -1209,7 +1210,7 @@ value coq_interprete
           Field(accu, 1) = 1; /* 2*0+1 */
         }
         else {
-          uint32 modulus;
+          uint32_t modulus;
           modulus = uint32_of_value(accu);
           Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
 	  Field(accu, 0) = value_of_uint32(modulus/divisor);
@@ -1221,7 +1222,7 @@ value coq_interprete
       Instruct (ADDMULDIVINT31) {
         print_instr("ADDMULDIVINT31");
         /* higher level shift (does shifts and cycles and such) */
-        uint32 shiftby;
+        uint32_t shiftby;
         shiftby = uint32_of_value(accu);
         if (shiftby > 31) {
           if (shiftby < 62) {
@@ -1236,7 +1237,7 @@ value coq_interprete
         /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */
         accu = (value)(((*sp++)^1) << shiftby);
         /* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */
-        accu = (value)((accu | (((uint32)(*sp++)) >> (31-shiftby)))|1);
+        accu = (value)((accu | (((uint32_t)(*sp++)) >> (31-shiftby)))|1);
 	}
         Next;
       }
@@ -1245,11 +1246,11 @@ value coq_interprete
 	/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
 	/* assumes Inudctive _ : _ := Eq | Lt | Gt */
 	print_instr("COMPAREINT31");
-	if ((uint32)accu == (uint32)*sp) {
+	if ((uint32_t)accu == (uint32_t)*sp) {
 	  accu = 1;  /* 2*0+1 */
 	  sp++;
 	}
-	else{if ((uint32)accu < (uint32)(*sp++)) {
+	else{if ((uint32_t)accu < (uint32_t)(*sp++)) {
 	  accu = 3;  /* 2*1+1 */
 	}
 	else{
@@ -1260,9 +1261,9 @@ value coq_interprete
  
       Instruct (HEAD0INT31) {
 	int r = 0;
-        uint32 x;
+        uint32_t x;
         print_instr("HEAD0INT31");
-	x = (uint32) accu;
+	x = (uint32_t) accu;
         if (!(x & 0xFFFF0000)) { x <<= 16; r += 16; }
         if (!(x & 0xFF000000)) { x <<= 8;  r += 8; }
         if (!(x & 0xF0000000)) { x <<= 4;  r += 4; }
@@ -1275,9 +1276,9 @@ value coq_interprete
         
       Instruct (TAIL0INT31) {
 	int r = 0;
-        uint32 x;
+        uint32_t x;
         print_instr("TAIL0INT31");
-	x = (((uint32) accu >> 1) | 0x80000000);
+	x = (((uint32_t) accu >> 1) | 0x80000000);
         if (!(x & 0xFFFF)) { x >>= 16; r += 16; }
         if (!(x & 0x00FF)) { x >>= 8;  r += 8; }
         if (!(x & 0x000F)) { x >>= 4;  r += 4; }
@@ -1327,7 +1328,7 @@ value coq_interprete
         /*accu=accu or accu = (value)((unsigned long)1-accu) if bool
 	               is used for the bits */
         for(i=0; i < 30; i++) {
-	  accu = (value) ((((uint32)accu-1) << 1) | *sp++);
+	  accu = (value) ((((uint32_t)accu-1) << 1) | *sp++);
           /* -1 removes the tag bit, << 1 multiplies the value by 2, 
               | *sp++ pops the last value and add it (no carry involved)
 	      not that it reintroduces a tag bit */
@@ -1347,7 +1348,7 @@ value coq_interprete
         for(i = 30; i >= 0; i--) {
           Field(block, i) = (value)(accu & 3); /* two last bits of the accumulator */
           //Field(block, i) = 3;
-          accu = (value) ((uint32)accu >> 1) | 1;  /* last bit must be a one */
+          accu = (value) ((uint32_t)accu >> 1) | 1;  /* last bit must be a one */
         };
 	accu = block;
         Next;
diff --git a/kernel/byterun/int64_native.h b/kernel/byterun/int64_native.h
index 8a6a2664..657d0a07 100644
--- a/kernel/byterun/int64_native.h
+++ b/kernel/byterun/int64_native.h
@@ -18,9 +18,9 @@
 #ifndef CAML_INT64_NATIVE_H
 #define CAML_INT64_NATIVE_H
 
-#define I64_literal(hi,lo) ((int64)(hi) << 32 | (lo))
+#define I64_literal(hi,lo) ((int64_t)(hi) << 32 | (lo))
 #define I64_compare(x,y) (((x) > (y)) - ((x) < (y)))
-#define I64_ult(x,y) ((uint64)(x) < (uint64)(y))
+#define I64_ult(x,y) ((uint64_t)(x) < (uint64_t)(y))
 #define I64_neg(x) (-(x))
 #define I64_add(x,y) ((x) + (y))
 #define I64_sub(x,y) ((x) - (y))
@@ -30,19 +30,19 @@
 #define I64_div(x,y) ((x) / (y))
 #define I64_mod(x,y) ((x) % (y))
 #define I64_udivmod(x,y,quo,rem) \
-  (*(rem) = (uint64)(x) % (uint64)(y), \
-   *(quo) = (uint64)(x) / (uint64)(y))
+  (*(rem) = (uint64_t)(x) % (uint64_t)(y), \
+   *(quo) = (uint64_t)(x) / (uint64_t)(y))
 #define I64_and(x,y) ((x) & (y))
 #define I64_or(x,y) ((x) | (y))
 #define I64_xor(x,y) ((x) ^ (y))
 #define I64_lsl(x,y) ((x) << (y))
 #define I64_asr(x,y) ((x) >> (y))
-#define I64_lsr(x,y) ((uint64)(x) >> (y))
+#define I64_lsr(x,y) ((uint64_t)(x) >> (y))
 #define I64_to_intnat(x) ((intnat) (x))
 #define I64_of_intnat(x) ((intnat) (x))
-#define I64_to_int32(x) ((int32) (x))
-#define I64_of_int32(x) ((int64) (x))
+#define I64_to_int32(x) ((int32_t) (x))
+#define I64_of_int32(x) ((int64_t) (x))
 #define I64_to_double(x) ((double)(x))
-#define I64_of_double(x) ((int64)(x))
+#define I64_of_double(x) ((int64_t)(x))
 
 #endif /* CAML_INT64_NATIVE_H */
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index ae679027..700de502 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -24,6 +24,9 @@ let fix_tag = 3
 let switch_tag = 4
 let cofix_tag = 5
 let cofix_evaluated_tag = 6
+(* It could be greate if OCaml export this value,
+   So fixme if this occur in a new version of OCaml *)
+let last_variant_tag = 245 
 
 type structured_constant =
   | Const_sorts of sorts
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index b65268f7..fbb40ffd 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -20,6 +20,7 @@ val fix_tag : tag
 val switch_tag : tag
 val cofix_tag : tag
 val cofix_evaluated_tag : tag
+val last_variant_tag : tag 
 
 type structured_constant =
   | Const_sorts of sorts
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index d6c160c3..07fab06a 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -38,7 +38,7 @@ open Pre_env
 (* In the function body [arg1] is represented by de Bruijn [n], and       *)
 (* [argn] by de Bruijn [1]                                                *)
 
-(* Representation of environements of mutual fixpoints :                  *)
+(* Representation of environments of mutual fixpoints :                  *)
 (* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
 (*                ^<----------offset--------->                            *)
 (* type = [Ct1 | .... | Ctn]                                              *)
@@ -329,13 +329,50 @@ let init_fun_code () = fun_code := []
 
 (* Compilation of constructors and inductive types *)
 
+
+(* Limitation due to OCaml's representation of non-constant
+  constructors: limited to 245 + 1 (0 tag) cases. *)
+
+exception TooLargeInductive of Id.t
+
+let max_nb_const = 0x1000000 
+let max_nb_block = 0x1000000 + last_variant_tag - 1
+
+let str_max_constructors = 
+  Format.sprintf 
+    " which has more than %i constant constructors or more than %i non-constant constructors" max_nb_const max_nb_block
+
+let check_compilable ib = 
+  
+  if not (ib.mind_nb_args <= max_nb_block && ib.mind_nb_constant <= max_nb_const) then 
+    raise (TooLargeInductive ib.mind_typename)
+
+(* Inv: arity > 0 *)
+
+let const_bn tag args = 
+  if tag < last_variant_tag then Const_bn(tag, args)
+  else
+    Const_bn(last_variant_tag, Array.append [|Const_b0 (tag - last_variant_tag) |] args)
+
+  
+let code_makeblock arity tag cont = 
+  if tag < last_variant_tag then
+    Kmakeblock(arity, tag) :: cont
+  else
+    Kpush :: Kconst (Const_b0 (tag - last_variant_tag)) ::
+    Kmakeblock(arity+1, last_variant_tag) :: cont
+
 (* Inv : nparam + arity > 0 *)
 let code_construct tag nparams arity cont =
   let f_cont =
       add_pop nparams
       (if Int.equal arity 0 then
 	[Kconst (Const_b0 tag); Kreturn 0]
-       else [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0])
+       else if tag < last_variant_tag then
+         [Kacc 0; Kpop 1; Kmakeblock(arity, tag); Kreturn 0]
+       else 
+         [Kconst (Const_b0 (tag - last_variant_tag)); 
+          Kmakeblock(arity+1, last_variant_tag); Kreturn 0])
     in
     let lbl = Label.create() in
     fun_code := [Ksequence (add_grab (nparams+arity) lbl f_cont,!fun_code)];
@@ -345,7 +382,6 @@ let get_strcst = function
   | Bstrconst sc -> sc
   | _ -> raise Not_found
 
-
 let rec str_const c =
   match kind_of_term c with
   | Sort s -> Bstrconst (Const_sorts s)
@@ -357,7 +393,8 @@ let rec str_const c =
             begin
 	    let oib = lookup_mind kn !global_env in
 	    let oip = oib.mind_packets.(j) in
-	    let num,arity = oip.mind_reloc_tbl.(i-1) in
+	    let () = check_compilable oip in
+	    let tag,arity = oip.mind_reloc_tbl.(i-1) in
 	    let nparams = oib.mind_nparams in
 	    if Int.equal (nparams + arity) (Array.length args) then
               (* spiwack: *)
@@ -399,15 +436,15 @@ let rec str_const c =
               with Not_found ->
 		(* 3/ if no special behavior is available, then the compiler
 		      falls back to the normal behavior *)
-		if Int.equal arity 0 then Bstrconst(Const_b0 num)
+		if Int.equal arity 0 then Bstrconst(Const_b0 tag)
 		else
 		  let rargs = Array.sub args nparams arity in
 		  let b_args = Array.map str_const rargs in
 		  try
 		    let sc_args = Array.map get_strcst b_args in
-		    Bstrconst(Const_bn(num, sc_args))
+		    Bstrconst(const_bn tag sc_args)
 		  with Not_found ->
-		    Bmakeblock(num,b_args)
+		    Bmakeblock(tag,b_args)
 	    else
               let b_args = Array.map str_const args in
 	     (* spiwack: tries first to apply the run-time compilation
@@ -418,7 +455,7 @@ let rec str_const c =
                                            f),
                          b_args)
 	      with Not_found ->
-	        Bconstruct_app(num, nparams, arity, b_args)
+	        Bconstruct_app(tag, nparams, arity, b_args)
               end
 	| _ -> Bconstr c
       end
@@ -435,6 +472,7 @@ let rec str_const c =
       with Not_found ->
 	let oib = lookup_mind kn !global_env in
 	let oip = oib.mind_packets.(j) in
+	let () = check_compilable oip in
 	let num,arity = oip.mind_reloc_tbl.(i-1) in
 	let nparams = oib.mind_nparams in
 	if Int.equal (nparams + arity) 0 then Bstrconst(Const_b0 num)
@@ -489,9 +527,12 @@ let rec compile_fv reloc l sz cont =
 let rec get_allias env (kn,u as p) =
   let cb = lookup_constant kn env in
   let tps = cb.const_body_code in
-    (match Cemitcodes.force tps with
-    | BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
-    | _ -> p)
+    match tps with
+    | None -> p
+    | Some tps ->
+       (match Cemitcodes.force tps with
+	| BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
+	| _ -> p)
 
 (* Compiling expressions *)
 
@@ -607,9 +648,14 @@ let rec compile_constr reloc c sz cont =
       let ind = ci.ci_ind in
       let mib = lookup_mind (fst ind) !global_env in
       let oib = mib.mind_packets.(snd ind) in
+      let () = check_compilable oib in
       let tbl = oib.mind_reloc_tbl in
       let lbl_consts = Array.make oib.mind_nb_constant Label.no in
-      let lbl_blocks = Array.make (oib.mind_nb_args+1) Label.no in
+      let nallblock = oib.mind_nb_args + 1 in (* +1 : accumulate *)
+      let nblock = min nallblock (last_variant_tag + 1) in
+      let lbl_blocks = Array.make nblock Label.no in
+      let neblock = max 0 (nallblock - last_variant_tag) in
+      let lbl_eblocks = Array.make neblock Label.no in 
       let branch1,cont = make_branch cont in
       (* Compiling return type *)
       let lbl_typ,fcode =
@@ -629,6 +675,15 @@ let rec compile_constr reloc c sz cont =
       in
       lbl_blocks.(0) <- lbl_accu;
       let c = ref code_accu in
+      (* perform the extra match if needed (to many block constructors) *)
+      if neblock <> 0 then begin
+        let lbl_b, code_b = 
+          label_code (
+            Kpush :: Kfield 0 :: Kswitch(lbl_eblocks, [||]) :: !c) in
+        lbl_blocks.(last_variant_tag) <- lbl_b;
+        c := code_b
+      end;  
+      
       (* Compiling regular constructor branches *)
       for i = 0 to Array.length tbl - 1 do
 	let tag, arity = tbl.(i) in
@@ -640,22 +695,24 @@ let rec compile_constr reloc c sz cont =
 	else
 	  let args, body = decompose_lam branchs.(i) in
 	  let nargs = List.length args in
-	  let lbl_b,code_b =
-	    label_code(
-	    if Int.equal nargs arity then
-	      Kpushfields arity ::
+         
+          let code_b =  
+            if Int.equal nargs arity then
 	      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
-	      Kpushfields arity ::
 	      compile_constr reloc branchs.(i) (sz_b+arity)
-		(Kappterm(arity,sz_appterm) :: !c))
-	  in
-	  lbl_blocks.(tag) <- lbl_b;
+		(Kappterm(arity,sz_appterm) :: !c) in
+          let code_b = 
+            if tag < last_variant_tag then Kpushfields arity :: code_b
+            else Kacc 0::Kpop 1::Kpushfields(arity+1)::Kpop 1::code_b in
+          let lbl_b,code_b = label_code code_b in
+          if tag < last_variant_tag then lbl_blocks.(tag) <- lbl_b
+          else lbl_eblocks.(tag - last_variant_tag) <- lbl_b;
 	  c := code_b
       done;
-      c :=  Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
+      c := Klabel lbl_sw :: Kswitch(lbl_consts,lbl_blocks) :: !c;
       let code_sw =
  	match branch1 with
         (* spiwack : branch1 can't be a lbl anymore it's a Branch instead
@@ -677,9 +734,10 @@ and compile_str_cst reloc sc sz cont =
   | Bstrconst sc -> Kconst sc :: cont
   | Bmakeblock(tag,args) ->
       let nargs = Array.length args in
-      comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont)
+      comp_args compile_str_cst reloc args sz (code_makeblock nargs tag cont)
   | Bconstruct_app(tag,nparams,arity,args) ->
-      if Int.equal (Array.length args) 0 then code_construct tag nparams arity cont
+      if Int.equal (Array.length args) 0 then
+        code_construct tag nparams arity cont
       else
 	comp_app
 	  (fun _ _ _ cont -> code_construct tag nparams arity cont)
@@ -706,13 +764,14 @@ and compile_const =
                    Kgetglobal (get_allias !global_env (kn,u)) :: cont)
         compile_constr reloc () args sz cont
 
-let compile env c =
+let compile fail_on_error env c =
   set_global_env env;
   init_fun_code ();
   Label.reset_label_counter ();
   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
+  try 
+    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 = ";
@@ -722,21 +781,26 @@ let compile env c =
     | 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 = function
-  | Undef _ | OpaqueDef _ -> BCconstant
+      Some (init_code,!fun_code, Array.of_list fv)
+  with TooLargeInductive tname ->
+    let fn = if fail_on_error then Errors.errorlabstrm "compile" else Pp.msg_warning in
+      (Pp.(fn
+	   (str "Cannot compile code for virtual machine as it uses inductive " ++
+	    Id.print tname ++ str str_max_constructors));
+       None)
+
+let compile_constant_body fail_on_error env = function
+  | Undef _ | OpaqueDef _ -> Some BCconstant
   | Def sb ->
       let body = Mod_subst.force_constr sb in
       match kind_of_term body with
 	| Const (kn',u) ->
 	    (* we use the canonical name of the constant*)
 	    let con= constant_of_kn (canonical_con kn') in
-	      BCallias (get_allias env (con,u))
+	      Some (BCallias (get_allias env (con,u)))
 	| _ ->
-	    let res = compile env body in
-	    let to_patch = to_memory res in
-	    BCdefined to_patch
+	    let res = compile fail_on_error env body in
+	      Option.map (fun x -> BCdefined (to_memory x)) res
 
 (* Shortcut of the previous function used during module strengthening *)
 
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index eab36d8b..1128f0d0 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -1,4 +1,3 @@
-open Names
 open Cbytecodes
 open Cemitcodes
 open Term
@@ -6,10 +5,12 @@ open Declarations
 open Pre_env
 
 
-val compile : env -> constr -> bytecodes * bytecodes * fv
-                              (** init, fun, fv *)
+val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *)
+	      env -> constr -> (bytecodes * bytecodes * fv) option
+(** init, fun, fv *)
 
-val compile_constant_body : env -> constant_def -> body_code
+val compile_constant_body : bool -> 
+			    env -> constant_def -> body_code option
 
 (** Shortcut of the previous function used during module strengthening *)
 
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 3c9692a5..2535a64d 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -10,7 +10,6 @@
    machine, Oct 2004 *)
 (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
 
-open Names
 open Term
 open Cbytecodes
 open Copcodes
@@ -24,34 +23,22 @@ type reloc_info =
 
 type patch = reloc_info * int
 
+let patch_char4 buff pos c1 c2 c3 c4 = 
+  String.unsafe_set buff pos       c1;
+  String.unsafe_set buff (pos + 1) c2;
+  String.unsafe_set buff (pos + 2) c3;
+  String.unsafe_set buff (pos + 3) c4 
+  
 let patch_int buff pos n =
-  String.unsafe_set buff pos (Char.unsafe_chr n);
-  String.unsafe_set buff (pos + 1) (Char.unsafe_chr (n asr 8));
-  String.unsafe_set buff (pos + 2) (Char.unsafe_chr (n asr 16));
-  String.unsafe_set buff (pos + 3) (Char.unsafe_chr (n asr 24))
-
+  patch_char4 buff pos 
+    (Char.unsafe_chr n) (Char.unsafe_chr (n asr 8))  (Char.unsafe_chr (n asr 16))
+    (Char.unsafe_chr (n asr 24))
 
 (* Buffering of bytecode *)
 
 let out_buffer = ref(String.create 1024)
 and out_position = ref 0
 
-(*
-let out_word b1 b2 b3 b4 =
-  let p = !out_position in
-  if p >= String.length !out_buffer then begin
-    let len = String.length !out_buffer in
-    let new_buffer = String.create (2 * len) in
-    String.blit !out_buffer 0 new_buffer 0 len;
-    out_buffer := new_buffer
-  end;
-  String.unsafe_set !out_buffer p (Char.unsafe_chr b1);
-  String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2);
-  String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
-  String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
-  out_position := p + 4
-*)
-
 let out_word b1 b2 b3 b4 =
   let p = !out_position in
   if p >= String.length !out_buffer then begin
@@ -67,13 +54,10 @@ let out_word b1 b2 b3 b4 =
     String.blit !out_buffer 0 new_buffer 0 len;
     out_buffer := new_buffer
   end;
-  String.unsafe_set !out_buffer p (Char.unsafe_chr b1);
-  String.unsafe_set !out_buffer (p+1) (Char.unsafe_chr b2);
-  String.unsafe_set !out_buffer (p+2) (Char.unsafe_chr b3);
-  String.unsafe_set !out_buffer (p+3) (Char.unsafe_chr b4);
+  patch_char4 !out_buffer p (Char.unsafe_chr b1)
+   (Char.unsafe_chr b2) (Char.unsafe_chr b3) (Char.unsafe_chr b4);
   out_position := p + 4
 
-
 let out opcode =
   out_word opcode 0 0 0
 
@@ -102,7 +86,7 @@ let extend_label_table needed =
 
 let backpatch (pos, orig) =
   let displ = (!out_position - orig) asr 2 in
-  !out_buffer.[pos] <- Char.unsafe_chr displ;
+  !out_buffer.[pos]   <- Char.unsafe_chr displ;
   !out_buffer.[pos+1] <- Char.unsafe_chr (displ asr 8);
   !out_buffer.[pos+2] <- Char.unsafe_chr (displ asr 16);
   !out_buffer.[pos+3] <- Char.unsafe_chr (displ asr 24)
@@ -223,8 +207,12 @@ let emit_instr = function
       out_label typlbl; out_label swlbl;
       slot_for_annot annot;out_int sz
   | Kswitch (tbl_const, tbl_block) ->
+      let lenb = Array.length tbl_block in
+      let lenc = Array.length tbl_const in
+      assert (lenb < 0x100 && lenc < 0x1000000);
       out opSWITCH;
-      out_int (Array.length tbl_const + (Array.length tbl_block lsl 16));
+      out_word lenc (lenc asr 8) (lenc asr 16) (lenb);
+(*      out_int (Array.length tbl_const + (Array.length tbl_block lsl 23)); *)
       let org = !out_position in
       Array.iter (out_label_with_orig org) tbl_const;
       Array.iter (out_label_with_orig org) tbl_block
@@ -334,25 +322,41 @@ let subst_patch s (ri,pos) =
 let subst_to_patch s (code,pl,fv) =
   code,List.rev_map (subst_patch s) pl,fv
 
+let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
+
 type body_code =
   | BCdefined of to_patch
   | BCallias of pconstant
   | BCconstant
 
-let subst_body_code s = function
-  | BCdefined tp -> BCdefined (subst_to_patch s tp)
-  | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u)
-  | BCconstant -> BCconstant
-
-type to_patch_substituted = body_code substituted
-
-let from_val = from_val
-
-let force = force subst_body_code
-
-let subst_to_patch_subst = subst_substituted
-
-let repr_body_code = repr_substituted
+type to_patch_substituted =
+| PBCdefined of to_patch substituted
+| PBCallias of pconstant substituted
+| PBCconstant
+
+let from_val = function
+| BCdefined tp -> PBCdefined (from_val tp)
+| BCallias cu -> PBCallias (from_val cu)
+| BCconstant -> PBCconstant
+
+let force = function
+| PBCdefined tp -> BCdefined (force subst_to_patch tp)
+| PBCallias cu -> BCallias (force subst_pconstant cu)
+| PBCconstant -> BCconstant
+
+let subst_to_patch_subst s = function
+| PBCdefined tp -> PBCdefined (subst_substituted s tp)
+| PBCallias cu -> PBCallias (subst_substituted s cu)
+| PBCconstant -> PBCconstant
+
+let repr_body_code = function
+| PBCdefined tp ->
+  let (s, tp) = repr_substituted tp in
+  (s, BCdefined tp)
+| PBCallias cu ->
+  let (s, cu) = repr_substituted cu in
+  (s, BCallias cu)
+| PBCconstant -> (None, BCconstant)
 
 let to_memory (init_code, fun_code, fv) =
   init();
diff --git a/kernel/closure.ml b/kernel/closure.ml
index f06b13d8..ea9b2755 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -771,24 +771,6 @@ let drop_parameters depth n argstk =
   (* we know that n < stack_args_size(argstk) (if well-typed term) *) 
   anomaly (Pp.str "ill-typed term: found a match on a partially applied constructor")
 
-
-let rec get_parameters depth n argstk =
-  match argstk with
-      Zapp args::s ->
-        let q = Array.length args in
-        if n > q then Array.append args (get_parameters depth (n-q) s)
-        else if Int.equal n q then [||]
-        else Array.sub args 0 n
-    | Zshift(k)::s -> 
-      get_parameters (depth-k) n s
-    | [] -> (* we know that n < stack_args_size(argstk) (if well-typed term) *)
-	if Int.equal n 0 then [||]
-	else raise Not_found (* Trying to eta-expand a partial application..., should do 
-				eta expansion first? *)
-    | _ -> assert false
-	(* strip_update_shift_app only produces Zapp and Zshift items *)
-
-
 (** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
     to the conversion of the eta expansion of t, considered as an inhabitant 
     of ind, and the Constructor c of this inductive type applied to arguments
@@ -942,7 +924,7 @@ let rec knr info m stk =
         | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
       (match strip_update_shift_app m stk with
-          (_, args, (((Zcase _|ZcaseT _)::_) as stk')) ->
+          (_, args, (((Zcase _|ZcaseT _|Zproj _)::_) as stk')) ->
             let (fxe,fxbd) = contract_fix_vect m.term in
             knit info fxe fxbd (args@stk')
         | (_,args,s) -> (m,args@s))
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 49f74841..e823c01b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -464,55 +464,22 @@ let map_with_binders g f l c0 = match kind c0 with
     let bl' = CArray.Fun1.smartmap f l' bl in
     mkCoFix (ln,(lna,tl',bl'))
 
-(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
-   the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
-   instances and [s] to compare sorts; Cast's,
+(* [compare_head_gen_evar k1 k2 u s e eq leq c1 c2] compare [c1] and
+   [c2] (using [k1] to expose the structure of [c1] and [k2] to expose
+   the structure [c2]) using [eq] to compare the immediate subterms of
+   [c1] of [c2] for conversion if needed, [leq] for cumulativity, [u]
+   to compare universe instances, and [s] to compare sorts; Cast's,
    application associativity, binders name and Cases annotations are
-   not taken into account *)
+   not taken into account. Note that as [kind1] and [kind2] are
+   potentially different, we cannot use, in recursive case, the
+   optimisation that physically equal arrays are equals (hence the
+   calls to {!Array.equal_norefl}). *)
 
-let compare_head_gen eq_universes eq_sorts f t1 t2 =
-  match kind t1, kind t2 with
+let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
+  match kind1 t1, kind2 t2 with
   | Rel n1, Rel n2 -> Int.equal n1 n2
   | Meta m1, Meta m2 -> Int.equal m1 m2
   | Var id1, Var id2 -> Id.equal id1 id2
-  | Sort s1, Sort s2 -> eq_sorts s1 s2
-  | Cast (c1,_,_), _ -> f c1 t2
-  | _, Cast (c2,_,_) -> f t1 c2
-  | Prod (_,t1,c1), Prod (_,t2,c2) -> f t1 t2 && f c1 c2
-  | Lambda (_,t1,c1), Lambda (_,t2,c2) -> f t1 t2 && f c1 c2
-  | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> f b1 b2 && f t1 t2 && f c1 c2
-  | App (Cast(c1, _, _),l1), _ -> f (mkApp (c1,l1)) t2
-  | _, App (Cast (c2, _, _),l2) -> f t1 (mkApp (c2,l2))
-  | App (c1,l1), App (c2,l2) ->
-    Int.equal (Array.length l1) (Array.length l2) &&
-      f c1 c2 && Array.equal f l1 l2
-  | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal f l1 l2
-  | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && f c1 c2
-  | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
-  | Ind (c1,u1), Ind (c2,u2) -> eq_ind c1 c2 && eq_universes false u1 u2
-  | Construct (c1,u1), Construct (c2,u2) -> eq_constructor c1 c2 && eq_universes false u1 u2
-  | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-      f p1 p2 && f c1 c2 && Array.equal f bl1 bl2
-  | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
-      Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
-      && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      Int.equal ln1 ln2 && Array.equal f tl1 tl2 && Array.equal f bl1 bl2
-  | _ -> false
-
-let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
-
-(* [compare_head_gen_leq u s sl eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
-   the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
-   [u] to compare universe instances and [s] to compare sorts; Cast's,
-   application associativity, binders name and Cases annotations are
-   not taken into account *)
-
-let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
-  match kind t1, kind t2 with
-  | Rel n1, Rel n2 -> Int.equal n1 n2
-  | Meta m1, Meta m2 -> Int.equal m1 m2
-  | Var id1, Var id2 -> Int.equal (id_ord id1 id2) 0
   | Sort s1, Sort s2 -> leq_sorts s1 s2
   | Cast (c1,_,_), _ -> leq c1 t2
   | _, Cast (c2,_,_) -> leq t1 c2
@@ -522,8 +489,8 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
   | App (Cast(c1, _, _),l1), _ -> leq (mkApp (c1,l1)) t2
   | _, App (Cast (c2, _, _),l2) -> leq t1 (mkApp (c2,l2))
   | App (c1,l1), App (c2,l2) ->
-    Int.equal (Array.length l1) (Array.length l2) &&
-      eq c1 c2 && Array.equal eq l1 l2
+      Int.equal (Array.length l1) (Array.length l2) &&
+        eq c1 c2 && Array.equal_norefl eq l1 l2
   | Proj (p1,c1), Proj (p2,c2) -> Projection.equal p1 p2 && eq c1 c2
   | Evar (e1,l1), Evar (e2,l2) -> Evar.equal e1 e2 && Array.equal eq l1 l2
   | Const (c1,u1), Const (c2,u2) -> eq_constant c1 c2 && eq_universes true u1 u2
@@ -533,11 +500,31 @@ let compare_head_gen_leq eq_universes eq_sorts leq_sorts eq leq t1 t2 =
       eq p1 p2 && eq c1 c2 && Array.equal eq bl1 bl2
   | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
       Int.equal i1 i2 && Array.equal Int.equal ln1 ln2
-      && Array.equal eq tl1 tl2 && Array.equal eq bl1 bl2
+      && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
   | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      Int.equal ln1 ln2 && Array.equal eq tl1 tl2 && Array.equal eq bl1 bl2
+      Int.equal ln1 ln2 && Array.equal_norefl eq tl1 tl2 && Array.equal_norefl eq bl1 bl2
   | _ -> false
 
+(* [compare_head_gen_leq u s eq leq c1 c2] compare [c1] and [c2] using [eq] to compare
+   the immediate subterms of [c1] of [c2] for conversion if needed, [leq] for cumulativity,
+   [u] to compare universe instances and [s] to compare sorts; Cast's,
+   application associativity, binders name and Cases annotations are
+   not taken into account *)
+
+let compare_head_gen_leq eq_universes leq_sorts eq leq t1 t2 =
+  compare_head_gen_with kind kind  eq_universes leq_sorts eq leq t1 t2
+
+(* [compare_head_gen u s f c1 c2] compare [c1] and [c2] using [f] to compare
+   the immediate subterms of [c1] of [c2] if needed, [u] to compare universe
+   instances and [s] to compare sorts; Cast's,
+   application associativity, binders name and Cases annotations are
+   not taken into account *)
+
+let compare_head_gen eq_universes eq_sorts eq t1 t2 =
+  compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2
+
+let compare_head = compare_head_gen (fun _ -> Univ.Instance.equal) Sorts.equal
+
 (*******************************)
 (*  alpha conversion functions *)
 (*******************************)
@@ -549,6 +536,14 @@ let rec eq_constr m n =
 
 let equal m n = eq_constr m n (* to avoid tracing a recursive fun *)
 
+let rec equal_with kind1 kind2 m n =
+  (* note that pointer equality is not sufficient to ensure equality
+     up to [eq_evars], because we may evaluates evars of [m] and [n]
+     in different evar contexts. *)
+  let req_constr m n = equal_with kind1 kind2 m n in
+  compare_head_gen_with kind1 kind2
+    (fun _ -> Instance.equal) Sorts.equal req_constr req_constr m n
+
 let eq_constr_univs univs m n =
   if m == n then true
   else 
@@ -570,7 +565,7 @@ let leq_constr_univs univs m n =
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n
+      compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
       compare_leq m n
 
@@ -620,7 +615,7 @@ let leq_constr_univs_infer univs m n =
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let rec compare_leq m n =
-      compare_head_gen_leq eq_universes eq_sorts leq_sorts eq_constr' leq_constr' m n
+      compare_head_gen_leq eq_universes leq_sorts eq_constr' leq_constr' m n
     and leq_constr' m n = m == n || compare_leq m n in
     let res = compare_leq m n in
       res, !cstrs
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 5d11511b..67d1aded 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -203,6 +203,14 @@ val kind : constr -> (constr, types) kind_of_term
    and application grouping *)
 val equal : constr -> constr -> bool
 
+(** [equal_with_evars k1 k2 a b] is true when [a] equals [b] modulo
+    alpha, casts, application grouping, and using [k1] to expose the
+    head of [a] and [k2] to expose the head of [b]. *)
+val equal_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  constr -> constr -> bool
+
 (** [eq_constr_univs u a b] is [true] if [a] equals [b] modulo alpha, casts,
    application grouping and the universe equalities in [u]. *)
 val eq_constr_univs : constr Univ.check_function
@@ -285,16 +293,15 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   (constr -> constr -> bool) ->
   constr -> constr -> bool
 
-(** [compare_head_gen_leq u s sle f fle c1 c2] compare [c1] and [c2]
-    using [f] to compare the immediate subterms of [c1] of [c2] for
+(** [compare_head_gen_leq u s f fle c1 c2] compare [c1] and [c2] using
+    [f] to compare the immediate subterms of [c1] of [c2] for
     conversion, [fle] for cumulativity, [u] to compare universe
     instances (the first boolean tells if they belong to a constant),
-    [s] to compare sorts for equality and [sle] for subtyping; Cast's,
-    binders name and Cases annotations are not taken into account *)
+    [s] to compare sorts for for subtyping; Cast's, binders name and
+    Cases annotations are not taken into account *)
 
 val compare_head_gen_leq : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   (Sorts.t -> Sorts.t -> bool) ->
-  (Sorts.t -> Sorts.t -> bool) ->
   (constr -> constr -> bool) ->
   (constr -> constr -> bool) ->
   constr -> constr -> bool
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index ed8b0a6d..b29f06c6 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -148,14 +148,17 @@ let rec slot_for_getglobal env (kn,u) =
   with NotEvaluated ->
 (*    Pp.msgnl(str"not yet evaluated");*)
     let pos =
-      match Cemitcodes.force cb.const_body_code with
-      | BCdefined(code,pl,fv) ->
-	if Univ.Instance.is_empty u then
-	  let v = eval_to_patch env (code,pl,fv) in
-	    set_global v
-	else set_global (val_of_constant (kn,u))
-    | BCallias kn' -> slot_for_getglobal env kn'
-    | BCconstant -> set_global (val_of_constant (kn,u)) in
+      match cb.const_body_code with
+      | None -> set_global (val_of_constant (kn,u))
+      | Some code ->
+	 match Cemitcodes.force code with
+	 | BCdefined(code,pl,fv) ->
+	    if Univ.Instance.is_empty u then
+	    let v = eval_to_patch env (code,pl,fv) in
+	      set_global v
+	    else set_global (val_of_constant (kn,u))
+	 | BCallias kn' -> slot_for_getglobal env kn'
+	 | BCconstant -> set_global (val_of_constant (kn,u)) in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
     rk := Some (Ephemeron.create pos);
     pos
@@ -210,7 +213,9 @@ and eval_to_patch env (buff,pl,fv) =
 
 and val_of_constr env c =
   let (_,fun_code,_ as ccfv) =
-    try compile env c
+    try match compile true env c with
+	| Some v -> v
+	| None -> assert false
     with reraise ->
       let reraise = Errors.push reraise in
       let () = print_string "can not compile \n" in
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index bec52122..27c1c3f3 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -70,7 +70,7 @@ type constant_body = {
     const_hyps : Context.section_context; (** New: younger hyp at top *)
     const_body : constant_def;
     const_type : constant_type;
-    const_body_code : Cemitcodes.to_patch_substituted;
+    const_body_code : Cemitcodes.to_patch_substituted option;
     const_polymorphic : bool; (** Is it polymorphic or not *)
     const_universes : constant_universes;
     const_proj : projection_body option;
@@ -139,7 +139,7 @@ type one_inductive_body = {
 
     mind_kelim : sorts_family list; (** List of allowed elimination sorts *)
 
-    mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *)
+    mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
 
     mind_consnrealargs : int array;
  (** Number of expected proper arguments of the constructors (w/o params)
@@ -172,7 +172,7 @@ type mutual_inductive_body = {
 
     mind_hyps : Context.section_context;  (** Section hypotheses on which the block depends *)
 
-    mind_nparams : int;  (** Number of expected parameters *)
+    mind_nparams : int;  (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *)
 
     mind_nparams_rec : int;  (** Number of recursively uniform (i.e. ordinary) parameters *)
 
@@ -202,7 +202,7 @@ type ('ty,'a) functorize =
 
 type with_declaration =
   | WithMod of Id.t list * module_path
-  | WithDef of Id.t list * constr
+  | WithDef of Id.t list * constr Univ.in_universe_context
 
 type module_alg_expr =
   | MEident of module_path
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 48a6098e..a7051d5c 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -129,7 +129,7 @@ let subst_const_body sub cb =
         const_type = type';
         const_proj = proj';
         const_body_code =
-          Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
+          Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
         const_polymorphic = cb.const_polymorphic;
         const_universes = cb.const_universes;
         const_inline_code = cb.const_inline_code }
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 47a82cc6..ce65af97 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -9,7 +9,6 @@
 open Declarations
 open Mod_subst
 open Univ
-open Context
 
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 0ebff440..a79abbb7 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -473,7 +473,7 @@ type unsafe_type_judgment = {
 
 (*s Compilation of global declaration *)
 
-let compile_constant_body = Cbytegen.compile_constant_body
+let compile_constant_body = Cbytegen.compile_constant_body false
 
 exception Hyp_not_found
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index de960ecc..ede356e6 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -253,7 +253,7 @@ type unsafe_type_judgment = {
 
 (** {6 Compilation of global declaration } *)
 
-val compile_constant_body : env -> constant_def -> Cemitcodes.body_code
+val compile_constant_body : env -> constant_def -> Cemitcodes.body_code option
 
 exception Hyp_not_found
 
diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli
index 4c2c92cc..90d9c55f 100644
--- a/kernel/fast_typeops.mli
+++ b/kernel/fast_typeops.mli
@@ -6,13 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
-open Univ
 open Term
-open Context
 open Environ
-open Entries
-open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
     
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 99d9f52c..6b909824 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -164,10 +164,12 @@ let infer_constructor_packet env_ar_par ctx params lc =
 (* If indices matter *)
 let cumulate_arity_large_levels env sign =
   fst (List.fold_right
-    (fun (_,_,t as d) (lev,env) ->
-      let tj = infer_type env t in
-      let u = univ_of_sort tj.utj_type in
-	(Universe.sup u lev, push_rel d env))
+    (fun (_,b,t as d) (lev,env) ->
+      if Option.is_empty b then
+	let tj = infer_type env t in
+	let u = univ_of_sort tj.utj_type in
+	  (Universe.sup u lev, push_rel d env)
+      else lev, push_rel d env)
     sign (Universe.type0m,env))
 
 let is_impredicative env u =
@@ -344,7 +346,7 @@ let typecheck_inductive env mie =
       in
 	(id,cn,lc,(sign,arity)))
     inds
-  in (env_arities, params, inds)
+  in (env_arities, env_ar_par, params, inds)
 
 (************************************************************************)
 (************************************************************************)
@@ -364,9 +366,8 @@ exception IllFormedInd of ill_formed_ind
 
 let mind_extract_params = decompose_prod_n_assum
 
-let explain_ind_err id ntyp env0 nbpar c nargs err =
+let explain_ind_err id ntyp env nbpar c nargs err =
   let (lpar,c') = mind_extract_params nbpar c in
-  let env = push_rel_context lpar env0 in
   match err with
     | LocalNonPos kt ->
 	raise (InductiveError (NonPos (env,c',mkRel (kt+nbpar))))
@@ -484,6 +485,7 @@ let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcname
 	          check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d)
 	| Rel k ->
             (try let (ra,rarg) = List.nth ra_env (k-1) in
+            let largs = List.map (whd_betadeltaiota env) largs in
 	    let nmr1 =
 	      (match ra with
                   Mrec _ -> compute_rec_par ienv hyps nmr largs
@@ -654,7 +656,6 @@ let used_section_variables env inds =
   keep_hyps env ids
 
 let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
-let rel_appvect n m = rel_vect n (List.length m)
 
 exception UndefinableExpansion
 
@@ -821,9 +822,9 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 
 let check_inductive env kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar, params, inds) = typecheck_inductive env mie in
+  let (env_ar, env_ar_par, params, inds) = typecheck_inductive env mie in
   (* Then check positivity conditions *)
-  let (nmr,recargs) = check_positivity kn env_ar params inds in
+  let (nmr,recargs) = check_positivity kn env_ar_par params inds in
   (* Build the inductive packets *)
     build_inductive env mie.mind_entry_polymorphic mie.mind_entry_private
       mie.mind_entry_universes
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index bb57ad25..ca814f49 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -364,7 +364,7 @@ let build_branches_type (ind,u) (_,mip as specif) params p =
       let cstr = ith_constructor_of_inductive ind (i+1) in
       let dep_cstr = applist (mkConstructU (cstr,u),lparams@(local_rels args)) in
       vargs @ [dep_cstr] in
-    let base = beta_appvect (lift nargs p) (Array.of_list cargs) in
+    let base = betazeta_appvect mip.mind_nrealdecls (lift nargs p) (Array.of_list cargs) in
     it_mkProd_or_LetIn base args in
   Array.mapi build_one_branch mip.mind_nf_lc
 
@@ -447,13 +447,6 @@ type subterm_spec =
 
 let eq_wf_paths = Rtree.equal Declareops.eq_recarg
 
-let pp_recarg = function
-  | Norec -> Pp.str "Norec"
-  | Mrec i -> Pp.str ("Mrec "^MutInd.to_string (fst i))
-  | Imbr i -> Pp.str ("Imbr "^MutInd.to_string (fst i))
-
-let pp_wf_paths = Rtree.pp_tree pp_recarg
-
 let inter_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> Some r1
 | Mrec i1, Mrec i2
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 97c1d1fd..26dd45f5 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -54,7 +54,7 @@ let rec rebuild_mp mp l =
 
 let (+++) = Univ.Constraint.union
 
-let rec check_with_def env struc (idl,c) mp equiv =
+let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
   let lab,idl = match idl with
     | [] -> assert false
     | id::idl -> Label.of_id id, idl
@@ -74,30 +74,33 @@ let rec check_with_def env struc (idl,c) mp equiv =
 	 as long as they have the right type *)
       let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
       let env' = Environ.add_constraints ccst env' in
+      let newus, cst = Univ.UContext.dest ctx in
+      let env' = Environ.add_constraints cst env' in
       let c',cst = match cb.const_body with
 	| Undef _ | OpaqueDef _ ->
 	  let j = Typeops.infer env' c in
 	  let typ = Typeops.type_of_constant_type env' cb.const_type in
-	  let cst = Reduction.infer_conv_leq env' (Environ.universes env')
+	  let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
 	    j.uj_type typ in
-	  j.uj_val,cst
+	  j.uj_val,cst' +++ cst
 	| Def cs ->
-	  let cst = Reduction.infer_conv env' (Environ.universes env') c
+	  let cst' = Reduction.infer_conv env' (Environ.universes env') c
 	    (Mod_subst.force_constr cs) in
 	  let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
-	    if cb.const_polymorphic then cst
-	    else ccst +++ cst 
+	    if cb.const_polymorphic then cst' +++ cst
+	    else cst' +++ cst
 	  in
             c, cst
       in
       let def = Def (Mod_subst.from_val c') in
+      let ctx' = Univ.UContext.make (newus, cst) in
       let cb' =
 	{ cb with
 	  const_body = def;
-	  const_body_code = Cemitcodes.from_val (compile_constant_body env' def) }
-	  (* const_universes = Future.from_val cst } *)
+	  const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def);
+	  const_universes = ctx' }
       in
-      before@(lab,SFBconst(cb'))::after, c', cst
+      before@(lab,SFBconst(cb'))::after, c', ctx'
     else
       (* Definition inside a sub-module *)
       let mb = match spec with
@@ -108,7 +111,7 @@ let rec check_with_def env struc (idl,c) mp equiv =
       | Abstract ->
         let struc = Modops.destr_nofunctor mb.mod_type in
         let struc',c',cst =
-          check_with_def env' struc (idl,c) (MPdot(mp,lab)) mb.mod_delta
+          check_with_def env' struc (idl,(c,ctx)) (MPdot(mp,lab)) mb.mod_delta
         in
         let mb' = { mb with
           mod_type = NoFunctor struc';
@@ -204,8 +207,8 @@ let check_with env mp (sign,alg,reso,cst) = function
   |WithDef(idl,c) ->
     let struc = destr_nofunctor sign in
     let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
-    let alg' = mk_alg_with alg (WithDef (idl,c')) in
-    (NoFunctor struc'),alg',reso, cst+++cst'
+    let alg' = mk_alg_with alg (WithDef (idl,(c',cst'))) in
+    (NoFunctor struc'),alg',reso, cst+++(Univ.UContext.constraints cst')
   |WithMod(idl,mp1) as wd ->
     let struc = destr_nofunctor sign in
     let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 392e667b..d52fe611 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -177,9 +177,9 @@ let subst_with_body sub = function
   |WithMod(id,mp) as orig ->
     let mp' = subst_mp sub mp in
     if mp==mp' then orig else WithMod(id,mp')
-  |WithDef(id,c) as orig ->
+  |WithDef(id,(c,ctx)) as orig ->
     let c' = subst_mps sub c in
-    if c==c' then orig else WithDef(id,c')
+    if c==c' then orig else WithDef(id,(c',ctx))
 
 let rec subst_structure sub do_delta sign =
   let subst_body ((l,body) as orig) = match body with
@@ -337,7 +337,7 @@ let strengthen_const mp_from l cb resolver =
     in
       { cb with
 	const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
-	const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias (con,u)) }
+	const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias (con,u))) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if mp_in_delta mb.mod_mp mb.mod_delta then mb
@@ -428,16 +428,20 @@ let rec strengthen_and_subst_mod mb subst mp_from mp_to =
 and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
   match str with
     | [] -> empty_delta_resolver,[]
-    | (l,SFBconst cb) :: rest ->
+    | (l,SFBconst cb) as item :: rest ->
         let cb' = subst_const_body subst cb in
-        let cb'' =
+        let cb' =
           if alias then cb'
           else strengthen_const mp_from l cb' reso
         in
-        let item' = l, SFBconst cb'' in
+        let item' = if cb' == cb then item else (l, SFBconst cb') in
 	let reso',rest' =
 	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
+        let str' =
+          if rest' == rest && item' == item then str
+          else item' :: rest'
+        in
 	if incl then
           (* If we are performing an inclusion we need to add
              the fact that the constant mp_to.l is \Delta-equivalent
@@ -445,26 +449,31 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
           let kn_from = KerName.make2 mp_from l in
           let kn_to = KerName.make2 mp_to l in
           let old_name = kn_of_delta reso kn_from in
-	  add_kn_delta_resolver kn_to old_name reso', item'::rest'
+	  add_kn_delta_resolver kn_to old_name reso', str'
 	else
 	  (* In this case the fact that the constant mp_to.l is
 	     \Delta-equivalent to resolver(mp_from.l) is already known
 	     because reso' contains mp_to maps to reso(mp_from) *)
-	  reso', item'::rest'
-    | (l,SFBmind mib) :: rest ->
-	let item' = l,SFBmind (subst_mind_body subst mib) in
+	  reso', str'
+    | (l,SFBmind mib) as item :: rest ->
+        let mib' = subst_mind_body subst mib in
+        let item' = if mib' == mib then item else (l, SFBmind mib') in
 	let reso',rest' =
 	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
+        let str' =
+          if rest' == rest && item' == item then str
+          else item' :: rest'
+        in
 	(* Same as constant *)
 	if incl then
 	  let kn_from = KerName.make2 mp_from l in
 	  let kn_to = KerName.make2 mp_to l in
 	  let old_name = kn_of_delta reso kn_from in
-	  add_kn_delta_resolver kn_to old_name reso', item'::rest'
+          add_kn_delta_resolver kn_to old_name reso', str'
 	else
-	  reso', item'::rest'
-    | (l,SFBmodule mb) :: rest ->
+          reso', str'
+    | (l,SFBmodule mb) as item :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
 	let mp_to' = MPdot (mp_to,l) in
 	let mb' = if alias then
@@ -472,31 +481,39 @@ and strengthen_and_subst_struct str subst mp_from mp_to alias incl reso =
 	else
 	  strengthen_and_subst_mod mb subst mp_from' mp_to'
 	in
-	let item' = l,SFBmodule mb' in
+        let item' = if mb' == mb then item else (l, SFBmodule mb') in
 	let reso',rest' =
 	  strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
+        let str' =
+          if rest' == rest && item' == item then str
+          else item' :: rest'
+        in
         (* if mb is a functor we should not derive new equivalences
            on names, hence we add the fact that the functor can only
            be equivalent to itself. If we adopt an applicative
            semantic for functor this should be changed.*)
 	if is_functor mb'.mod_type then
-	  add_mp_delta_resolver mp_to' mp_to' reso', item':: rest'
+          add_mp_delta_resolver mp_to' mp_to' reso', str'
 	else
-	  add_delta_resolver reso' mb'.mod_delta, item':: rest'
-    | (l,SFBmodtype mty) :: rest ->
+          add_delta_resolver reso' mb'.mod_delta, str'
+    | (l,SFBmodtype mty) as item :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
 	let mp_to' = MPdot(mp_to,l) in
 	let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in
-	let mty = subst_modtype subst'
+	let mty' = subst_modtype subst'
 	  (fun resolver _ -> subst_dom_codom_delta_resolver subst' resolver)
           mty
         in
-        let item' = l,SFBmodtype mty in
+        let item' = if mty' == mty then item else (l, SFBmodtype mty') in
 	let reso',rest' =
           strengthen_and_subst_struct rest subst mp_from mp_to alias incl reso
         in
-	add_mp_delta_resolver mp_to' mp_to' reso', item'::rest'
+        let str' =
+          if rest' == rest && item' == item then str
+          else item' :: rest'
+        in
+	add_mp_delta_resolver mp_to' mp_to' reso', str'
 
 
 (** Let P be a module path when we write:
diff --git a/kernel/names.ml b/kernel/names.ml
index b349ccb0..480b37e8 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -33,9 +33,9 @@ struct
 
   let hash = String.hash
 
-  let check_soft x =
+  let check_soft ?(warn = true) x =
     let iter (fatal, x) =
-      if fatal then Errors.error x else Pp.msg_warning (str x)
+      if fatal then Errors.error x else if warn then Pp.msg_warning (str x)
     in
     Option.iter iter (Unicode.ident_refutation x)
 
@@ -48,6 +48,11 @@ struct
     let s = String.copy s in
     String.hcons s
 
+  let of_string_soft s =
+    let () = check_soft ~warn:false s in
+    let s = String.copy s in
+    String.hcons s
+
   let to_string id = String.copy id
 
   let print id = str id
@@ -571,7 +576,6 @@ let constr_modpath (ind,_) = ind_modpath ind
 
 let ith_mutual_inductive (mind, _) i = (mind, i)
 let ith_constructor_of_inductive ind i = (ind, i)
-let ith_constructor_of_pinductive (ind,u) i = ((ind,i),u)
 let inductive_of_constructor (ind, i) = ind
 let index_of_constructor (ind, i) = i
 
diff --git a/kernel/names.mli b/kernel/names.mli
index d82043da..92ee58f2 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -29,7 +29,11 @@ sig
 
   val of_string : string -> t
   (** Converts a string into an identifier. May raise [UserError _] if the
-      string is not valid. *)
+      string is not valid, or echo a warning if it contains invalid identifier
+      characters. *)
+
+  val of_string_soft : string -> t
+  (** Same as {!of_string} except that no warning is ever issued. *)
 
   val to_string : t -> string
   (** Converts a identifier into an string. *)
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 1a4a4b54..ada7ae73 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -12,7 +12,6 @@ open Context
 open Declarations
 open Util
 open Nativevalues
-open Primitives
 open Nativeinstr
 open Nativelambda
 open Pre_env
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 543397df..383f8102 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -375,9 +375,12 @@ let makeblock env cn u tag args =
 
 let rec get_allias env (kn, u as p) =
   let tps = (lookup_constant kn env).const_body_code in
-  match Cemitcodes.force tps with
-  |  Cemitcodes.BCallias kn' -> get_allias env kn'
-  | _ -> p
+    match tps with
+    | None -> p
+    | Some tps ->
+       match Cemitcodes.force tps with
+       | Cemitcodes.BCallias kn' -> get_allias env kn'
+       | _ -> p
 
 (*i Global environment *)
 
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 6a97edc4..ccf2888b 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -8,7 +8,6 @@
 open Names
 open Term
 open Pre_env
-open Nativevalues
 open Nativeinstr
 
 (** This file defines the lambda code generation phase of the native compiler *)
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index dd47bc06..605c1225 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -77,7 +77,10 @@ let call_compiler ml_filename =
     ::include_dirs
     @ ["-impl"; ml_filename] in
   if !Flags.debug then Pp.msg_debug (Pp.str (compiler_name ^ " " ^ (String.concat " " args)));
-  CUnix.sys_command compiler_name args = Unix.WEXITED 0, link_filename
+  try CUnix.sys_command compiler_name args = Unix.WEXITED 0, link_filename
+  with Unix.Unix_error (e,_,_) ->
+    Pp.(msg_warning (str (Unix.error_message e)));
+    false, link_filename
 
 let compile fn code =
   write_ml_code fn code;
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 914f577e..0b8662ff 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -12,7 +12,6 @@ open Environ
 open Mod_subst
 open Modops
 open Nativecode
-open Nativelib
 
 (** This file implements separate compilation for libraries in the native
 compiler *)
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index d7a21950..e4a77999 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -370,6 +370,11 @@ type coq_pair =
   | Paccu of t
   | PPair of t * t
 
+type coq_zn2z =
+  | Zaccu of t
+  | ZW0
+  | ZWW of t * t
+
 let mkCarry b i =
   if b then (Obj.magic (C1(of_uint i)):t)
   else (Obj.magic (C0(of_uint i)):t)
@@ -413,8 +418,13 @@ let subcarryc accu x y =
 let of_pair (x, y) =
   (Obj.magic (PPair(of_uint x, of_uint y)):t)
 
+let zn2z_of_pair (x,y) =
+  if Uint31.equal x (Uint31.of_uint 0) &&
+    Uint31.equal y (Uint31.of_uint 0) then Obj.magic ZW0
+  else (Obj.magic (ZWW(of_uint x, of_uint y)) : t)
+
 let no_check_mulc x y =
-    of_pair(Uint31.mulc (to_uint x) (to_uint y))
+  zn2z_of_pair(Uint31.mulc (to_uint x) (to_uint y))
 
 let mulc accu x y =
   if is_int x && is_int y then no_check_mulc x y
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 87cebd62..0609c851 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -9,7 +9,6 @@
 open Names
 open Term
 open Mod_subst
-open Int
 
 (** This module implements the handling of opaque proof terms.
     Opauqe proof terms are special since:
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4153b323..b09367dd 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -28,14 +28,6 @@ open Esubst
 
 let left2right = ref false
 
-let conv_key k =
-  match k with
-    VarKey id -> 
-    VarKey id
-  | ConstKey (cst,_) -> 
-     ConstKey cst
-  | RelKey n -> RelKey n
-		       
 let rec is_empty_stack = function
   [] -> true
   | Zupdate _::s -> is_empty_stack s
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 20cecc84..d762a246 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -379,7 +379,9 @@ let globalize_constant_universes env cb =
 	  | None -> []
 	  | Some fc ->
             match Future.peek_val fc with
-            | None -> [Later (Future.chain ~pure:true fc Univ.ContextSet.constraints)]
+            | None -> [Later (Future.chain
+                 ~greedy:(not (Future.is_exn fc))
+                 ~pure:true fc Univ.ContextSet.constraints)]
             | Some c -> [Now (Univ.ContextSet.constraints c)])
       
 let globalize_mind_universes mb =
@@ -821,7 +823,7 @@ let retroknowledge f senv =
 let register field value by_clause senv =
   (* todo : value closed, by_clause safe, by_clause of the proper type*)
   (* spiwack : updates the safe_env with the information that the register
-     action has to be performed (again) when the environement is imported *)
+     action has to be performed (again) when the environment is imported *)
   { senv with
     env = Environ.register senv.env field value;
     local_retroknowledge =
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a3441aa3..a316b449 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -15,7 +15,6 @@
 open Errors
 open Util
 open Names
-open Univ
 open Term
 open Context
 open Declarations
@@ -101,10 +100,6 @@ let hcons_j j =
 
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-  
-let subst_instance_j s j =
-  { uj_val = Vars.subst_univs_level_constr s j.uj_val;
-    uj_type = Vars.subst_univs_level_constr s j.uj_type }
 
 let infer_declaration env kn dcl =
   match dcl with
@@ -250,12 +245,14 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
   let tps = 
     (* FIXME: incompleteness of the bytecode vm: we compile polymorphic 
        constants like opaque definitions. *)
-    if poly then Cemitcodes.from_val Cemitcodes.BCconstant
+    if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant)
     else
-      match proj with
-      | None -> Cemitcodes.from_val (compile_constant_body env def)
-      | Some pb ->
-	Cemitcodes.from_val (compile_constant_body env (Def (Mod_subst.from_val pb.proj_body)))
+      let res = 
+	match proj with
+	| None -> compile_constant_body env def
+	| Some pb ->
+	   compile_constant_body env (Def (Mod_subst.from_val pb.proj_body))
+      in Option.map Cemitcodes.from_val res
   in
   { const_hyps = hyps;
     const_body = def;
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 696fc3d2..1b54b1ea 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Univ
 open Environ
 open Declarations
 open Entries
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 2642b186..48dbacf1 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -153,13 +153,13 @@ let type_of_constant_type_knowing_parameters env t paramtyps =
 
 let type_of_constant_knowing_parameters env cst paramtyps =
   let cb = lookup_constant (fst cst) env in
-  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
   let ty, cu = constant_type env cst in
     type_of_constant_type_knowing_parameters env ty paramtyps, cu
 
 let type_of_constant_knowing_parameters_in env cst paramtyps =
   let cb = lookup_constant (fst cst) env in
-  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
   let ty = constant_type_in env cst in
     type_of_constant_type_knowing_parameters env ty paramtyps
 
@@ -171,14 +171,14 @@ let type_of_constant env cst =
 
 let type_of_constant_in env cst =
   let cb = lookup_constant (fst cst) env in
-  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let () = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
   let ar = constant_type_in env cst in
     type_of_constant_type_knowing_parameters env ar [||]
 
 let judge_of_constant_knowing_parameters env (kn,u as cst) args =
   let c = mkConstU cst in
   let ty, cu = type_of_constant_knowing_parameters env cst args in
-  let _ = Environ.check_constraints cu env in
+  let () = check_constraints cu env in
     make_judge c ty
 
 let judge_of_constant env cst =
@@ -372,7 +372,7 @@ let judge_of_case env ci pj cj lfj =
   let (pind, _ as indspec) =
     try find_rectype env cj.uj_type
     with Not_found -> error_case_not_inductive env cj in
-  let _ = check_case_info env pind ci in
+  let () = check_case_info env pind ci in
   let (bty,rslty) =
     type_case_branches env indspec pj cj.uj_val in
   let () = check_branch_types env pind cj (lfj,bty) in
diff --git a/kernel/uint31.ml b/kernel/uint31.ml
index 3a0da2f6..d9c723c2 100644
--- a/kernel/uint31.ml
+++ b/kernel/uint31.ml
@@ -1,7 +1,7 @@
   (* Invariant: For arch64 all extra bytes are set to 0 *)
 type t = int 
     
-  (* to be used only on 32 bits achitectures *)
+  (* to be used only on 32 bits architectures *)
 let maxuint31 = Int32.of_string "0x7FFFFFFF"
 let uint_32 i =  Int32.logand (Int32.of_int i) maxuint31
     
@@ -16,7 +16,7 @@ let of_int_64 i = i land 0x7FFFFFFF
 let of_int = select of_int_32 of_int_64
 let of_uint i = i
  	
-    (* convertion of an uint31 to a string *)
+    (* conversion of an uint31 to a string *)
 let to_string_32 i = Int32.to_string (uint_32 i)
 let to_string_64 = string_of_int 
 
diff --git a/kernel/uint31.mli b/kernel/uint31.mli
index e8b98080..d1f933cc 100644
--- a/kernel/uint31.mli
+++ b/kernel/uint31.mli
@@ -5,7 +5,7 @@ val to_int : t -> int
 val of_int : int -> t
 val of_uint : int -> t
 
-     (* convertion to a string *)
+     (* conversion to a string *)
 val to_string : t -> string
 val of_string : string -> t
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 08e9fee0..763c0822 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -194,7 +194,17 @@ struct
     | Level _, _ -> -1
     | _, Level _ -> 1
     | Var n, Var m -> Int.compare n m
-      
+
+  let hequal x y =
+    x == y ||
+      match x, y with
+      | Prop, Prop -> true
+      | Set, Set -> true
+      | Level (n,d), Level (n',d') ->
+        n == n' && d == d'
+      | Var n, Var n' -> n == n'
+      | _ -> false
+
   let hcons = function
     | Prop as x -> x
     | Set as x -> x
@@ -233,27 +243,26 @@ module Level = struct
 
   let hash x = x.hash
 
-  let hcons x = 
-    let data' = RawLevel.hcons x.data in
-      if data' == x.data then x
-      else { x with data = data' }
-
   let data x = x.data
 
   (** Hashcons on levels + their hash *)
 
-  let make =
-    let module Self = struct
-      type _t = t
-      type t = _t
-      let equal = equal
-      let hash = hash
-    end in
-    let module WH = Weak.Make(Self) in
-    let pool = WH.create 4910 in fun x ->
-    let x = { hash = RawLevel.hash x; data = x } in
-    try WH.find pool x
-    with Not_found -> WH.add pool x; x
+  module Self = struct
+    type _t = t
+    type t = _t
+    type u = unit
+    let equal x y = x.hash == y.hash && RawLevel.hequal x.data y.data
+    let hash x = x.hash
+    let hashcons () x =
+      let data' = RawLevel.hcons x.data in
+      if x.data == data' then x else { x with data = data' }
+  end
+
+  let hcons =
+    let module H = Hashcons.Make(Self) in
+    Hashcons.simple_hcons H.generate H.hcons ()
+
+  let make l = hcons { hash = RawLevel.hash l; data = l }
 
   let set = make Set
   let prop = make Prop
@@ -2064,7 +2073,7 @@ let explain_universe_inconsistency prl (o,u,v,p) =
 	    (spc() ++ str "= " ++ pr_uni u)) 
   in
     str "Cannot enforce" ++ spc() ++ pr_uni u ++ spc() ++
-      pr_rel o ++ spc() ++ pr_uni v ++ reason ++ str")"
+      pr_rel o ++ spc() ++ pr_uni v ++ reason
 
 let compare_levels = Level.compare
 let eq_levels = Level.equal
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 80b15f8b..1c31cc04 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -42,8 +42,6 @@ let conv_vect fconv vect1 vect2 cu =
 
 let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
 
-let eq_table_key = Names.eq_table_key eq_constant
-
 let rec conv_val env pb k v1 v2 cu =
   if v1 == v2 then cu
   else conv_whd env pb k (whd_val v1) (whd_val v2) cu
@@ -66,8 +64,9 @@ and conv_whd env pb k whd1 whd2 cu =
   | Vconstr_const i1, Vconstr_const i2 ->
       if Int.equal i1 i2 then cu else raise NotConvertible
   | Vconstr_block b1, Vconstr_block b2 ->
+      let tag1 = btag b1 and tag2 = btag b2 in
       let sz = bsize b1 in
-      if Int.equal (btag b1) (btag b2) && Int.equal sz (bsize b2) then
+      if Int.equal tag1 tag2 && Int.equal sz (bsize b2) then
 	let rcu = ref cu in
 	for i = 0 to sz - 1 do
 	  rcu := conv_val env CONV k (bfield b1 i) (bfield b2 i) !rcu
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 2cc1efe4..d4bf461b 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -79,7 +79,7 @@ type vprod
 type vfun
 type vfix
 type vcofix
-type vblock
+type vblock 
 type arguments
 
 type vm_env
@@ -224,10 +224,9 @@ let whd_val : values -> whd =
 	   | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
 	   | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
 	   | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work"))
-	else Vconstr_block(Obj.obj o)
-
-
-
+	else 
+          Vconstr_block(Obj.obj o)
+         
 (************************************************)
 (* Abstrct machine ******************************)
 (************************************************)
@@ -518,8 +517,13 @@ let type_of_switch sw =
 let branch_arg k (tag,arity) =
   if Int.equal arity 0 then  ((Obj.magic tag):values)
   else
-    let b = Obj.new_block tag arity in
-    for i = 0 to arity - 1 do
+    let b, ofs = 
+      if tag < last_variant_tag then Obj.new_block tag arity, 0
+      else
+        let b = Obj.new_block last_variant_tag (arity+1) in
+        Obj.set_field b 0 (Obj.repr (tag-last_variant_tag));
+        b,1 in
+    for i = ofs to ofs + arity - 1 do
       Obj.set_field b i (Obj.repr (val_of_rel (k+i)))
     done;
     val_of_obj b
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 295ea83c..51903568 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -94,7 +94,7 @@ val reduce_cofix : int -> vcofix -> values array * values array
 
 (** Block *)
 
-val btag : vblock -> int
+val btag  : vblock -> int
 val bsize : vblock -> int
 val bfield : vblock -> int -> values