10 files changed, 535 insertions, 377 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index d2c88bffcc..2293ae9dfd 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -193,6 +193,12 @@ if (sp - num_args < coq_stack_threshold) {                                     \
 #define AllocCarry(cond) Alloc_small(accu, 1, (cond)? coq_tag_C1 : coq_tag_C0)
 #define AllocPair() Alloc_small(accu, 2, coq_tag_pair)
 
+#define Swap_accu_sp do{                        \
+    value swap_accu_sp_tmp__ = accu;            \
+    accu = *sp;                                 \
+    *sp = swap_accu_sp_tmp__;                   \
+  }while(0)
+
 /* For signal handling, we hijack some code from the caml runtime */
 
 extern intnat caml_signals_are_pending;
@@ -1213,7 +1219,7 @@ value coq_interprete
         /* Adds the integer in the accumulator with 
            the one ontop of the stack (which is poped)*/
         print_instr("ADDINT63");
-        accu = uint63_add(accu, *sp++);
+        Uint63_add(accu, *sp++);
         Next;
       }
 
@@ -1221,10 +1227,12 @@ value coq_interprete
         print_instr("CHECKADDCINT63");
         CheckInt2();
 	/* returns the sum with a carry */
-        value s;
-        s = uint63_add(accu, *sp++);
-        AllocCarry(uint63_lt(s,accu));
-        Field(accu, 0) = s;
+        int c;
+        Uint63_add(accu, *sp);
+        Uint63_lt(c, accu, *sp);
+        Swap_accu_sp;
+        AllocCarry(c);
+        Field(accu, 0) = *sp++;
 	Next;
       }
 
@@ -1232,10 +1240,12 @@ value coq_interprete
         print_instr("ADDCARRYCINT63");
         CheckInt2();
 	/* returns the sum plus one with a carry */
-        value s;
-        s = uint63_addcarry(accu, *sp++);
-        AllocCarry(uint63_leq(s, accu));
-        Field(accu, 0) = s;
+        int c;
+        Uint63_addcarry(accu, *sp);
+        Uint63_leq(c, accu, *sp);
+        Swap_accu_sp;
+        AllocCarry(c);
+        Field(accu, 0) = *sp++;
 	Next;
       }
 
@@ -1246,7 +1256,7 @@ value coq_interprete
       Instruct (SUBINT63) {
         print_instr("SUBINT63");
 	/* returns the subtraction */
-        accu = uint63_sub(accu, *sp++);
+        Uint63_sub(accu, *sp++);
         Next;
       }
 
@@ -1254,12 +1264,12 @@ value coq_interprete
         print_instr("SUBCINT63");
         CheckInt2();
 	/* returns the subtraction with a carry */
-        value b;
-        value s;
-        b = *sp++;
-        s = uint63_sub(accu,b);
-        AllocCarry(uint63_lt(accu,b));
-        Field(accu, 0) = s;
+        int c;
+        Uint63_lt(c, accu, *sp);
+        Uint63_sub(accu, *sp);
+        Swap_accu_sp;
+        AllocCarry(c);
+        Field(accu, 0) = *sp++;
 	Next;
       }
 
@@ -1267,12 +1277,12 @@ value coq_interprete
         print_instr("SUBCARRYCINT63");
         CheckInt2();
 	/* returns the subtraction minus one with a carry */
-        value b;
-        value s;
-        b = *sp++;
-        s = uint63_subcarry(accu,b);
-        AllocCarry(uint63_leq(accu,b));
-        Field(accu, 0) = s;
+        int c;
+        Uint63_leq(c,accu,*sp);
+        Uint63_subcarry(accu,*sp);
+        Swap_accu_sp;
+        AllocCarry(c);
+        Field(accu, 0) = *sp++;
 	Next;
       }
 
@@ -1280,7 +1290,7 @@ value coq_interprete
         print_instr("MULINT63");
         CheckInt2();
 	/* returns the multiplication */
-        accu = uint63_mul(accu,*sp++);
+        Uint63_mul(accu,*sp++);
 	Next;
       }
 
@@ -1294,9 +1304,11 @@ value coq_interprete
         AllocPair(); */
         /* Field(accu, 0) = (value)(I64_lsr(p,31)|1) ; */ /*higher part*/
         /* Field(accu, 1) = (value)(I64_to_int32(p)|1); */ /*lower part*/
-        value x = accu;
+        Uint63_mulc(accu, *sp, sp);
+        *--sp = accu;
         AllocPair();
-        Field(accu, 1) = uint63_mulc(x, *sp++, &Field(accu, 0));
+        Field(accu, 1) = *sp++;
+        Field(accu, 0) = *sp++;
         Next;
       }
 
@@ -1306,13 +1318,13 @@ 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 */
-        value divisor;
-        divisor = *sp++;
-        if (uint63_eq0(divisor)) {
-          accu = divisor;
+        int b;
+        Uint63_eq0(b, *sp);
+        if (b) {
+          accu = *sp++;
 	}
 	else {
-          accu = uint63_div(accu, divisor);
+          Uint63_div(accu, *sp++);
         }
 	Next;
       }
@@ -1320,13 +1332,13 @@ value coq_interprete
       Instruct(CHECKMODINT63) {
         print_instr("CHEKMODINT63");
         CheckInt2();
-        value divisor;
-        divisor = *sp++;
-        if (uint63_eq0(divisor)) {
-          accu = divisor;
+        int b;
+        Uint63_eq0(b, *sp);
+        if (b) {
+          accu = *sp++;
 	}
         else {
-          accu = uint63_mod(accu,divisor);
+          Uint63_mod(accu,*sp++);
 	}
 	Next;
       }
@@ -1337,19 +1349,24 @@ 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 */
-        value divisor;
-        divisor = *sp++;
-        if (uint63_eq0(divisor)) {
-          Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-          Field(accu, 0) = divisor;
-          Field(accu, 1) = divisor;
+        int b;
+        Uint63_eq0(b, *sp);
+        if (b) {
+          AllocPair();
+          Field(accu, 0) = *sp;
+          Field(accu, 1) = *sp++;
         }
         else {
-          value modulus;
-          modulus = accu;
-          Alloc_small(accu, 2, 1); /* ( _ , arity, tag ) */
-          Field(accu, 0) = uint63_div(modulus,divisor);
-          Field(accu, 1) = uint63_mod(modulus,divisor);
+          *--sp = accu;
+          Uint63_div(sp[0],sp[1]);
+          Swap_accu_sp;
+          Uint63_mod(accu,sp[1]);
+          sp[1] = sp[0];
+          Swap_accu_sp;
+          AllocPair();
+          Field(accu, 0) = sp[1];
+          Field(accu, 1) = sp[0];
+          sp += 2;
         }
 	Next;
       }
@@ -1376,59 +1393,57 @@ value coq_interprete
           Field(accu, 0) = value_of_uint32(I64_to_int32(quo));
           Field(accu, 1) = value_of_uint32(I64_to_int32(mod));
         } */
-        value bigint; /* TODO: fix */
-        bigint = *sp++; /* TODO: take accu into account */
-        value divisor;
-        divisor = *sp++;
-        if (uint63_eq0(divisor)) {
-          Alloc_small(accu, 2, 1);
-          Field(accu, 0) = divisor;
-          Field(accu, 1) = divisor;
+        int b;
+        Uint63_eq0(b, sp[1]);
+        if (b) {
+          AllocPair();
+          Field(accu, 0) = sp[1];
+          Field(accu, 1) = sp[1];
 	}
         else {
-          value quo, mod;
-          mod = uint63_div21(accu, bigint, divisor, &quo);
-          Alloc_small(accu, 2, 1);
-          Field(accu, 0) = quo;
-          Field(accu, 1) = mod;
+          Uint63_div21(accu, sp[0], sp[1], sp);
+          sp[1] = sp[0];
+          Swap_accu_sp;
+          AllocPair();
+          Field(accu, 0) = sp[1];
+          Field(accu, 1) = sp[0];
 	}
+        sp += 2;
         Next;
       }
 
       Instruct(CHECKLXORINT63) {
         print_instr("CHECKLXORINT63");
         CheckInt2();
-        accu = uint63_lxor(accu,*sp++);
+        Uint63_lxor(accu,*sp++);
         Next;
       }
 
       Instruct(CHECKLORINT63) {
         print_instr("CHECKLORINT63");
         CheckInt2();
-        accu = uint63_lor(accu,*sp++);
+        Uint63_lor(accu,*sp++);
         Next;
       }
 
       Instruct(CHECKLANDINT63) {
         print_instr("CHECKLANDINT63");
         CheckInt2();
-        accu = uint63_land(accu,*sp++);
+        Uint63_land(accu,*sp++);
         Next;
       }
 
       Instruct(CHECKLSLINT63) {
         print_instr("CHECKLSLINT63");
         CheckInt2();
-        value p = *sp++;
-        accu = uint63_lsl(accu,p);
+        Uint63_lsl(accu,*sp++);
         Next;
       }
 
       Instruct(CHECKLSRINT63) {
         print_instr("CHECKLSRINT63");
         CheckInt2();
-        value p = *sp++;
-        accu = uint63_lsr(accu,p);
+        Uint63_lsr(accu,*sp++);
         Next;
       }
 
@@ -1436,7 +1451,7 @@ value coq_interprete
         print_instr("CHECKLSLINT63CONST1");
         if (Is_uint63(accu)) {
           pc++;
-          accu = uint63_lsl1(accu);
+          Uint63_lsl1(accu);
           Next;
         } else {
           *--sp = uint63_one();
@@ -1450,7 +1465,7 @@ value coq_interprete
         print_instr("CHECKLSRINT63CONST1");
         if (Is_uint63(accu)) {
           pc++;
-          accu = uint63_lsr1(accu);
+          Uint63_lsr1(accu);
           Next;
         } else {
           *--sp = uint63_one();
@@ -1463,18 +1478,17 @@ value coq_interprete
       Instruct (CHECKADDMULDIVINT63) {
         print_instr("CHECKADDMULDIVINT63");
         CheckInt3();
-        value x;
-        value y;
-        x = *sp++;
-        y = *sp++;
-        accu = uint63_addmuldiv(accu,x,y);
+        Uint63_addmuldiv(accu,sp[0],sp[1]);
+        sp += 2;
         Next;
       }
 
       Instruct (CHECKEQINT63) {
         print_instr("CHECKEQINT63");
         CheckInt2();
-        accu = uint63_eq(accu,*sp++) ? coq_true : coq_false;
+        int b;
+        Uint63_eq(b, accu, *sp++);
+        accu = b ? coq_true : coq_false;
         Next;
       }
 
@@ -1484,7 +1498,9 @@ value coq_interprete
      }
      Instruct (LTINT63) {
        print_instr("LTINT63");
-       accu = uint63_lt(accu,*sp++) ? coq_true : coq_false;
+       int b;
+       Uint63_lt(b,accu,*sp++);
+       accu = b ? coq_true : coq_false;
        Next;
      }
 
@@ -1494,7 +1510,9 @@ value coq_interprete
      }
      Instruct (LEINT63) {
        print_instr("LEINT63");
-       accu = uint63_leq(accu,*sp++) ? coq_true : coq_false;
+       int b;
+       Uint63_leq(b,accu,*sp++);
+       accu = b ? coq_true : coq_false;
        Next;
      }
 
@@ -1503,25 +1521,30 @@ value coq_interprete
         /* assumes Inductive _ : _ := Eq | Lt | Gt */
         print_instr("CHECKCOMPAREINT63");
         CheckInt2();
-        if (uint63_eq(accu,*sp)) {
+        int b;
+        Uint63_eq(b, accu, *sp);
+        if (b) {
           accu = coq_Eq;
           sp++;
         }
-        else accu = uint63_lt(accu,*sp++) ? coq_Lt : coq_Gt;
+        else {
+          Uint63_lt(b, accu, *sp++);
+          accu = b ? coq_Lt : coq_Gt;
+        }
         Next;
       }
 
       Instruct (CHECKHEAD0INT63) {
         print_instr("CHECKHEAD0INT63");
         CheckInt1();
-        accu = uint63_head0(accu);
+        Uint63_head0(accu);
         Next;
       }
 
       Instruct (CHECKTAIL0INT63) {
         print_instr("CHECKTAIL0INT63");
         CheckInt1();
-        accu = uint63_tail0(accu);
+        Uint63_tail0(accu);
         Next;
       }
 
diff --git a/kernel/byterun/coq_memory.h b/kernel/byterun/coq_memory.h
index 9375b15de2..1ea461c5e5 100644
--- a/kernel/byterun/coq_memory.h
+++ b/kernel/byterun/coq_memory.h
@@ -19,7 +19,7 @@
 
 
 #define Coq_stack_size (4096 * sizeof(value))
-#define Coq_stack_threshold (256 * sizeof(value))
+#define Coq_stack_threshold (256 * sizeof(value))  /* see kernel/cbytegen.ml */
 #define Coq_max_stack_size (256 * 1024)
 
 #define TRANSP 0
diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h
index 5499f124a2..d982f67566 100644
--- a/kernel/byterun/coq_uint63_emul.h
+++ b/kernel/byterun/coq_uint63_emul.h
@@ -15,83 +15,142 @@ value uint63_##name() { \
   }
 
 # define DECLARE_UNOP(name) \
-value uint63_##name(value x) { \
+value uint63_##name##_ml(value x) { \
   static value* cb = 0; \
   CAMLparam1(x); \
   if (!cb) cb = caml_named_value("uint63 " #name); \
   CAMLreturn(caml_callback(*cb, x)); \
   }
 
-# define DECLARE_PREDICATE(name) \
-value uint63_##name(value x) { \
-  static value* cb = 0; \
-  CAMLparam1(x); \
-  if (!cb) cb = caml_named_value("uint63 " #name); \
-  CAMLreturn(Int_val(caml_callback(*cb, x))); \
-  }
+# define CALL_UNOP_NOASSIGN(name, x) \
+  value uint63_return_value__; \
+  value uint63_arg_x__ = (x); \
+  Setup_for_gc; \
+  uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__); \
+  Restore_after_gc
+
+# define CALL_UNOP(name, x) do{ \
+    CALL_UNOP_NOASSIGN(name, x); \
+    accu = uint63_return_value__; \
+  }while(0)
+
+# define CALL_PREDICATE(r, name, x) do{ \
+    CALL_UNOP_NOASSIGN(name, x); \
+    (r) = Int_val(uint63_return_value__); \
+  }while(0)
 
 # define DECLARE_BINOP(name) \
-value uint63_##name(value x, value y) { \
+value uint63_##name##_ml(value x, value y) { \
   static value* cb = 0; \
   CAMLparam2(x, y); \
   if (!cb) cb = caml_named_value("uint63 " #name); \
   CAMLreturn(caml_callback2(*cb, x, y)); \
   }
 
-# define DECLARE_RELATION(name) \
-value uint63_##name(value x, value y) { \
-  static value* cb = 0; \
-  CAMLparam2(x, y); \
-  if (!cb) cb = caml_named_value("uint63 " #name); \
-  CAMLreturn(Int_val(caml_callback2(*cb, x, y))); \
-  }
+# define CALL_BINOP_NOASSIGN(name, x, y) \
+  value uint63_return_value__; \
+  value uint63_arg_x__ = (x); \
+  value uint63_arg_y__ = (y); \
+  Setup_for_gc; \
+  uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__); \
+  Restore_after_gc
+
+# define CALL_BINOP(name, x, y) do{ \
+    CALL_BINOP_NOASSIGN(name, x, y);  \
+    accu = uint63_return_value__; \
+  }while(0)
+
+# define CALL_RELATION(r, name, x, y) do{ \
+    CALL_BINOP_NOASSIGN(name, x, y); \
+    (r) = Int_val(uint63_return_value__); \
+  }while(0)
 
 # define DECLARE_TEROP(name) \
-value uint63_##name(value x, value y, value z) { \
+value uint63_##name##_ml(value x, value y, value z) { \
   static value* cb = 0; \
   CAMLparam3(x, y, z); \
   if (!cb) cb = caml_named_value("uint63 " #name); \
   CAMLreturn(caml_callback3(*cb, x, y, z)); \
   }
 
+# define CALL_TEROP(name, x, y, z) do{ \
+    value uint63_return_value__; \
+    value uint63_arg_x__ = (x); \
+    value uint63_arg_y__ = (y); \
+    value uint63_arg_z__ = (z); \
+    Setup_for_gc; \
+    uint63_return_value__ = uint63_##name##_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \
+    Restore_after_gc; \
+    accu = uint63_return_value__; \
+  }while(0)
 
 DECLARE_NULLOP(one)
 DECLARE_BINOP(add)
+#define Uint63_add(x, y) CALL_BINOP(add, x, y)
 DECLARE_BINOP(addcarry)
+#define Uint63_addcarry(x, y) CALL_BINOP(addcarry, x, y)
 DECLARE_TEROP(addmuldiv)
+#define Uint63_addmuldiv(x, y, z) CALL_TEROP(addmuldiv, x, y, z)
 DECLARE_BINOP(div)
-DECLARE_TEROP(div21_ml)
-DECLARE_RELATION(eq)
-DECLARE_PREDICATE(eq0)
+#define Uint63_div(x, y) CALL_BINOP(div, x, y)
+DECLARE_BINOP(eq)
+#define Uint63_eq(r, x, y) CALL_RELATION(r, eq, x, y)
+DECLARE_UNOP(eq0)
+#define Uint63_eq0(r, x) CALL_PREDICATE(r, eq0, x)
 DECLARE_UNOP(head0)
+#define Uint63_head0(x) CALL_UNOP(head0, x)
 DECLARE_BINOP(land)
-DECLARE_RELATION(leq)
+#define Uint63_land(x, y) CALL_BINOP(land, x, y)
+DECLARE_BINOP(leq)
+#define Uint63_leq(r, x, y) CALL_RELATION(r, leq, x, y)
 DECLARE_BINOP(lor)
+#define Uint63_lor(x, y) CALL_BINOP(lor, x, y)
 DECLARE_BINOP(lsl)
+#define Uint63_lsl(x, y) CALL_BINOP(lsl, x, y)
 DECLARE_UNOP(lsl1)
+#define Uint63_lsl1(x) CALL_UNOP(lsl1, x)
 DECLARE_BINOP(lsr)
+#define Uint63_lsr(x, y) CALL_BINOP(lsr, x, y)
 DECLARE_UNOP(lsr1)
-DECLARE_RELATION(lt)
+#define Uint63_lsr1(x) CALL_UNOP(lsr1, x)
+DECLARE_BINOP(lt)
+#define Uint63_lt(r, x, y) CALL_RELATION(r, lt, x, y)
 DECLARE_BINOP(lxor)
+#define Uint63_lxor(x, y) CALL_BINOP(lxor, x, y)
 DECLARE_BINOP(mod)
+#define Uint63_mod(x, y) CALL_BINOP(mod, x, y)
 DECLARE_BINOP(mul)
-DECLARE_BINOP(mulc_ml)
+#define Uint63_mul(x, y) CALL_BINOP(mul, x, y)
 DECLARE_BINOP(sub)
+#define Uint63_sub(x, y) CALL_BINOP(sub, x, y)
 DECLARE_BINOP(subcarry)
+#define Uint63_subcarry(x, y) CALL_BINOP(subcarry, x, y)
 DECLARE_UNOP(tail0)
+#define Uint63_tail0(x) CALL_UNOP(tail0, x)
+
+DECLARE_TEROP(div21_ml)
+# define Uint63_div21(x, y, z, q) do{ \
+    value uint63_return_value__; \
+    value uint63_arg_x__ = (x); \
+    value uint63_arg_y__ = (y); \
+    value uint63_arg_z__ = (z); \
+    Setup_for_gc; \
+    uint63_return_value__ = \
+      uint63_div21_ml_ml(uint63_arg_x__, uint63_arg_y__, uint63_arg_z__); \
+    Restore_after_gc; \
+    *q = Field(uint63_return_value__, 0); \
+    accu = Field(uint63_return_value__, 1); \
+  }while(0)
 
-value uint63_div21(value x, value y, value z, value* q) {
-  CAMLparam3(x, y, z);
-  CAMLlocal1(qr);
-  qr = uint63_div21_ml(x, y, z);
-  *q = Field(qr, 0);
-  CAMLreturn(Field(qr, 1));
-}
-
-value uint63_mulc(value x, value y, value* h) {
-  CAMLparam2(x, y);
-  CAMLlocal1(hl);
-  hl = uint63_mulc_ml(x, y);
-  *h = Field(hl, 0);
-  CAMLreturn(Field(hl, 1));
-}
+DECLARE_BINOP(mulc_ml)
+# define Uint63_mulc(x, y, h) do{ \
+    value uint63_return_value__; \
+    value uint63_arg_x__ = (x); \
+    value uint63_arg_y__ = (y); \
+    Setup_for_gc; \
+    uint63_return_value__ = \
+      uint63_mulc_ml_ml(uint63_arg_x__, uint63_arg_y__); \
+    Restore_after_gc; \
+    *(h) = Field(uint63_return_value__, 0); \
+    accu = Field(uint63_return_value__, 1); \
+  }while(0)
diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h
index 92f4dc79bc..d431dc1e5c 100644
--- a/kernel/byterun/coq_uint63_native.h
+++ b/kernel/byterun/coq_uint63_native.h
@@ -9,28 +9,43 @@
 #define uint63_one() ((value) 3) /* 2*1 + 1 */
 
 #define uint63_eq(x,y) ((x) == (y))
-#define uint63_eq0(x) ((x) == (uint64_t)1)
+#define Uint63_eq(r,x,y) ((r) = uint63_eq(x,y))
+#define Uint63_eq0(r,x) ((r) = ((x) == (uint64_t)1))
 #define uint63_lt(x,y) ((uint64_t) (x) < (uint64_t) (y))
+#define Uint63_lt(r,x,y) ((r) = uint63_lt(x,y))
 #define uint63_leq(x,y) ((uint64_t) (x) <= (uint64_t) (y))
+#define Uint63_leq(r,x,y) ((r) = uint63_leq(x,y))
 
-#define uint63_add(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) - 1))
-#define uint63_addcarry(x,y) ((value)((uint64_t) (x) + (uint64_t) (y) + 1))
-#define uint63_sub(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) + 1))
-#define uint63_subcarry(x,y) ((value)((uint64_t) (x) - (uint64_t) (y) - 1))
-#define uint63_mul(x,y) (Val_long(uint63_of_value(x) * uint63_of_value(y)))
-#define uint63_div(x,y) (Val_long(uint63_of_value(x) / uint63_of_value(y)))
-#define uint63_mod(x,y) (Val_long(uint63_of_value(x) % uint63_of_value(y)))
+#define Uint63_add(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) - 1))
+#define Uint63_addcarry(x,y) (accu = (value)((uint64_t) (x) + (uint64_t) (y) + 1))
+#define Uint63_sub(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) + 1))
+#define Uint63_subcarry(x,y) (accu = (value)((uint64_t) (x) - (uint64_t) (y) - 1))
+#define Uint63_mul(x,y) (accu = Val_long(uint63_of_value(x) * uint63_of_value(y)))
+#define Uint63_div(x,y) (accu = Val_long(uint63_of_value(x) / uint63_of_value(y)))
+#define Uint63_mod(x,y) (accu = Val_long(uint63_of_value(x) % uint63_of_value(y)))
 
-#define uint63_lxor(x,y) ((value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
-#define uint63_lor(x,y) ((value)((uint64_t)(x) | (uint64_t)(y)))
-#define uint63_land(x,y) ((value)((uint64_t)(x) & (uint64_t)(y)))
+#define Uint63_lxor(x,y) (accu = (value)(((uint64_t)(x) ^ (uint64_t)(y)) | 1))
+#define Uint63_lor(x,y) (accu = (value)((uint64_t)(x) | (uint64_t)(y)))
+#define Uint63_land(x,y) (accu = (value)((uint64_t)(x) & (uint64_t)(y)))
 
 /* TODO: is + or | better? OCAML uses + */
 /* TODO: is - or ^ better? */
-#define uint63_lsl(x,y) ((y) < (uint64_t) 127 ? ((value)((((uint64_t)(x)-1) << (uint63_of_value(y))) | 1)) : uint63_zero)
-#define uint63_lsr(x,y) ((y) < (uint64_t) 127 ? ((value)(((uint64_t)(x) >> (uint63_of_value(y))) | 1)) : uint63_zero)
-#define uint63_lsl1(x) ((value)((((uint64_t)(x)-1) << 1) +1))
-#define uint63_lsr1(x) ((value)(((uint64_t)(x) >> 1) |1))
+#define Uint63_lsl(x,y) do{ \
+  value uint63_lsl_y__ = (y); \
+  if (uint63_lsl_y__ < (uint64_t) 127) \
+    accu = (value)((((uint64_t)(x)-1) << uint63_of_value(uint63_lsl_y__)) | 1); \
+  else \
+    accu = uint63_zero; \
+  }while(0)
+#define Uint63_lsr(x,y) do{ \
+  value uint63_lsl_y__ = (y); \
+  if (uint63_lsl_y__ < (uint64_t) 127) \
+    accu = (value)(((uint64_t)(x) >> uint63_of_value(uint63_lsl_y__)) | 1); \
+  else \
+    accu = uint63_zero; \
+  }while(0)
+#define Uint63_lsl1(x) (accu = (value)((((uint64_t)(x)-1) << 1) +1))
+#define Uint63_lsr1(x) (accu = (value)(((uint64_t)(x) >> 1) |1))
 
 /* addmuldiv(p,x,y) = x * 2^p + y / 2 ^ (63 - p) */
 /* (modulo 2^63) for p <= 63 */
@@ -40,6 +55,7 @@ value uint63_addmuldiv(uint64_t p, uint64_t x, uint64_t y) {
   r |= ((uint64_t)y >> (63-shiftby)) | 1;
   return r;
 }
+#define Uint63_addmuldiv(p, x, y) (accu = uint63_addmuldiv(p, x, y))
 
 value uint63_head0(uint64_t x) {
   int r = 0;
@@ -51,6 +67,7 @@ value uint63_head0(uint64_t x) {
   if (!(x & 0x8000000000000000)) { x <<=1;   r += 1; }
   return Val_int(r);
 }
+#define Uint63_head0(x) (accu = uint63_head0(x))
 
 value uint63_tail0(value x) {
   int r = 0;
@@ -63,6 +80,7 @@ value uint63_tail0(value x) {
   if (!(x & 0x00000001)) { x >>=1;   r += 1; }
   return Val_int(r);
 }
+#define Uint63_tail0(x) (accu = uint63_tail0(x))
 
 value uint63_mulc(value x, value y, value* h) {
   x = (uint64_t)x >> 1;
@@ -86,6 +104,7 @@ value uint63_mulc(value x, value y, value* h) {
   *h = Val_int(hr);
   return Val_int(lr);
 }
+#define Uint63_mulc(x, y, h) (accu = uint63_mulc(x, y, h))
 
 #define lt128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_lt(xl,yl)))
 #define le128(xh,xl,yh,yl) (uint63_lt(xh,yh) || (uint63_eq(xh,yh) && uint63_leq(xl,yl)))
@@ -123,3 +142,4 @@ value uint63_div21(value xh, value xl, value y, value* q) {
   *q = Val_int(quotient);
   return Val_int(reml);
 }
+#define Uint63_div21(xh, xl, y, q) (accu = uint63_div21(xh, xl, y, q))
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 94ed288d2d..3f791dfc22 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -51,7 +51,6 @@ let fresh_lname n =
 (** Global names **)
 type gname = 
   | Gind of string * inductive (* prefix, inductive name *)
-  | Gconstruct of string * constructor (* prefix, constructor name *)
   | Gconstant of string * Constant.t (* prefix, constant name *)
   | Gproj of string * inductive * int (* prefix, inductive, index (start from 0) *)
   | Gcase of Label.t option * int
@@ -67,8 +66,6 @@ let eq_gname gn1 gn2 =
   match gn1, gn2 with
   | Gind (s1, ind1), Gind (s2, ind2) ->
      String.equal s1 s2 && eq_ind ind1 ind2
-  | Gconstruct (s1, c1), Gconstruct (s2, c2) ->
-      String.equal s1 s2 && eq_constructor c1 c2
   | Gconstant (s1, c1), Gconstant (s2, c2) ->
       String.equal s1 s2 && Constant.equal c1 c2
   | Gproj (s1, ind1, i1), Gproj (s2, ind2, i2) ->
@@ -88,7 +85,7 @@ let eq_gname gn1 gn2 =
   | Ginternal s1, Ginternal s2 -> String.equal s1 s2
   | Grel i1, Grel i2 -> Int.equal i1 i2
   | Gnamed id1, Gnamed id2 -> Id.equal id1 id2
-  | (Gind _| Gconstruct _ | Gconstant _ | Gproj _ | Gcase _ | Gpred _
+  | (Gind _| Gconstant _ | Gproj _ | Gcase _ | Gpred _
     | Gfixtype _ | Gnorm _ | Gnormtbl _ | Ginternal _ | Grel _ | Gnamed _), _ ->
       false
 
@@ -100,19 +97,17 @@ open Hashset.Combine
 let gname_hash gn = match gn with
 | Gind (s, ind) ->
    combinesmall 1 (combine (String.hash s) (ind_hash ind))
-| Gconstruct (s, c) ->
-   combinesmall 2 (combine (String.hash s) (constructor_hash c))
 | Gconstant (s, c) ->
-   combinesmall 3 (combine (String.hash s) (Constant.hash c))
-| Gcase (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gpred (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gfixtype (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gnorm (l, i) -> combinesmall 7 (combine (Option.hash Label.hash l) (Int.hash i))
-| Gnormtbl (l, i) -> combinesmall 8 (combine (Option.hash Label.hash l) (Int.hash i))
-| Ginternal s -> combinesmall 9 (String.hash s)
-| Grel i -> combinesmall 10 (Int.hash i)
-| Gnamed id -> combinesmall 11 (Id.hash id)
-| Gproj (s, p, i) -> combinesmall 12 (combine (String.hash s) (combine (ind_hash p) i))
+   combinesmall 2 (combine (String.hash s) (Constant.hash c))
+| Gcase (l, i) -> combinesmall 3 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gpred (l, i) -> combinesmall 4 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gfixtype (l, i) -> combinesmall 5 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gnorm (l, i) -> combinesmall 6 (combine (Option.hash Label.hash l) (Int.hash i))
+| Gnormtbl (l, i) -> combinesmall 7 (combine (Option.hash Label.hash l) (Int.hash i))
+| Ginternal s -> combinesmall 8 (String.hash s)
+| Grel i -> combinesmall 9 (Int.hash i)
+| Gnamed id -> combinesmall 10 (Id.hash id)
+| Gproj (s, p, i) -> combinesmall 11 (combine (String.hash s) (combine (ind_hash p) i))
 
 let case_ctr = ref (-1)
 
@@ -382,8 +377,8 @@ type mllambda =
   | MLif           of mllambda * mllambda * mllambda
   | MLmatch        of annot_sw * mllambda * mllambda * mllam_branches
                               (* argument, prefix, accu branch, branches *)
-  | MLconstruct    of string * constructor * mllambda array
-                   (* prefix, constructor name, arguments *)
+  | MLconstruct    of string * inductive * int * mllambda array
+                   (* prefix, inductive name, tag, arguments *)
   | MLint          of int
   | MLuint         of Uint63.t
   | MLsetref       of string * mllambda
@@ -391,7 +386,11 @@ type mllambda =
   | MLarray        of mllambda array
   | MLisaccu       of string * inductive * mllambda
 
-and mllam_branches = ((constructor * lname option array) list * mllambda) array
+and 'a mllam_pattern =
+  | ConstPattern of int
+  | NonConstPattern of tag * 'a array
+
+and mllam_branches = (lname option mllam_pattern list * mllambda) array
 
 let push_lnames n env lns =
   snd (Array.fold_left (fun (i,r) x -> (i+1, LNmap.add x i r)) (n,env) lns)
@@ -444,9 +443,10 @@ let rec eq_mllambda gn1 gn2 n env1 env2 t1 t2 =
       eq_mllambda gn1 gn2 n env1 env2 c1 c2 &&
       eq_mllambda gn1 gn2 n env1 env2 accu1 accu2 &&
       eq_mllam_branches gn1 gn2 n env1 env2 br1 br2
-  | MLconstruct (pf1, cs1, args1), MLconstruct (pf2, cs2, args2) ->
+  | MLconstruct (pf1, ind1, tag1, args1), MLconstruct (pf2, ind2, tag2, args2) ->
       String.equal pf1 pf2 &&
-      eq_constructor cs1 cs2 &&
+      eq_ind ind1 ind2 &&
+      Int.equal tag1 tag2 &&
       Array.equal (eq_mllambda gn1 gn2 n env1 env2) args1 args2
   | MLint i1, MLint i2 ->
       Int.equal i1 i2
@@ -479,15 +479,22 @@ and eq_letrec gn1 gn2 n env1 env2 defs1 defs2 =
 
 (* we require here that patterns have the same order, which may be too strong *)
 and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 =
-  let eq_cargs (cs1, args1) (cs2, args2) body1 body2 =
+  let eq_cargs args1 args2 body1 body2 =
     Int.equal (Array.length args1) (Array.length args2) &&
-    eq_constructor cs1 cs2 &&
     let env1 = opush_lnames n env1 args1 in
     let env2 = opush_lnames n env2 args2 in
     eq_mllambda gn1 gn2 (n + Array.length args1) env1 env2 body1 body2
   in
-  let eq_branch (ptl1,body1) (ptl2,body2) =
-   List.equal (fun pt1 pt2 -> eq_cargs pt1 pt2 body1 body2) ptl1 ptl2
+  let eq_pattern pat1 pat2 body1 body2 =
+    match pat1, pat2 with
+    | ConstPattern tag1, ConstPattern tag2 ->
+      Int.equal tag1 tag2 && eq_mllambda gn1 gn2 n env1 env2 body1 body2
+    | NonConstPattern (tag1,args1), NonConstPattern (tag2,args2) ->
+      Int.equal tag1 tag2 && eq_cargs args1 args2 body1 body2
+    | (ConstPattern _ | NonConstPattern _), _ -> false
+  in
+  let eq_branch (patl1,body1) (patl2,body2) =
+    List.equal (fun pt1 pt2 -> eq_pattern pt1 pt2 body1 body2) patl1 patl2
   in
   Array.equal eq_branch br1 br2
 
@@ -523,10 +530,11 @@ let rec hash_mllambda gn n env t =
       let hc = hash_mllambda gn n env c in
       let haccu = hash_mllambda gn n env accu in
       combinesmall 9 (hash_mllam_branches gn n env (combine3 hannot hc haccu) br)
-  | MLconstruct (pf, cs, args) ->
+  | MLconstruct (pf, ind, tag, args) ->
       let hpf = String.hash pf in
-      let hcs = constructor_hash cs in
-      combinesmall 10 (hash_mllambda_array gn n env (combine hpf hcs) args)
+      let hcs = ind_hash ind in
+      let htag = Int.hash tag in
+      combinesmall 10 (hash_mllambda_array gn n env (combine3 hpf hcs htag) args)
   | MLint i ->
       combinesmall 11 i
   | MLuint i ->
@@ -556,15 +564,18 @@ and hash_mllambda_array gn n env init arr =
   Array.fold_left (fun acc t -> combine (hash_mllambda gn n env t) acc) init arr
 
 and hash_mllam_branches gn n env init br =
-  let hash_cargs (cs, args) body =
+  let hash_cargs args body =
     let nargs = Array.length args in
-    let hcs = constructor_hash cs in
     let env = opush_lnames n env args in
     let hbody = hash_mllambda gn (n + nargs) env body in
-    combine3 nargs hcs hbody
+    combine nargs hbody
+  in
+  let hash_pattern pat body = match pat with
+    | ConstPattern i -> combinesmall 1 (Int.hash i)
+    | NonConstPattern (tag,args) -> combinesmall 2 (combine (Int.hash tag) (hash_cargs args body))
   in
   let hash_branch acc (ptl,body) =
-    List.fold_left (fun acc t -> combine (hash_cargs t body) acc) acc ptl
+    List.fold_left (fun acc t -> combine (hash_pattern t body) acc) acc ptl
   in
   Array.fold_left hash_branch init br
 
@@ -594,17 +605,20 @@ let fv_lam l =
     | MLmatch(_,a,p,bs) ->
       let fv = aux a bind (aux p bind fv) in
       let fv_bs (cargs, body) fv =
-	let bind = 
-	  List.fold_right (fun (_,args) bind ->
-	    Array.fold_right 
-	      (fun o bind -> match o with 
-	      | Some l -> LNset.add l bind 
-	      | _ -> bind) args bind) 
-	    cargs bind in
-	aux body bind fv in
+        let bind =
+          List.fold_right (fun pat bind ->
+              match pat with
+              | ConstPattern _ -> bind
+              | NonConstPattern(_,args) ->
+                Array.fold_right
+                  (fun o bind -> match o with
+                     | Some l -> LNset.add l bind
+                     | _ -> bind) args bind)
+            cargs bind in
+        aux body bind fv in
       Array.fold_right fv_bs bs fv
-          (* argument, accu branch, branches *)
-    | MLconstruct (_,_,p) ->
+    (* argument, accu branch, branches *)
+    | MLconstruct (_,_,_,p) ->
 	Array.fold_right (fun a fv -> aux a bind fv) p fv
     | MLsetref(_,l) -> aux l bind fv
     | MLsequence(l1,l2) -> aux l1 bind (aux l2 bind fv)
@@ -652,8 +666,8 @@ type global =
   | Gletcase of 
       gname * lname array * annot_sw * mllambda * mllambda * mllam_branches
   | Gopen of string
-  | Gtype of inductive * int array
-    (* ind name, arities of constructors *)
+  | Gtype of inductive * (tag * int) array
+    (* ind name, tag and arities of constructors *)
   | Gcomment of string
 
 (* Alpha-equivalence on globals *)
@@ -678,7 +692,8 @@ let eq_global g1 g2 =
       eq_mllambda gn1 gn2 (Array.length lns1) env1 env2 t1 t2
   | Gopen s1, Gopen s2 -> String.equal s1 s2
   | Gtype (ind1, arr1), Gtype (ind2, arr2) ->
-      eq_ind ind1 ind2 && Array.equal Int.equal arr1 arr2
+    eq_ind ind1 ind2 &&
+    Array.equal (fun (tag1,ar1) (tag2,ar2) -> Int.equal tag1 tag2 && Int.equal ar1 ar2) arr1 arr2
   | Gcomment s1, Gcomment s2 -> String.equal s1 s2
   | _, _ -> false
 
@@ -705,7 +720,10 @@ let hash_global g =
       combinesmall 4 (combine nlns (hash_mllambda gn nlns env t))
   | Gopen s -> combinesmall 5 (String.hash s)
   | Gtype (ind, arr) ->
-      combinesmall 6 (combine (ind_hash ind) (Array.fold_left combine 0 arr))
+    let hash_aux acc (tag,ar) =
+      combine3 acc (Int.hash tag) (Int.hash ar)
+    in
+    combinesmall 6 (combine (ind_hash ind) (Array.fold_left hash_aux 0 arr))
   | Gcomment s -> combinesmall 7 (String.hash s)
   
 let global_stack = ref ([] : global list)
@@ -912,26 +930,33 @@ let get_proj_code i =
     [|MLglobal symbols_tbl_name; MLint i|])
 
 type rlist =
-  | Rnil 
-  | Rcons of (constructor * lname option array) list ref * LNset.t * mllambda * rlist' 
+  | Rnil
+  | Rcons of lname option mllam_pattern list ref * LNset.t * mllambda * rlist'
 and rlist' = rlist ref
 
-let rm_params fv params = 
-  Array.map (fun l -> if LNset.mem l fv then Some l else None) params 
+let rm_params fv params =
+  Array.map (fun l -> if LNset.mem l fv then Some l else None) params
 
-let rec insert cargs body rl =
+let rec insert pat body rl =
  match !rl with
  | Rnil ->
      let fv = fv_lam body in
-     let (c,params) = cargs in
-     let params = rm_params fv params in
-     rl:= Rcons(ref [(c,params)], fv, body, ref Rnil)
+     begin match pat with
+     | ConstPattern _ as p ->
+       rl:= Rcons(ref [p], fv, body, ref Rnil)
+     | NonConstPattern (tag,args) ->
+       let args = rm_params fv args in
+       rl:= Rcons(ref [NonConstPattern (tag,args)], fv, body, ref Rnil)
+     end
  | Rcons(l,fv,body',rl) ->
-     if eq_mllambda body body' then
-       let (c,params) = cargs in
-       let params = rm_params fv params in
-       l := (c,params)::!l
-     else insert cargs body rl
+   if eq_mllambda body body' then
+     match pat with
+     | ConstPattern _ as p ->
+       l := p::!l
+     | NonConstPattern (tag,args) ->
+       let args = rm_params fv args in
+       l := NonConstPattern (tag,args)::!l
+   else insert pat body rl
 
 let rec to_list rl =
   match !rl with
@@ -940,7 +965,7 @@ let rec to_list rl =
 
 let merge_branches t =
   let newt = ref Rnil in
-  Array.iter (fun (c,args,body) -> insert (c,args) body newt) t;
+  Array.iter (fun (pat,body) -> insert pat body newt) t;
   Array.of_list (to_list newt)
 
 let app_prim p args = MLapp(MLprimitive p, args)
@@ -1097,14 +1122,19 @@ let ml_of_instance instance u =
       let a_uid = fresh_lname Anonymous in
       let la_uid = MLlocal a_uid in
       (* compilation of branches *)
-      let ml_br (c,params, body) = 
-	let lnames, env_c = push_rels env_c params in
-	(c, lnames, ml_of_lam env_c l body)
+      let nbconst = Array.length bs.constant_branches in
+      let nbtotal = nbconst + Array.length bs.nonconstant_branches in
+      let br = Array.init nbtotal (fun i -> if i < Array.length bs.constant_branches then
+                                  (ConstPattern i, ml_of_lam env_c l bs.constant_branches.(i))
+                                else
+                                  let (params, body) = bs.nonconstant_branches.(i-nbconst) in
+                                  let lnames, env_c = push_rels env_c params in
+                                  (NonConstPattern (i-nbconst+1,lnames), ml_of_lam env_c l body)
+                              )
       in
-      let bs = Array.map ml_br bs in
       let cn = fresh_gcase l in
       (* Compilation of accu branch *)
-      let pred = MLapp(MLglobal pn, fv_args env_c pfvn pfvr) in  
+      let pred = MLapp(MLglobal pn, fv_args env_c pfvn pfvr) in
       let (fvn, fvr) = !(env_c.env_named), !(env_c.env_urel) in
       let cn_fv = mkMLapp (MLglobal cn) (fv_args env_c fvn fvr) in
          (* remark : the call to fv_args does not add free variables in env_c *)
@@ -1117,7 +1147,7 @@ let ml_of_instance instance u =
 (*      let body = MLlam([|a_uid|], MLmatch(annot, la_uid, accu, bs)) in
       let case = generalize_fv env_c body in *)
       let cn = push_global_case cn (Array.append (fv_params env_c) [|a_uid|])
-        annot la_uid accu (merge_branches bs)
+        annot la_uid accu (merge_branches br)
       in
       (* Final result *)
       let arg = ml_of_lam env l a in
@@ -1277,12 +1307,11 @@ let ml_of_instance instance u =
 	(lname, paramsi, body) in
       MLletrec(Array.mapi mkrec lf, lf_args.(start)) *)
 
-  | Lmakeblock (prefix,(cn,_u),_,args) ->
+  | Lint tag -> MLapp(MLprimitive Mk_int, [|MLint tag|])
+
+  | Lmakeblock (prefix,cn,tag,args) ->
      let args = Array.map (ml_of_lam env l) args in
-     MLconstruct(prefix,cn,args)
-  | Lconstruct (prefix, (cn,u)) ->
-     let uargs = ml_of_instance env.env_univ u in
-      mkMLapp (MLglobal (Gconstruct (prefix, cn))) uargs
+     MLconstruct(prefix,cn,tag,args)
   | Luint i -> MLapp(MLprimitive Mk_uint, [|MLuint i|])
   | Lval v ->
       let i = push_symbol (SymbValue v) in get_value_code i
@@ -1345,7 +1374,7 @@ let subst s l =
       | MLmatch(annot,a,accu,bs) ->
 	  let auxb (cargs,body) = (cargs,aux body) in
 	  MLmatch(annot,a,aux accu, Array.map auxb bs)
-      | MLconstruct(prefix,c,args) -> MLconstruct(prefix,c,Array.map aux args)
+      | MLconstruct(prefix,c,tag,args) -> MLconstruct(prefix,c,tag,Array.map aux args)
       | MLsetref(s,l1) -> MLsetref(s,aux l1) 
       | MLsequence(l1,l2) -> MLsequence(aux l1, aux l2)
       | MLarray arr -> MLarray (Array.map aux arr)
@@ -1454,8 +1483,8 @@ let optimize gdef l =
     | MLmatch(annot,a,accu,bs) ->
 	let opt_b (cargs,body) = (cargs,optimize s body) in
 	MLmatch(annot, optimize s a, subst s accu, Array.map opt_b bs)
-    | MLconstruct(prefix,c,args) ->
-        MLconstruct(prefix,c,Array.map (optimize s) args)
+    | MLconstruct(prefix,c,tag,args) ->
+        MLconstruct(prefix,c,tag,Array.map (optimize s) args)
     | MLsetref(r,l) -> MLsetref(r, optimize s l) 
     | MLsequence(l1,l2) -> MLsequence(optimize s l1, optimize s l2)
     | MLarray arr -> MLarray (Array.map (optimize s) arr)
@@ -1528,13 +1557,12 @@ let string_of_kn kn =
 
 let string_of_con c = string_of_kn (Constant.user c)
 let string_of_mind mind = string_of_kn (MutInd.user mind)
+let string_of_ind (mind,i) = string_of_kn (MutInd.user mind) ^ "_" ^ string_of_int i
 
 let string_of_gname g =
   match g with
   | Gind (prefix, (mind, i)) ->
       Format.sprintf "%sindaccu_%s_%i" prefix (string_of_mind mind) i
-  | Gconstruct (prefix, ((mind, i), j)) ->
-      Format.sprintf "%sconstruct_%s_%i_%i" prefix (string_of_mind mind) i (j-1)
   | Gconstant (prefix, c) ->
       Format.sprintf "%sconst_%s" prefix (string_of_con c)
   | Gproj (prefix, (mind, n), i) ->
@@ -1567,10 +1595,13 @@ let pp_ldecls fmt ids =
     Format.fprintf fmt " (%a : Nativevalues.t)" pp_lname ids.(i)
   done
 
-let string_of_construct prefix ((mind,i),j) =
-  let id = Format.sprintf "Construct_%s_%i_%i" (string_of_mind mind) i (j-1) in
-  prefix ^ id
-   
+let string_of_construct prefix ~constant ind tag =
+  let base = if constant then "Int" else "Construct" in
+  Format.sprintf "%s%s_%s_%i" prefix base (string_of_ind ind) tag
+
+let string_of_accu_construct prefix ind =
+  Format.sprintf "%sAccu_%s" prefix (string_of_ind ind)
+
 let pp_int fmt i =
   if i < 0 then Format.fprintf fmt "(%i)" i else Format.fprintf fmt "%i" i
 
@@ -1596,16 +1627,16 @@ let pp_mllam fmt l =
 	Format.fprintf fmt "@[(if %a then@\n  %a@\nelse@\n  %a)@]"
 	  pp_mllam t pp_mllam l1 pp_mllam l2 
     | MLmatch (annot, c, accu_br, br) ->
-	  let mind,i = annot.asw_ind in
+      let ind = annot.asw_ind in
       let prefix = annot.asw_prefix in
-	  let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in
-	  Format.fprintf fmt 
-	    "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n  %a@\n%aend@]"
-	  pp_mllam c accu pp_mllam accu_br (pp_branches prefix) br
-	  
-    | MLconstruct(prefix,c,args) ->
+      let accu = string_of_accu_construct prefix ind in
+      Format.fprintf fmt
+        "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n  %a@\n%aend@]"
+        pp_mllam c accu pp_mllam accu_br (pp_branches prefix ind) br
+
+    | MLconstruct(prefix,ind,tag,args) ->
         Format.fprintf fmt "@[(Obj.magic (%s%a) : Nativevalues.t)@]" 
-          (string_of_construct prefix c) pp_cargs args
+          (string_of_construct prefix ~constant:false ind tag) pp_cargs args
     | MLint i -> pp_int fmt i
     | MLuint i -> Format.fprintf fmt "(%s)" (Uint63.compile i)
     | MLsetref (s, body) ->
@@ -1622,8 +1653,8 @@ let pp_mllam fmt l =
          pp_mllam fmt arr.(len-1)
        end;
        Format.fprintf fmt "|]@]"
-    | MLisaccu (prefix, (mind, i), c) ->
-        let accu = Format.sprintf "%sAccu_%s_%i" prefix (string_of_mind mind) i in
+    | MLisaccu (prefix, ind, c) ->
+        let accu = string_of_accu_construct prefix ind in
         Format.fprintf fmt
           "@[begin match Obj.magic (%a) with@\n| %s _ ->@\n  true@\n| _ ->@\n  false@\nend@]"
         pp_mllam c accu
@@ -1646,7 +1677,7 @@ let pp_mllam fmt l =
     | MLprimitive (Mk_prod | Mk_sort) (* FIXME: why this special case? *)
     | MLlam _ | MLletrec _ | MLlet _ | MLapp _ | MLif _ ->
 	Format.fprintf fmt "(%a)" pp_mllam l
-    | MLconstruct(_,_,args) when Array.length args > 0 ->
+    | MLconstruct(_,_,_,args) when Array.length args > 0 ->
 	Format.fprintf fmt "(%a)" pp_mllam l
     | _ -> pp_mllam fmt l
 
@@ -1685,19 +1716,23 @@ let pp_mllam fmt l =
 	  done in 
 	Format.fprintf fmt "(%a)" aux params
 
-  and pp_branches prefix fmt bs =
+  and pp_branches prefix ind fmt bs =
     let pp_branch (cargs,body) =
-      let pp_c fmt (cn,args) = 
-        Format.fprintf fmt "| %s%a " 
-      (string_of_construct prefix cn) pp_cparams args in
-      let rec pp_cargs fmt cargs =
-        match cargs with
-    | [] -> ()
-    | cargs::cargs' -> 
-        Format.fprintf fmt "%a%a" pp_c cargs pp_cargs cargs' in
-      Format.fprintf fmt "%a ->@\n  %a@\n" 
-    pp_cargs cargs pp_mllam body
+      let pp_pat fmt = function
+        | ConstPattern i ->
+          Format.fprintf fmt "| %s "
+            (string_of_construct prefix ~constant:true ind i)
+        | NonConstPattern (tag,args) ->
+          Format.fprintf fmt "| %s%a "
+            (string_of_construct prefix ~constant:false ind tag) pp_cparams args in
+      let rec pp_pats fmt pats =
+        match pats with
+        | [] -> ()
+        | pat::pats ->
+          Format.fprintf fmt "%a%a" pp_pat pat pp_pats pats
       in
+      Format.fprintf fmt "%a ->@\n  %a@\n" pp_pats cargs pp_mllam body
+    in
     Array.iter pp_branch bs
 
   and pp_primitive fmt = function
@@ -1771,19 +1806,24 @@ let pp_global fmt g =
 	pp_mllam c
   | Gopen s ->
       Format.fprintf fmt "@[open %s@]@." s
-  | Gtype ((mind, i), lar) ->
-      let l = string_of_mind mind in
-      let rec aux s ar = 
-	if Int.equal ar 0 then s else aux (s^" * Nativevalues.t") (ar-1) in
-      let pp_const_sig i fmt j ar =
-        let sig_str = if ar > 0 then aux "of Nativevalues.t" (ar-1) else "" in
-        Format.fprintf fmt "  | Construct_%s_%i_%i %s@\n" l i j sig_str
-      in
-      let pp_const_sigs i fmt lar =
-        Format.fprintf fmt "  | Accu_%s_%i of Nativevalues.t@\n" l i;
-        Array.iteri (pp_const_sig i fmt) lar
-      in
-      Format.fprintf fmt "@[type ind_%s_%i =@\n%a@]@\n@." l i (pp_const_sigs i) lar
+  | Gtype (ind, lar) ->
+    let rec aux s arity =
+      if Int.equal arity 0 then s else aux (s^" * Nativevalues.t") (arity-1) in
+    let pp_const_sig fmt (tag,arity) =
+      if arity > 0 then
+        let sig_str = aux "of Nativevalues.t" (arity-1) in
+        let cstr = string_of_construct "" ~constant:false ind tag in
+        Format.fprintf fmt "  | %s %s@\n" cstr sig_str
+      else
+        let sig_str = if arity > 0 then aux "of Nativevalues.t" (arity-1) else "" in
+        let cstr = string_of_construct "" ~constant:true ind tag in
+        Format.fprintf fmt "  | %s %s@\n" cstr sig_str
+    in
+    let pp_const_sigs fmt lar =
+      Format.fprintf fmt "  | %s of Nativevalues.t@\n" (string_of_accu_construct "" ind);
+      Array.iter (pp_const_sig fmt) lar
+    in
+    Format.fprintf fmt "@[type ind_%s =@\n%a@]@\n@." (string_of_ind ind) pp_const_sigs lar
   | Gtblfixtype (g, params, t) ->
       Format.fprintf fmt "@[let %a %a =@\n  %a@]@\n@." pp_gname g
 	pp_ldecls params pp_array t
@@ -1920,7 +1960,7 @@ let compile_mind mb mind stack =
   (** Generate data for every block *)
   let f i stack ob =
     let ind = (mind, i) in
-    let gtype = Gtype(ind, Array.map snd ob.mind_reloc_tbl) in
+    let gtype = Gtype(ind, ob.mind_reloc_tbl) in
     let j = push_symbol (SymbInd ind) in
     let name = Gind ("", ind) in
     let accu =
@@ -1932,16 +1972,6 @@ let compile_mind mb mind stack =
       Glet(name, MLapp (MLprimitive Mk_ind, args))
     in
     let nparams = mb.mind_nparams in
-    let params = 
-      Array.init nparams (fun i -> {lname = param_name; luid = i}) in
-    let add_construct j acc (_,arity) = 
-      let args = Array.init arity (fun k -> {lname = arg_name; luid = k}) in 
-      let c = ind, (j+1) in
-	  Glet(Gconstruct ("", c),
-	     mkMLlam (Array.append params args)
-	       (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc
-    in
-    let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in
     let add_proj proj_arg acc _pb =
       let tbl = ob.mind_reloc_tbl in
       (* Building info *)
@@ -1953,7 +1983,8 @@ let compile_mind mb mind stack =
                   asw_reloc = tbl; asw_finite = true } in
       let c_uid = fresh_lname Anonymous in
       let cf_uid = fresh_lname Anonymous in
-      let _, arity = tbl.(0) in
+      let tag, arity = tbl.(0) in
+      assert (arity > 0);
       let ci_uid = fresh_lname Anonymous in
       let cargs = Array.init arity
         (fun i -> if Int.equal i proj_arg then Some ci_uid else None)
@@ -1961,7 +1992,7 @@ let compile_mind mb mind stack =
       let i = push_symbol (SymbProj (ind, proj_arg)) in
       let accu = MLapp (MLprimitive Cast_accu, [|MLlocal cf_uid|]) in
       let accu_br = MLapp (MLprimitive Mk_proj, [|get_proj_code i;accu|]) in
-      let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[((ind,1),cargs)],MLlocal ci_uid|]) in
+      let code = MLmatch(asw,MLlocal cf_uid,accu_br,[|[NonConstPattern (tag,cargs)],MLlocal ci_uid|]) in
       let code = MLlet(cf_uid, mkForceCofix "" ind (MLlocal c_uid), code) in
       let gn = Gproj ("", ind, proj_arg) in
       Glet (gn, mkMLlam [|c_uid|] code) :: acc
@@ -1972,7 +2003,7 @@ let compile_mind mb mind stack =
       let _, _, _, pbs = info.(i) in
       Array.fold_left_i add_proj [] pbs
     in
-    projs @ constructors @ gtype :: accu :: stack
+    projs @ gtype :: accu :: stack
   in
   Array.fold_left_i f stack mb.mind_packets
 
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index baa290367f..d153f84e9c 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
 open Names
 open Nativelib
 open Reduction
@@ -152,19 +151,15 @@ let native_conv_gen pb sigma env univs t1 t2 =
   else
   let ml_filename, prefix = get_ml_filename () in
   let code, upds = mk_conv_code env sigma prefix t1 t2 in
-  match compile ml_filename code ~profile:false with
-  | (true, fn) ->
-      begin
-        if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
-        let t0 = Sys.time () in
-        call_linker ~fatal:true prefix fn (Some upds);
-        let t1 = Sys.time () in
-        let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
-        if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
-        (* TODO change 0 when we can have de Bruijn *)
-        fst (conv_val env pb 0 !rt1 !rt2 univs)
-      end
-  | _ -> anomaly (Pp.str "Compilation failure.") 
+  let fn = compile ml_filename code ~profile:false in
+  if !Flags.debug then Feedback.msg_debug (Pp.str "Running test...");
+  let t0 = Sys.time () in
+  call_linker ~fatal:true prefix fn (Some upds);
+  let t1 = Sys.time () in
+  let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
+  if !Flags.debug then Feedback.msg_debug (Pp.str time_info);
+  (* TODO change 0 when we can have de Bruijn *)
+  fst (conv_val env pb 0 !rt1 !rt2 univs)
 
 (* Wrapper for [native_conv] above *)
 let native_conv cv_pb sigma env t1 t2 =
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index ec3a7b893d..62afd9df68 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -39,11 +39,10 @@ type lambda =
   | Lif           of lambda * lambda * lambda
   | Lfix          of (int array * (string * inductive) array * int) * fix_decl
   | Lcofix        of int * fix_decl
-  | Lmakeblock    of prefix * pconstructor * int * lambda array
-                  (* prefix, constructor Name.t, constructor tag, arguments *)
-        (* A fully applied constructor *)
-  | Lconstruct    of prefix * pconstructor (* prefix, constructor Name.t *)
-        (* A partially applied constructor *)
+  | Lint          of int (* a constant constructor *)
+  | Lmakeblock    of prefix * inductive * int * lambda array
+                  (* prefix, inductive name, constructor tag, arguments *)
+        (* A fully applied non-constant constructor *)
   | Luint         of Uint63.t
   | Lval          of Nativevalues.t
   | Lsort         of Sorts.t
@@ -51,7 +50,10 @@ type lambda =
   | Llazy
   | Lforce
 
-and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array
+and lam_branches =
+  { constant_branches : lambda array;
+    nonconstant_branches : (Name.t Context.binder_annot array * lambda) array;
+  }
 
 and fix_decl =  Name.t Context.binder_annot array * lambda array * lambda array
 
@@ -121,7 +123,7 @@ let get_const_prefix env c =
 let map_lam_with_binders g f n lam =
   match lam with
   | Lrel _ | Lvar _  | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Luint _
-  | Lconstruct _ | Llazy | Lforce | Lmeta _ -> lam
+  | Llazy | Lforce | Lmeta _ | Lint _ -> lam
   | Lprod(dom,codom) -> 
       let dom' = f n dom in
       let codom' = f n codom in
@@ -143,17 +145,26 @@ let map_lam_with_binders g f n lam =
   | Lprim(prefix,kn,op,args) ->
       let args' = Array.Smart.map (f n) args in
       if args == args' then lam else Lprim(prefix,kn,op,args')
-  | Lcase(annot,t,a,br) ->
-      let t' = f n t in
-      let a' = f n a in
-      let on_b b = 
-	let (cn,ids,body) = b in
-	let body' = 
-	  if Array.is_empty ids then f n body 
-	  else f (g (Array.length ids) n) body in
-	if body == body' then b else (cn,ids,body') in
-      let br' = Array.Smart.map on_b br in
-      if t == t' && a == a' && br == br' then lam else Lcase(annot,t',a',br')
+  | Lcase(annot,t,a,branches) ->
+    let const = branches.constant_branches in
+    let nonconst = branches.nonconstant_branches in
+    let t' = f n t in
+    let a' = f n a in
+    let const' = Array.Smart.map (f n) const in
+    let on_b b =
+      let (ids,body) = b in
+      let body' = f (g (Array.length ids) n) body in
+      if body == body' then b else (ids,body') in
+    let nonconst' = Array.Smart.map on_b nonconst in
+    let branches' =
+      if const == const' && nonconst == nonconst' then
+        branches
+      else
+        { constant_branches = const';
+          nonconstant_branches = nonconst' }
+    in
+    if t == t' && a == a' && branches == branches' then lam else
+      Lcase(annot,t',a',branches')
   | Lif(t,bt,bf) ->
       let t' = f n t in
       let bt' = f n bt in
@@ -222,7 +233,7 @@ let lam_subst_args subst args =
 let can_subst lam = 
   match lam with
   | Lrel _ | Lvar _ | Lconst _ | Lproj _ | Lval _ | Lsort _ | Lind _ | Llam _
-  | Lconstruct _ | Lmeta _ | Levar _ -> true
+  | Lmeta _ | Levar _ -> true
   | _ -> false
 
 let can_merge_if bt bf =
@@ -320,16 +331,13 @@ and reduce_lapp substf lids body substa largs =
 
 let is_value lc =
   match lc with
-  | Lval _ -> true
-  | Lmakeblock(_,_,_,args) when Array.is_empty args -> true
-  | Luint _ -> true
+  | Lval _ | Lint _ | Luint _ -> true
   | _ -> false
 
 let get_value lc =
   match lc with
   | Lval v -> v
-  | Lmakeblock(_,_,tag,args) when Array.is_empty args ->
-      Nativevalues.mk_int tag
+  | Lint tag -> Nativevalues.mk_int tag
   | Luint i -> Nativevalues.mk_uint i
   | _ -> raise Not_found
 
@@ -337,14 +345,30 @@ let make_args start _end =
   Array.init (start - _end + 1) (fun i -> Lrel (Anonymous, start - i))
     
 (* Translation of constructors *)	
+let expand_constructor prefix ind tag nparams arity =
+  let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *)
+  let ids = Array.make (nparams + arity) anon in
+  if Int.equal arity 0 then mkLlam ids (Lint tag)
+  else
+  let args = make_args arity 1 in
+  Llam(ids, Lmakeblock (prefix, ind, tag, args))
 
-let makeblock env cn u tag args =
-  if Array.for_all is_value args && Array.length args > 0 then
+(* [nparams] is the number of parameters still expected *)
+let makeblock env ind tag nparams arity args =
+  let nargs = Array.length args in
+  if nparams > 0 || nargs < arity then
+    let prefix = get_mind_prefix env (fst ind) in
+    mkLapp (expand_constructor prefix ind tag nparams arity) args
+  else
+  (* The constructor is fully applied *)
+  if Int.equal arity 0 then Lint tag
+  else
+  if Array.for_all is_value args then
     let args = Array.map get_value args in
     Lval (Nativevalues.mk_block tag args)
   else
-    let prefix = get_mind_prefix env (fst (fst cn)) in
-    Lmakeblock(prefix, (cn,u), tag, args)
+    let prefix = get_mind_prefix env (fst ind) in
+    Lmakeblock(prefix, ind, tag, args)
 
 (* Translation of constants *)
 
@@ -420,8 +444,6 @@ let empty_evars =
   { evars_val = (fun _ -> None);
     evars_metas = (fun _ -> assert false) }
 
-let empty_ids = [||]
-
 (** Extract the inductive type over which a fixpoint is decreasing *)
 let rec get_fix_struct env i t = match kind (Reduction.whd_all env t) with
 | Prod (na, dom, t) ->
@@ -492,43 +514,51 @@ let rec lambda_of_constr cache env sigma c =
     let prefix = get_mind_prefix env (fst ind) in
     mkLapp (Lproj (prefix, ind, Projection.arg p)) [|lambda_of_constr cache env sigma c|]
 
-  | Case(ci,t,a,branches) ->  
-      let (mind,i as ind) = ci.ci_ind in
-      let mib = lookup_mind mind env in
-      let oib = mib.mind_packets.(i) in
-      let tbl = oib.mind_reloc_tbl in 
-      (* Building info *)
-      let prefix = get_mind_prefix env mind in
-      let annot_sw = 
-	    { asw_ind = ind;
-          asw_ci = ci;
-          asw_reloc = tbl; 
-          asw_finite = mib.mind_finite <> CoFinite;
-          asw_prefix = prefix}
-      in
-      (* translation of the argument *)
-      let la = lambda_of_constr cache env sigma a in
-      (* translation of the type *)
-      let lt = lambda_of_constr cache env sigma t in
-      (* translation of branches *)
-      let mk_branch i b =
-	let cn = (ind,i+1) in
-	let _, arity = tbl.(i) in
-        let b = lambda_of_constr cache env sigma b in
-	if Int.equal arity 0 then (cn, empty_ids, b)
-	else 
-	  match b with
-	  | Llam(ids, body) when Int.equal (Array.length ids) arity -> (cn, ids, body)
+  | Case(ci,t,a,branches) ->
+    let (mind,i as ind) = ci.ci_ind in
+    let mib = lookup_mind mind env in
+    let oib = mib.mind_packets.(i) in
+    let tbl = oib.mind_reloc_tbl in
+    (* Building info *)
+    let prefix = get_mind_prefix env mind in
+    let annot_sw =
+      { asw_ind = ind;
+        asw_ci = ci;
+        asw_reloc = tbl;
+        asw_finite = mib.mind_finite <> CoFinite;
+        asw_prefix = prefix}
+    in
+    (* translation of the argument *)
+    let la = lambda_of_constr cache env sigma a in
+    (* translation of the type *)
+    let lt = lambda_of_constr cache env sigma t in
+    (* translation of branches *)
+    let dummy = Lrel(Anonymous,0) in
+    let consts = Array.make oib.mind_nb_constant dummy in
+    let blocks = Array.make oib.mind_nb_args ([||],dummy) in
+    let rtbl = oib.mind_reloc_tbl in
+    for i = 0 to Array.length rtbl - 1 do
+      let tag, arity = rtbl.(i) in
+      let b = lambda_of_constr cache env sigma branches.(i) in
+      if arity = 0 then consts.(tag) <- b
+      else
+        let b =
+          match b with
+          | Llam(ids, body) when Array.length ids = arity -> (ids, body)
           | _ ->
-              (** TODO relevance *)
-              let anon = Context.make_annot Anonymous Sorts.Relevant in
-              let ids = Array.make arity anon in
-	      let args = make_args arity 1 in
-	      let ll = lam_lift arity b in
-	      (cn, ids, mkLapp  ll args) in
-      let bs = Array.mapi mk_branch branches in
-      Lcase(annot_sw, lt, la, bs)
-	
+            let anon = Context.make_annot Anonymous Sorts.Relevant in (* TODO relevance *)
+            let ids = Array.make arity anon in
+            let args = make_args arity 1 in
+            let ll = lam_lift arity b in
+            (ids, mkLapp  ll args)
+        in blocks.(tag-1) <- b
+    done;
+    let branches =
+      { constant_branches = consts;
+        nonconstant_branches = blocks }
+    in
+    Lcase(annot_sw, lt, la, branches)
+
   | Fix((pos, i), (names,type_bodies,rec_bodies)) ->
       let ltypes = lambda_of_args cache env sigma 0 type_bodies in
       let map i t =
@@ -572,17 +602,13 @@ and lambda_of_app cache env sigma f args =
           let prefix = get_const_prefix env kn in
           mkLapp (Lconst (prefix, (kn,u))) (lambda_of_args cache env sigma 0 args)
       end
-  | Construct (c,u) ->
-      let tag, nparams, arity = Cache.get_construct_info cache env c in
-      let expected = nparams + arity in
-      let nargs = Array.length args in
-      let prefix = get_mind_prefix env (fst (fst c)) in
-      if Int.equal nargs expected then 
-          let args = lambda_of_args cache env sigma nparams args in
-          makeblock env c u tag args
-      else
-        let args = lambda_of_args cache env sigma 0 args in
-            mkLapp (Lconstruct (prefix, (c,u))) args
+  | Construct ((ind,_ as c),_) ->
+    let tag, nparams, arity = Cache.get_construct_info cache env c in
+    let nargs = Array.length args in
+    if nparams < nargs then (* got all parameters *)
+      let args = lambda_of_args cache env sigma nparams args in
+      makeblock env ind tag 0 arity args
+    else makeblock env ind tag (nparams - nargs) arity empty_args
   | _ -> 
       let f = lambda_of_constr cache env sigma f in
       let args = lambda_of_args cache env sigma 0 args in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index b0de257a27..446df1a1ea 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -33,11 +33,10 @@ type lambda =
   | Lif           of lambda * lambda * lambda
   | Lfix          of (int array * (string * inductive) array * int) * fix_decl
   | Lcofix        of int * fix_decl
-  | Lmakeblock    of prefix * pconstructor * int * lambda array
-                  (* prefix, constructor Name.t, constructor tag, arguments *)
-        (* A fully applied constructor *)
-  | Lconstruct    of prefix * pconstructor (* prefix, constructor Name.t *)
-        (* A partially applied constructor *)
+  | Lint          of int (* a constant constructor *)
+  | Lmakeblock    of prefix * inductive * int * lambda array
+                  (* prefix, inductive name, constructor tag, arguments *)
+        (* A fully applied non-constant constructor *)
   | Luint         of Uint63.t
   | Lval          of Nativevalues.t
   | Lsort         of Sorts.t
@@ -45,7 +44,10 @@ type lambda =
   | Llazy
   | Lforce
 
-and lam_branches = (constructor * Name.t Context.binder_annot array * lambda) array
+and lam_branches =
+  { constant_branches : lambda array;
+    nonconstant_branches : (Name.t Context.binder_annot array * lambda) array;
+  }
 
 and fix_decl =  Name.t Context.binder_annot array * lambda array * lambda array
 
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 833e4082f0..43c9676f05 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -56,14 +56,15 @@ let write_ml_code fn ?(header=[]) code =
   List.iter (pp_global fmt) (header@code);
   close_out ch_out
 
-let warn_native_compiler_failed =
-  let print = function
+let error_native_compiler_failed e =
+  let msg = match e with
+  | Inl (Unix.WEXITED 127) -> Pp.(strbrk "The OCaml compiler was not found. Make sure it is installed, together with findlib.")
   | Inl (Unix.WEXITED n) -> Pp.(strbrk "Native compiler exited with status" ++ str" " ++ int n)
   | Inl (Unix.WSIGNALED n) -> Pp.(strbrk "Native compiler killed by signal" ++ str" " ++ int n)
   | Inl (Unix.WSTOPPED n) -> Pp.(strbrk "Native compiler stopped by signal" ++ str" " ++ int n)
   | Inr e -> Pp.(strbrk "Native compiler failed with error: " ++ strbrk (Unix.error_message e))
   in
-  CWarnings.create ~name:"native-compiler-failed" ~category:"native-compiler" print
+  CErrors.user_err msg
 
 let call_compiler ?profile:(profile=false) ml_filename =
   let load_path = !get_load_paths () in
@@ -100,15 +101,12 @@ let call_compiler ?profile:(profile=false) ml_filename =
   if !Flags.debug then Feedback.msg_debug (Pp.str (Envars.ocamlfind () ^ " " ^ (String.concat " " args)));
   try
     let res = CUnix.sys_command (Envars.ocamlfind ()) args in
-    let res = match res with
-      | Unix.WEXITED 0 -> true
-      | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
-        warn_native_compiler_failed (Inl res); false
-    in
-    res, link_filename
+    match res with
+    | Unix.WEXITED 0 -> link_filename
+    | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n ->
+      error_native_compiler_failed (Inl res)
   with Unix.Unix_error (e,_,_) ->
-    warn_native_compiler_failed (Inr e);
-    false, link_filename
+    error_native_compiler_failed (Inr e)
 
 let compile fn code ~profile:profile =
   write_ml_code fn code;
@@ -128,9 +126,8 @@ let compile_library dir code fn =
   in
   let fn = dirname / basename in
   write_ml_code fn ~header code;
-  let r = fst (call_compiler fn) in
-  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn;
-  r
+  let _ = call_compiler fn in
+  if (not !Flags.debug) && Sys.file_exists fn then Sys.remove fn
 
 (* call_linker links dynamically the code for constants in environment or a  *)
 (* conversion test. *)
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 25adcf224b..e113350368 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -21,9 +21,14 @@ val load_obj : (string -> unit) ref
 
 val get_ml_filename : unit -> string * string
 
-val compile : string -> global list -> profile:bool -> bool * string
-
-val compile_library : Names.DirPath.t -> global list -> string -> bool
+(** [compile file code ~profile] will compile native [code] to [file],
+   and return the name of the object file; this name depends on
+   whether are in byte mode or not; file is expected to be .ml file *)
+val compile : string -> global list -> profile:bool -> string
+
+(** [compile_library lib code file] is similar to [compile file code]
+   but will perform some extra tweaks to handle [code] as a Coq lib. *)
+val compile_library : Names.DirPath.t -> global list -> string -> unit
 
 val call_linker :
   ?fatal:bool -> string -> string -> code_location_updates option -> unit