Imported Upstream version 8.5~beta3+dfsg

67 files changed, 2052 insertions, 1371 deletions

diff --git a/kernel/byterun/coq_fix_code.c b/kernel/byterun/coq_fix_code.c
index 1be3e651..29e33d34 100644
--- a/kernel/byterun/coq_fix_code.c
+++ b/kernel/byterun/coq_fix_code.c
@@ -60,7 +60,7 @@ void init_arity () {
     arity[BRANCH]=arity[ISCONST]= 1;
   /* instruction with two operands */
   arity[APPTERM]=arity[MAKEBLOCK]=arity[CLOSURE]=
-  arity[ARECONST]=2;
+  arity[ARECONST]=arity[PROJ]=2;
   /* instruction with four operands */ 
   arity[MAKESWITCHBLOCK]=4;
   /* instruction with arbitrary operands */
diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h
index c7b18b90..f0627586 100644
--- a/kernel/byterun/coq_gc.h
+++ b/kernel/byterun/coq_gc.h
@@ -12,6 +12,7 @@
 #define _COQ_CAML_GC_
 #include <caml/mlvalues.h>
 #include <caml/alloc.h>
+#include <caml/memory.h>
 
 typedef void (*scanning_action) (value, value *);
 
@@ -24,12 +25,22 @@ CAMLextern void minor_collection (void);
 #define Caml_white (0 << 8)
 #define Caml_black (3 << 8)
 
+#ifdef HAS_OCP_MEMPROF
+
+/*  This code is necessary to make the OCamlPro memory profiling branch of
+    OCaml compile. */
+
+#define Make_header(wosize, tag, color)                                 \
+  caml_make_header(wosize, tag, color)
+
+#else
+
 #define Make_header(wosize, tag, color)                                 \
   (((header_t) (((header_t) (wosize) << 10)                             \
 		+ (color)                                               \
 		+ (tag_t) (tag)))   					\
    )
-
+#endif
 
 #define Alloc_small(result, wosize, tag) do{                            \
   young_ptr -= Bhsize_wosize (wosize);                                  \
diff --git a/kernel/byterun/coq_instruct.h b/kernel/byterun/coq_instruct.h
index 9cbf4077..8c5ab0ec 100644
--- a/kernel/byterun/coq_instruct.h
+++ b/kernel/byterun/coq_instruct.h
@@ -36,6 +36,7 @@ enum instructions {
   SWITCH, PUSHFIELDS, 
   GETFIELD0, GETFIELD1, GETFIELD, 
   SETFIELD0, SETFIELD1, SETFIELD,
+  PROJ,
   CONST0, CONST1, CONST2, CONST3, CONSTINT,
   PUSHCONST0, PUSHCONST1, PUSHCONST2, PUSHCONST3, PUSHCONSTINT,
   ACCUMULATE,
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0ab9f89f..dc571699 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -77,9 +77,11 @@ sp is a local copy of the global variable extern_sp. */
 #ifdef _COQ_DEBUG_ 
 #   define print_instr(s) /*if (drawinstr)*/ printf("%s\n",s)
 #   define print_int(i)   /*if (drawinstr)*/ printf("%d\n",i)
+#   define print_lint(i)  /*if (drawinstr)*/ printf("%ld\n",i)
 # else 
 #   define print_instr(s) 
 #   define print_int(i) 
+#   define print_lint(i)
 #endif
 
 /* GC interface */
@@ -339,6 +341,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(ENVACC){
 	print_instr("ENVACC");
+	print_int(*pc);
 	accu = Field(coq_env, *pc++);
         Next;
       }
@@ -369,6 +372,10 @@ value coq_interprete
 	sp[1] = (value)pc;
 	sp[2] = coq_env;
 	sp[3] = Val_long(coq_extra_args);
+	print_instr("call stack=");
+	print_lint(sp[1]);
+	print_lint(sp[2]);
+	print_lint(sp[3]);
 	pc = Code_val(accu);
 	coq_env = accu;
 	coq_extra_args = 0;
@@ -456,6 +463,7 @@ value coq_interprete
 	sp[0] = arg1;
 	sp[1] = arg2;
 	pc = Code_val(accu);
+	print_lint(accu);
 	coq_env = accu;
 	coq_extra_args += 1;
 	goto check_stacks;
@@ -479,11 +487,18 @@ value coq_interprete
 	print_instr("RETURN");
 	print_int(*pc);
 	sp += *pc++;
+	print_instr("stack=");
+	print_lint(sp[0]);
+	print_lint(sp[1]);
+	print_lint(sp[2]);
 	if (coq_extra_args > 0) {
+	  print_instr("extra args > 0");
+	  print_lint(coq_extra_args);
 	  coq_extra_args--;
 	  pc = Code_val(accu);
 	  coq_env = accu;
 	} else {
+	  print_instr("extra args = 0");
 	  pc = (code_t)(sp[0]);
 	  coq_env = sp[1];
 	  coq_extra_args = Long_val(sp[2]);
@@ -583,7 +598,10 @@ value coq_interprete
 	Alloc_small(accu, 1 + nvars, Closure_tag);
 	Code_val(accu) = pc + *pc;
 	pc++;
-	for (i = 0; i < nvars; i++) Field(accu, i + 1) = sp[i];
+	for (i = 0; i < nvars; i++) {
+	  print_lint(sp[i]);
+	  Field(accu, i + 1) = sp[i];
+	}
 	sp += nvars;
 	Next;
       }
@@ -718,6 +736,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(GETGLOBAL){
 	print_instr("GETGLOBAL");
+	print_int(*pc);
 	accu = Field(coq_global_data, *pc);
         pc++;
         Next;
@@ -730,7 +749,7 @@ value coq_interprete
 	tag_t tag = *pc++;
 	mlsize_t i;
 	value block;
-	print_instr("MAKEBLOCK");
+	print_instr("MAKEBLOCK, tag=");
 	Alloc_small(block, wosize, tag);
 	Field(block, 0) = accu;
 	for (i = 1; i < wosize; i++) Field(block, i) = *sp++;
@@ -741,7 +760,8 @@ value coq_interprete
 	
 	tag_t tag = *pc++;
 	value block;
-	print_instr("MAKEBLOCK1");
+	print_instr("MAKEBLOCK1, tag=");
+	print_int(tag);
 	Alloc_small(block, 1, tag);
 	Field(block, 0) = accu;
 	accu = block;
@@ -751,7 +771,8 @@ value coq_interprete
 	
 	tag_t tag = *pc++;
 	value block;
-	print_instr("MAKEBLOCK2");
+	print_instr("MAKEBLOCK2, tag=");
+	print_int(tag);
 	Alloc_small(block, 2, tag);
 	Field(block, 0) = accu;
 	Field(block, 1) = sp[0];
@@ -762,7 +783,8 @@ value coq_interprete
       Instruct(MAKEBLOCK3) {
 	tag_t tag = *pc++;
 	value block;
-	print_instr("MAKEBLOCK3");
+	print_instr("MAKEBLOCK3, tag=");
+	print_int(tag);
 	Alloc_small(block, 3, tag);
 	Field(block, 0) = accu;
 	Field(block, 1) = sp[0];
@@ -774,7 +796,8 @@ value coq_interprete
       Instruct(MAKEBLOCK4) {
 	tag_t tag = *pc++;
 	value block;
-	print_instr("MAKEBLOCK4");
+	print_instr("MAKEBLOCK4, tag=");
+	print_int(tag);
 	Alloc_small(block, 4, tag);
 	Field(block, 0) = accu;
 	Field(block, 1) = sp[0];
@@ -795,12 +818,12 @@ value coq_interprete
 	if (Is_block(accu)) {
 	  long index = Tag_val(accu);
 	  print_instr("block");
-	  print_int(index);
+	  print_lint(index);
 	  pc += pc[(sizes & 0xFFFFFF) + index];
 	} else {
 	  long index = Long_val(accu);
 	  print_instr("constant");
-	  print_int(index);
+	  print_lint(index);
 	  pc += pc[index];
 	}
 	  Next;
@@ -842,7 +865,6 @@ value coq_interprete
       }
 	
       Instruct(SETFIELD1){
-        int i, j, size, size_aux;
 	print_instr("SETFIELD1");
 	caml_modify(&Field(accu, 1),*sp);
        	sp++;
@@ -876,8 +898,30 @@ value coq_interprete
 	caml_modify(&Field(accu, *pc),*sp);
 	sp++; pc++;
 	Next;
-      }	
-   
+      }
+
+
+      Instruct(PROJ){
+	print_instr("PROJ");
+	if (Is_accu (accu)) {
+          value block;
+	  /* Skip over the index of projected field */
+	  pc++;
+	  /* Create atom */
+	  Alloc_small(block, 2, ATOM_PROJ_TAG);
+	  Field(block, 0) = Field(coq_global_data, *pc);
+	  Field(block, 1) = accu;
+	  /* Create accumulator */
+	  Alloc_small(accu, 2, Accu_tag);
+	  Code_val(accu) = accumulate;
+	  Field(accu, 1) = block;
+	} else {
+	    accu = Field(accu, *pc++);
+	}
+	pc++;
+	Next;
+      }
+
 /* Integer constants */
 
       Instruct(CONST0){
@@ -917,6 +961,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(CONSTINT) {
 	print_instr("CONSTINT");
+	print_int(*pc);
 	accu = Val_int(*pc);
 	pc++;
 	Next;
@@ -957,7 +1002,7 @@ value coq_interprete
 	    sp -= nargs;
 	    for (i = 0; i < nargs; i++) sp[i] = Field(accu, i + 2);
 	    *--sp = accu;
-	    print_int(nargs);
+	    print_lint(nargs);
 	    coq_extra_args = nargs;
 	    pc = Code_val(coq_env);
 	    goto check_stacks;
@@ -1084,7 +1129,6 @@ value coq_interprete
 	/* returns the sum plus one with a carry */
 	uint32_t s;
 	s = (uint32_t)accu + (uint32_t)*sp++ + 1;
-	value block;
         if( (uint32_t)s <= (uint32_t)accu ) {
           /* carry */
 	  Alloc_small(accu, 1, 2); /* ( _ , arity, tag ) */
@@ -1226,16 +1270,17 @@ value coq_interprete
         shiftby = uint32_of_value(accu);
         if (shiftby > 31) {
           if (shiftby < 62) {
-            *sp++;
-	    accu = (value)((((*sp++)^1) << (shiftby - 31)) | 1);
+            sp++;
+	    accu = (value)(((((uint32_t)*sp++)^1) << (shiftby - 31)) | 1);
           }
           else {
+            sp+=2;
             accu = (value)(1);
           }
 	}
         else{
         /* *sp = 2*x+1 --> accu = 2^(shiftby+1)*x */
-        accu = (value)(((*sp++)^1) << shiftby);
+	  accu = (value)((((uint32_t)*sp++)^1) << shiftby);
         /* accu = 2^(shiftby+1)*x --> 2^(shifby+1)*x+2*y/2^(31-shiftby)+1 */
         accu = (value)((accu | (((uint32_t)(*sp++)) >> (31-shiftby)))|1);
 	}
@@ -1244,7 +1289,7 @@ value coq_interprete
 
       Instruct (COMPAREINT31) {
 	/* returns Eq if equal, Lt if accu is less than *sp, Gt otherwise */
-	/* assumes Inudctive _ : _ := Eq | Lt | Gt */
+	/* assumes Inductive _ : _ := Eq | Lt | Gt */
 	print_instr("COMPAREINT31");
 	if ((uint32_t)accu == (uint32_t)*sp) {
 	  accu = 1;  /* 2*0+1 */
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index 8d03829a..c9bcdc32 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -26,7 +26,6 @@ asize_t coq_max_stack_size = Coq_max_stack_size;
 
 
 value coq_global_data;
-int coq_all_transp;
 value coq_atom_tbl;
 
 int drawinstr;
@@ -104,7 +103,6 @@ static int coq_vm_initialized = 0;
 
 value init_coq_vm(value unit) /* ML */
 {
-  int i;
   if (coq_vm_initialized == 1) {
     fprintf(stderr,"already open \n");fflush(stderr);}
   else {
@@ -117,7 +115,6 @@ value init_coq_vm(value unit) /* ML */
     init_coq_global_data(Coq_global_data_Size);
     init_coq_atom_tbl(40);
     /* Initialing the interpreter */
-    coq_all_transp = 0;
     init_coq_interpreter();
     
     /* Some predefined pointer code */
@@ -137,7 +134,6 @@ void realloc_coq_stack(asize_t required_space)
 {
   asize_t size;
   value * new_low, * new_high, * new_sp;
-  value * p;
   size = coq_stack_high - coq_stack_low;
   do {
     size *= 2;
@@ -207,18 +203,6 @@ value realloc_coq_atom_tbl(value size)            /* ML */
   return Val_unit;
 }
 
-
-value coq_set_transp_value(value transp)
-{
-  coq_all_transp = (transp == Val_true);
-  return Val_unit;
-}
-
-value get_coq_transp_value(value unit)
-{
-  return Val_bool(coq_all_transp);
-}
-
 value coq_set_drawinstr(value unit)
 {
   drawinstr = 1;
diff --git a/kernel/byterun/coq_values.c b/kernel/byterun/coq_values.c
index 007f61b2..528babeb 100644
--- a/kernel/byterun/coq_values.c
+++ b/kernel/byterun/coq_values.c
@@ -21,7 +21,6 @@
 
 value coq_kind_of_closure(value v) {
   opcode_t * c;
-  int res;
   int is_app = 0;
   c = Code_val(v);
   if (Is_instruction(c, GRAB)) return Val_int(0);
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 1bf493e2..bb0f0eb5 100644
--- a/kernel/byterun/coq_values.h
+++ b/kernel/byterun/coq_values.h
@@ -17,22 +17,17 @@
 #define Default_tag 0
 #define Accu_tag 0
 
-
-
 #define ATOM_ID_TAG 0
-#define ATOM_IDDEF_TAG 1
-#define ATOM_INDUCTIVE_TAG 2
-#define ATOM_FIX_TAG 3
-#define ATOM_SWITCH_TAG 4
-#define ATOM_COFIX_TAG 5
-#define ATOM_COFIXEVALUATED_TAG 6
-
-
+#define ATOM_INDUCTIVE_TAG 1
+#define ATOM_TYPE_TAG 2
+#define ATOM_PROJ_TAG 3
+#define ATOM_FIX_TAG 4
+#define ATOM_SWITCH_TAG 5
+#define ATOM_COFIX_TAG 6
+#define ATOM_COFIXEVALUATED_TAG 7
 
 /* Les blocs accumulate */
 #define Is_accu(v) (Is_block(v) && (Tag_val(v) == Accu_tag))
 
 #define IS_EVALUATED_COFIX(v) (Is_accu(v) && Is_block(Field(v,1)) && (Tag_val(Field(v,1)) == ATOM_COFIXEVALUATED_TAG))
 #endif /* _COQ_VALUES_ */
-
-
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 700de502..0a24a75d 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -17,23 +17,28 @@ open Term
 
 type tag = int
 
-let id_tag = 0
-let iddef_tag = 1
-let ind_tag = 2
-let fix_tag = 3
-let switch_tag = 4
-let cofix_tag = 5
-let cofix_evaluated_tag = 6
-(* It could be greate if OCaml export this value,
-   So fixme if this occur in a new version of OCaml *)
+let accu_tag = 0
+
+let type_atom_tag = 2
+let max_atom_tag = 2
+let proj_tag = 3
+let fix_app_tag = 4
+let switch_tag = 5
+let cofix_tag = 6
+let cofix_evaluated_tag = 7
+
+(* It would be great if OCaml exported this value,
+   So fixme if this happens in a new version of OCaml *)
 let last_variant_tag = 245 
 
 type structured_constant =
   | Const_sorts of sorts
-  | Const_ind of pinductive
+  | Const_ind of inductive
+  | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
-
+  | Const_univ_level of Univ.universe_level
+  | Const_type of Univ.universe
 
 type reloc_table = (tag * int) array
 
@@ -58,29 +63,30 @@ type instruction =
   | Kpush
   | Kpop of int
   | Kpush_retaddr of Label.t
-  | Kapply of int                       (*  number of arguments *)
-  | Kappterm of int * int               (* number of arguments, slot size *)
-  | Kreturn of int                      (* slot size *)
+  | Kapply of int
+  | Kappterm of int * int
+  | Kreturn of int
   | Kjump
   | Krestart
-  | Kgrab of int                        (* number of arguments *)
-  | Kgrabrec of int                     (* rec arg *)
-  | Kclosure of Label.t * int           (* label, number of free variables *)
+  | Kgrab of int
+  | Kgrabrec of int
+  | Kclosure of Label.t * int
   | Kclosurerec of int * int * Label.t array * Label.t array
-                   (* nb fv, init, lbl types, lbl bodies *)
   | Kclosurecofix of int * int * Label.t array * Label.t array
                    (* nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal of pconstant
+  | Kgetglobal of constant
   | Kconst of structured_constant
-  | Kmakeblock of int * tag             (* size, tag *)
+  | Kmakeblock of int * tag
   | Kmakeprod
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
-  | Kswitch of Label.t array * Label.t array (* consts,blocks *)
+  | Kswitch of Label.t array * Label.t array
   | Kpushfields of int
   | Kfield of int
   | Ksetfield of int
   | Kstop
   | Ksequence of bytecodes * bytecodes
+  | Kproj of int * Constant.t  (* index of the projected argument,
+                                           name of projection *)
 (* spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (* jump to label *)
   | Kaddint31                           (* adds the int31 in the accu
@@ -124,7 +130,10 @@ type instruction =
 
 and bytecodes = instruction list
 
-type fv_elem = FVnamed of Id.t | FVrel of int
+type fv_elem =
+  | FVnamed of Id.t
+  | FVrel of int
+  | FVuniv_var of int
 
 type fv = fv_elem array
 
@@ -142,105 +151,138 @@ type vm_env = {
 
 
 type comp_env = {
-    nb_stack : int;              (* nbre de variables sur la pile          *)
-    in_stack : int list;         (* position dans la pile                  *)
-    nb_rec : int;                (* nbre de fonctions mutuellement         *)
-                                 (* recursives =  nbr                      *)
+    nb_uni_stack : int ;         (* number of universes on the stack,      *)
+                                 (* universes are always at the bottom.    *)
+    nb_stack : int;              (* number of variables on the stack       *)
+    in_stack : int list;         (* position in the stack                  *)
+    nb_rec : int;                (* number of mutually recursive functions *)
     pos_rec  : instruction list; (* instruction d'acces pour les variables *)
                                  (*  de point fix ou de cofix              *)
     offset : int;
-    in_env : vm_env ref
+    in_env : vm_env ref          (* The free variables of the expression   *)
   }
 
+(* --- Pretty print *)
+open Pp
+open Util
 
+let pp_sort s =
+  match family_of_sort s with
+  | InSet -> str "Set"
+  | InProp -> str "Prop"
+  | InType -> str "Type"
 
-(* --- Pretty print *)
-open Format
-let rec instruction ppf = function
-  | Klabel lbl -> fprintf ppf "L%i:" lbl
-  | Kacc n -> fprintf ppf "\tacc %i" n
-  | Kenvacc n -> fprintf ppf "\tenvacc %i" n
-  | Koffsetclosure n -> fprintf ppf "\toffsetclosure %i" n
-  | Kpush -> fprintf ppf "\tpush"
-  | Kpop n -> fprintf ppf "\tpop %i" n
-  | Kpush_retaddr lbl -> fprintf ppf "\tpush_retaddr L%i" lbl
-  | Kapply n -> fprintf ppf "\tapply %i" n
+let rec pp_struct_const = function
+  | Const_sorts s -> pp_sort s
+  | Const_ind (mind, i) -> pr_mind mind ++ str"#" ++ int i
+  | Const_proj p -> Constant.print p
+  | Const_b0 i -> int i
+  | Const_bn (i,t) ->
+     int i ++ surround (prvect_with_sep pr_comma pp_struct_const t)
+  | Const_univ_level l -> Univ.Level.pr l
+  | Const_type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}"
+
+let pp_lbl lbl = str "L" ++ int lbl
+
+let pp_pcon (id,u) =
+  pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}"
+
+let pp_fv_elem = function
+  | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")"
+  | FVrel i -> str "Rel(" ++ int i ++ str ")"
+  | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")"
+
+let rec pp_instr i =
+  match i with
+  | Klabel _   | Ksequence _ -> assert false
+  | Kacc n -> str "acc " ++ int n
+  | Kenvacc n -> str "envacc " ++ int n
+  | Koffsetclosure n -> str "offsetclosure " ++ int n
+  | Kpush -> str "push"
+  | Kpop n -> str "pop " ++ int n
+  | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl
+  | Kapply n -> str "apply " ++ int n
   | Kappterm(n, m) ->
-      fprintf ppf "\tappterm %i, %i" n m
-  | Kreturn n -> fprintf ppf "\treturn %i" n
-  | Kjump -> fprintf ppf "\tjump"
-  | Krestart -> fprintf ppf "\trestart"
-  | Kgrab n -> fprintf ppf "\tgrab %i" n
-  | Kgrabrec n -> fprintf ppf "\tgrabrec %i" n
+      str "appterm " ++ int n ++ str ", " ++ int m
+  | Kreturn n -> str "return " ++ int n
+  | Kjump -> str "jump"
+  | Krestart -> str "restart"
+  | Kgrab n -> str "grab " ++ int n
+  | Kgrabrec n -> str "grabrec " ++ int n
   | Kclosure(lbl, n) ->
-      fprintf ppf "\tclosure L%i, %i" lbl n
+      str "closure " ++ pp_lbl lbl ++ str ", " ++ int n
   | Kclosurerec(fv,init,lblt,lblb) ->
-      fprintf ppf "\tclosurerec";
-      fprintf ppf "%i , %i, " fv init;
-      print_string "types = ";
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
-      print_string " bodies = ";
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
+      h 1 (str "closurerec " ++
+	     int fv ++ str ", " ++ int init ++
+	     str " types = " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
+	     str " bodies = " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
   | Kclosurecofix (fv,init,lblt,lblb) ->
-      fprintf ppf "\tclosurecofix";
-      fprintf ppf " %i , %i, " fv init;
-      print_string "types = ";
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt;
-      print_string " bodies = ";
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
-  | Kgetglobal (id,u) -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id)
-  | Kconst cst ->
-      fprintf ppf "\tconst"
+      h 1 (str "closurecofix " ++
+	     int fv ++ str ", " ++ int init ++
+	     str " types = " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
+	     str " bodies = " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
+  | Kgetglobal idu -> str "getglobal " ++ pr_con idu
+  | Kconst sc ->
+      str "const " ++ pp_struct_const sc
   | Kmakeblock(n, m) ->
-      fprintf ppf "\tmakeblock %i, %i" n m
-  | Kmakeprod -> fprintf ppf "\tmakeprod"
+      str "makeblock " ++ int n ++ str ", " ++ int m
+  | Kmakeprod -> str "makeprod"
   | Kmakeswitchblock(lblt,lbls,_,sz) ->
-      fprintf ppf "\tmakeswitchblock %i, %i, %i" lblt lbls sz
+      str "makeswitchblock " ++ pp_lbl lblt ++ str ", " ++
+	pp_lbl lbls ++ str ", " ++ int sz
   | Kswitch(lblc,lblb) ->
-      fprintf ppf "\tswitch";
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblc;
-      Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb;
-  | Kpushfields n -> fprintf ppf "\tpushfields %i" n
-  | Ksetfield n -> fprintf ppf "\tsetfield %i" n
-  | Kfield  n -> fprintf ppf "\tgetfield %i" n
-  | Kstop -> fprintf ppf "\tstop"
-  | Ksequence (c1,c2) ->
-      fprintf ppf "%a@ %a" instruction_list c1 instruction_list c2
-(* spiwack *)
-  | Kbranch lbl -> fprintf ppf "\tbranch %i" lbl
-  | Kaddint31 -> fprintf ppf "\taddint31"
-  | Kaddcint31 -> fprintf ppf "\taddcint31"
-  | Kaddcarrycint31 -> fprintf ppf "\taddcarrycint31"
-  | Ksubint31 -> fprintf ppf "\tsubint31"
-  | Ksubcint31 -> fprintf ppf "\tsubcint31"
-  | Ksubcarrycint31 -> fprintf ppf "\tsubcarrycint31"
-  | Kmulint31 -> fprintf ppf "\tmulint31"
-  | Kmulcint31 -> fprintf ppf "\tmulcint31"
-  | Kdiv21int31 -> fprintf ppf "\tdiv21int31"
-  | Kdivint31 -> fprintf ppf "\tdivint31"
-  | Kcompareint31 -> fprintf ppf "\tcompareint31"
-  | Khead0int31 -> fprintf ppf "\thead0int31"
-  | Ktail0int31 -> fprintf ppf "\ttail0int31"
-  | Kaddmuldivint31 -> fprintf ppf "\taddmuldivint31"
-  | Kisconst lbl -> fprintf ppf "\tisconst %i" lbl
-  | Kareconst(n,lbl) -> fprintf ppf "\tareconst %i %i" n lbl
-  | Kcompint31 -> fprintf ppf "\tcompint31"
-  | Kdecompint31 -> fprintf ppf "\tdecompint"
-  | Klorint31 -> fprintf ppf "\tlorint31"
-  | Klandint31 -> fprintf ppf "\tlandint31"
-  | Klxorint31 -> fprintf ppf "\tlxorint31"
+      h 1 (str "switch " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblc) ++
+	     str " | " ++
+	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
+  | Kpushfields n -> str "pushfields " ++ int n
+  | Kfield n -> str "field " ++ int n
+  | Ksetfield n -> str "set field" ++ int n
 
-(* /spiwack *)
+  | Kstop -> str "stop"
+
+  | Kbranch lbl -> str "branch " ++ pp_lbl lbl
 
+  | Kproj(n,p) -> str "proj " ++ int n ++ str " " ++ Constant.print p
 
-and instruction_list ppf = function
-    [] -> ()
-  | Klabel lbl :: il ->
-      fprintf ppf "L%i:%a" lbl instruction_list il
-  | instr :: il ->
-      fprintf ppf "%a@ %a" instruction instr instruction_list il
+  | Kaddint31 -> str "addint31"
+  | Kaddcint31 -> str "addcint31"
+  | Kaddcarrycint31 -> str "addcarrycint31"
+  | Ksubint31 -> str "subint31"
+  | Ksubcint31 -> str "subcint31"
+  | Ksubcarrycint31 -> str "subcarrycint31"
+  | Kmulint31 -> str "mulint31"
+  | Kmulcint31 -> str "mulcint31"
+  | Kdiv21int31 -> str "div21int31"
+  | Kdivint31 -> str "divint31"
+  | Kcompareint31 -> str "compareint31"
+  | Khead0int31 -> str "head0int31"
+  | Ktail0int31 -> str "tail0int31"
+  | Kaddmuldivint31 -> str "addmuldivint31"
+  | Kisconst lbl -> str "isconst " ++ int lbl
+  | Kareconst(n,lbl) -> str "areconst " ++ int n ++ spc () ++ int lbl
+  | Kcompint31 -> str "compint31"
+  | Kdecompint31 -> str "decompint"
+  | Klorint31 -> str "lorint31"
+  | Klandint31 -> str "landint31"
+  | Klxorint31 -> str "lxorint31"
 
 
+and pp_bytecodes c =
+  match c with
+  | [] -> str ""
+  | Klabel lbl :: c ->
+	str "L" ++ int lbl ++ str ":" ++ fnl () ++
+	pp_bytecodes c
+  | Ksequence (l1, l2) :: c ->
+      pp_bytecodes l1 ++ pp_bytecodes l2 ++  pp_bytecodes c
+  | i :: c ->
+      tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c
+
 (*spiwack: moved this type in this file  because I needed it for
   retroknowledge which can't depend from cbytegen *)
 type block =
@@ -253,8 +295,3 @@ type block =
                 (* spiwack: compilation given by a function *)
                 (* compilation function (see get_vm_constant_dynamic_info in
                    retroknowledge.mli for more info) , argument array  *)
-
-
-
-let draw_instr c =
-  fprintf std_formatter "@[<v 0>%a@]" instruction_list c
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index fbb40ffd..03ae6b9c 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -13,20 +13,28 @@ open Term
 
 type tag = int
 
-val id_tag : tag
-val iddef_tag : tag
-val ind_tag : tag
-val fix_tag : tag
+val accu_tag : tag
+
+val type_atom_tag : tag
+val max_atom_tag : tag
+val proj_tag : tag
+val fix_app_tag : tag
 val switch_tag : tag
 val cofix_tag : tag
 val cofix_evaluated_tag : tag
-val last_variant_tag : tag 
+
+val last_variant_tag : tag
 
 type structured_constant =
   | Const_sorts of sorts
-  | Const_ind of pinductive
+  | Const_ind of inductive
+  | Const_proj of Constant.t
   | Const_b0 of tag
   | Const_bn of tag * structured_constant array
+  | Const_univ_level of Univ.universe_level
+  | Const_type of Univ.universe
+
+val pp_struct_const : structured_constant -> Pp.std_ppcmds
 
 type reloc_table = (tag * int) array
 
@@ -43,13 +51,13 @@ module Label :
 
 type instruction =
   | Klabel of Label.t
-  | Kacc of int
-  | Kenvacc of int
-  | Koffsetclosure of int
-  | Kpush
-  | Kpop of int
-  | Kpush_retaddr of Label.t
-  | Kapply of int                       (**  number of arguments *)
+  | Kacc of int                         (** accu = sp[n] *)
+  | Kenvacc of int                      (** accu = coq_env[n] *)
+  | Koffsetclosure of int               (** accu = &coq_env[n] *)
+  | Kpush                               (** sp = accu :: sp *)
+  | Kpop of int                         (** sp = skipn n sp *)
+  | Kpush_retaddr of Label.t            (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *)
+  | Kapply of int                       (** number of arguments (arguments on top of stack) *)
   | Kappterm of int * int               (** number of arguments, slot size *)
   | Kreturn of int                      (** slot size *)
   | Kjump
@@ -61,17 +69,21 @@ type instruction =
                    (** nb fv, init, lbl types, lbl bodies *)
   | Kclosurecofix of int * int * Label.t array * Label.t array
                    (** nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal of pconstant
+  | Kgetglobal of constant
   | Kconst of structured_constant
-  | Kmakeblock of int * tag             (** size, tag *)
+  | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0
+                                         ** is accu, all others are popped from
+					 ** the top of the stack  *)
   | Kmakeprod
   | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
   | Kswitch of Label.t array * Label.t array (** consts,blocks *)
   | Kpushfields of int
-  | Kfield of int
-  | Ksetfield of int
+  | Kfield of int                       (** accu = accu[n] *)
+  | Ksetfield of int                    (** accu[n] = sp[0] ; sp = pop sp *)
   | Kstop
   | Ksequence of bytecodes * bytecodes
+  | Kproj of int * Constant.t  (** index of the projected argument,
+                                            name of projection *)
 
 (** spiwack: instructions concerning integers *)
   | Kbranch of Label.t                  (** jump to label, is it needed ? *)
@@ -115,7 +127,10 @@ type instruction =
 
 and bytecodes = instruction list
 
-type fv_elem = FVnamed of Id.t | FVrel of int
+type fv_elem =
+  FVnamed of Id.t
+| FVrel of int
+| FVuniv_var of int
 
 type fv = fv_elem array
 
@@ -124,28 +139,28 @@ type fv = fv_elem array
             closed terms. *)
 exception NotClosed
 
-(*spiwack: both type have been moved from Cbytegen because I needed then
+(*spiwack: both type have been moved from Cbytegen because I needed them
   for the retroknowledge *)
 type vm_env = {
-    size : int;              (** longueur de la liste [n] *)
+    size : int;              (** length of the list [n] *)
     fv_rev : fv_elem list    (** [fvn; ... ;fv1] *)
   }
 
 
 type comp_env = {
-    nb_stack : int;              (** nbre de variables sur la pile          *)
-    in_stack : int list;         (** position dans la pile                  *)
-    nb_rec : int;                (** nbre de fonctions mutuellement         *)
-                                 (** recursives =  nbr                      *)
+    nb_uni_stack : int ;         (** number of universes on the stack       *)
+    nb_stack : int;              (** number of variables on the stack       *)
+    in_stack : int list;         (** position in the stack                  *)
+    nb_rec : int;                (** number of mutually recursive functions *)
+                                 (** (= nbr)                                *)
     pos_rec  : instruction list; (** instruction d'acces pour les variables *)
                                  (**  de point fix ou de cofix              *)
     offset : int;
-    in_env : vm_env ref
+    in_env : vm_env ref          (** the variables that are accessed        *)
   }
 
-val draw_instr : bytecodes -> unit
-
-
+val pp_bytecodes : bytecodes -> Pp.std_ppcmds
+val pp_fv_elem : fv_elem -> Pp.std_ppcmds
 
 (*spiwack: moved this here because I needed it for retroknowledge *)
 type block =
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 07fab06a..1f7cc3c7 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -91,18 +91,20 @@ open Pre_env
 (* In Cfxe_t accumulators, we need to store [fcofixi] for testing         *)
 (* conversion of cofixpoints (which is intentional).                      *)
 
+type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t
 
 let empty_fv = { size= 0;  fv_rev = [] }
 
 let fv r = !(r.in_env)
 
-let empty_comp_env ()=
-  { nb_stack = 0;
+let empty_comp_env ?(univs=0) ()=
+  { nb_uni_stack = univs;
+    nb_stack = 0;
     in_stack = [];
     nb_rec = 0;
     pos_rec = [];
     offset = 0;
-    in_env = ref empty_fv;
+    in_env = ref empty_fv
   }
 
 (*i Creation functions for comp_env *)
@@ -110,8 +112,9 @@ let empty_comp_env ()=
 let rec add_param n sz l =
   if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l)
 
-let comp_env_fun arity =
-  { nb_stack = arity;
+let comp_env_fun ?(univs=0) arity =
+  { nb_uni_stack = univs ;
+    nb_stack = arity;
     in_stack = add_param arity 0 [];
     nb_rec = 0;
     pos_rec = [];
@@ -120,8 +123,9 @@ let comp_env_fun arity =
   }
 
 
-let comp_env_fix_type rfv =
-  { nb_stack = 0;
+let comp_env_fix_type  rfv =
+  { nb_uni_stack = 0;
+    nb_stack = 0;
     in_stack = [];
     nb_rec = 0;
     pos_rec = [];
@@ -134,7 +138,8 @@ let comp_env_fix ndef curr_pos arity rfv =
    for i = ndef downto 1 do
      prec := Koffsetclosure (2 * (ndef - curr_pos - i)) :: !prec
    done;
-   { nb_stack = arity;
+   { nb_uni_stack = 0;
+     nb_stack = arity;
      in_stack = add_param arity 0 [];
      nb_rec = ndef;
      pos_rec = !prec;
@@ -143,7 +148,8 @@ let comp_env_fix ndef curr_pos arity rfv =
    }
 
 let comp_env_cofix_type ndef rfv =
-  { nb_stack = 0;
+  { nb_uni_stack = 0;
+    nb_stack = 0;
     in_stack = [];
     nb_rec = 0;
     pos_rec = [];
@@ -156,7 +162,8 @@ let comp_env_cofix ndef arity rfv =
    for i = 1 to ndef do
      prec := Kenvacc i :: !prec
    done;
-   { nb_stack = arity;
+   { nb_uni_stack = 0;
+     nb_stack = arity;
      in_stack = add_param arity 0 [];
      nb_rec = ndef;
      pos_rec = !prec;
@@ -168,7 +175,7 @@ let comp_env_cofix ndef arity rfv =
 let push_param n sz r =
   { r with
     nb_stack = r.nb_stack + n;
-    in_stack = add_param n sz r.in_stack }
+    in_stack = add_param n (sz - r.nb_uni_stack) r.in_stack }
 
 (* [push_local sz r] add a new variable on the stack at position [sz] *)
 let push_local sz r =
@@ -176,8 +183,6 @@ let push_local sz r =
     nb_stack = r.nb_stack + 1;
     in_stack = (sz + 1) :: r.in_stack }
 
-
-
 (*i Compilation of variables *)
 let find_at f l =
   let rec aux n = function
@@ -214,6 +219,22 @@ let pos_rel i r sz =
 	r.in_env := { size = pos+1; fv_rev =  db:: env.fv_rev};
 	Kenvacc(r.offset + pos)
 
+let pos_universe_var i r sz =
+  if i < r.nb_uni_stack then
+    Kacc (sz - r.nb_stack - (r.nb_uni_stack - i))
+  else
+    let env = !(r.in_env) in
+    let f = function
+      | FVuniv_var u -> Int.equal i u
+      | _ -> false
+    in
+    try Kenvacc (r.offset + env.size - (find_at f env.fv_rev))
+    with Not_found ->
+      let pos = env.size in
+      let db = FVuniv_var i in
+      r.in_env := { size = pos + 1; fv_rev = db::env.fv_rev } ;
+      Kenvacc(r.offset + pos)
+
 (*i  Examination of the continuation *)
 
 (* Discard all instructions up to the next label.                        *)
@@ -459,8 +480,9 @@ let rec str_const c =
               end
 	| _ -> Bconstr c
       end
-  | Ind ind -> Bstrconst (Const_ind ind)
-  | Construct (((kn,j),i),u) ->  
+  | Ind (ind,u) when Univ.Instance.is_empty u ->
+    Bstrconst (Const_ind ind)
+  | Construct (((kn,j),i),_) ->
       begin
       (* spiwack: tries first to apply the run-time compilation
            behavior of the constructor, as in 2/ above *)
@@ -513,6 +535,7 @@ let compile_fv_elem reloc fv sz cont =
   match fv with
   | FVrel i -> pos_rel i reloc sz :: cont
   | FVnamed id -> pos_named id reloc :: cont
+  | FVuniv_var i -> pos_universe_var i reloc sz :: cont
 
 let rec compile_fv reloc l sz cont =
   match l with
@@ -524,39 +547,71 @@ let rec compile_fv reloc l sz cont =
 
 (* Compiling constants *)
 
-let rec get_allias env (kn,u as p) =
+let rec get_alias env kn =
   let cb = lookup_constant kn env in
   let tps = cb.const_body_code in
     match tps with
-    | None -> p
+    | None -> kn
     | Some tps ->
        (match Cemitcodes.force tps with
-	| BCallias (kn',u') -> get_allias env (kn', Univ.subst_instance_instance u u')
-	| _ -> p)
-
-(* Compiling expressions *)
+	| BCalias kn' -> get_alias env kn'
+	| _ -> kn)
 
+(* sz is the size of the local stack *)
 let rec compile_constr reloc c sz cont =
   match kind_of_term c with
   | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta"
   | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar"
-  | Proj (p,c) -> 
-    (* compile_const reloc p [|c|] sz cont *)
-    let kn = Projection.constant p in
-    let cb = lookup_constant kn !global_env in
-      (* TODO: better representation of projections *)
-    let pb = Option.get cb.const_proj in
-    let args = Array.make pb.proj_npars mkProp in
-      compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont
+  | Proj (p,c) ->
+     let kn = Projection.constant p in
+     let cb = lookup_constant kn !global_env in
+     let pb = Option.get cb.const_proj in
+     let n = pb.proj_arg in
+     compile_constr reloc c sz (Kproj (n,kn) :: cont)
 
   | Cast(c,_,_) -> compile_constr reloc c sz cont
 
   | Rel i -> pos_rel i reloc sz :: cont
   | Var id -> pos_named id reloc :: cont
   | Const (kn,u) -> compile_const reloc kn u [||] sz cont
-  | Sort _  | Ind _ | Construct _ ->
+  | Ind (ind,u) ->
+     let bcst = Bstrconst (Const_ind ind) in
+    if Univ.Instance.is_empty u then
+      compile_str_cst reloc bcst sz cont
+    else
+      comp_app compile_str_cst compile_universe reloc
+	   bcst
+	   (Univ.Instance.to_array u)
+	   sz
+	   cont
+  | Sort (Prop _) | Construct _ ->
       compile_str_cst reloc (str_const c) sz cont
-
+  | Sort (Type u) ->
+     (* We separate global and local universes in [u]. The former will be part
+        of the structured constant, while the later (if any) will be applied as
+        arguments. *)
+     let open Univ in begin
+      let levels = Universe.levels u in
+      let global_levels =
+	LSet.filter (fun x -> Level.var_index x = None) levels
+      in
+      let local_levels =
+	List.map_filter (fun x -> Level.var_index x)
+	  (LSet.elements levels)
+      in
+      (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *)
+      let uglob =
+	LSet.fold (fun lvl u -> Universe.sup u (Universe.make lvl)) global_levels Universe.type0m
+      in
+      if local_levels = [] then
+	compile_str_cst reloc (Bstrconst (Const_sorts (Type uglob))) sz cont
+      else
+	let compile_get_univ reloc idx sz cont =
+	  compile_fv_elem reloc (FVuniv_var idx) sz cont
+	in
+        comp_app compile_str_cst compile_get_univ reloc
+	  (Bstrconst (Const_type u)) (Array.of_list local_levels) sz cont
+    end
   | LetIn(_,xb,_,body) ->
       compile_constr reloc xb sz
 	(Kpush ::
@@ -665,7 +720,9 @@ let rec compile_constr reloc c sz cont =
       let lbl_sw = Label.create () in
       let sz_b,branch,is_tailcall =
 	match branch1 with
-	| Kreturn k -> assert (Int.equal k sz); sz, branch1, true
+	| Kreturn k ->
+	  assert (Int.equal k sz) ;
+	  sz, branch1, true
 	| _ -> sz+3, Kjump, false
       in
       let annot = {ci = ci; rtbl = tbl; tailcall = is_tailcall} in
@@ -747,8 +804,20 @@ and compile_str_cst reloc sc sz cont =
 
 (* spiwack : compilation of constants with their arguments.
    Makes a special treatment with 31-bit integer addition *)
-and compile_const =
-  fun reloc-> fun  kn u -> fun args -> fun sz -> fun cont ->
+and compile_get_global reloc (kn,u) sz cont =
+  let kn = get_alias !global_env kn in
+  if Univ.Instance.is_empty u then
+    Kgetglobal kn :: cont
+  else
+    comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
+      compile_universe reloc () (Univ.Instance.to_array u) sz cont
+
+and compile_universe reloc uni sz cont =
+  match Univ.Level.var_index uni with
+  | None -> Kconst (Const_univ_level uni) :: cont
+  | Some idx -> pos_universe_var idx reloc sz :: cont
+
+and compile_const reloc kn u args sz cont =
   let nargs = Array.length args in
   (* spiwack: checks if there is a specific way to compile the constant
               if there is not, Not_found is raised, and the function
@@ -758,30 +827,85 @@ and compile_const =
                   (mkConstU (kn,u)) reloc args sz cont
   with Not_found ->
     if Int.equal nargs 0 then
-      Kgetglobal (get_allias !global_env (kn, u)) :: cont
+      compile_get_global reloc (kn,u) sz cont
     else
-      comp_app (fun _ _ _ cont ->
-                   Kgetglobal (get_allias !global_env (kn,u)) :: cont)
-        compile_constr reloc () args sz cont
-
-let compile fail_on_error env c =
+      if Univ.Instance.is_empty u then
+        (* normal compilation *)
+        comp_app (fun _ _ sz cont ->
+            compile_get_global reloc (kn,u) sz cont)
+          compile_constr reloc () args sz cont
+      else
+        let compile_arg reloc constr_or_uni sz cont =
+          match constr_or_uni with
+          | ArgConstr cst -> compile_constr reloc cst sz cont
+          | ArgUniv uni -> compile_universe reloc uni sz cont
+        in
+	let u = Univ.Instance.to_array u in
+	let lu = Array.length u in
+	let all =
+	  Array.init (lu + Array.length args) 
+	    (fun i -> if i < lu then ArgUniv u.(i) else ArgConstr args.(i-lu))
+	in
+        comp_app (fun _ _ _ cont -> Kgetglobal kn :: cont)
+          compile_arg reloc () all sz cont
+
+let is_univ_copy max u =
+  let u = Univ.Instance.to_array u in
+  if Array.length u = max then
+    Array.fold_left_i (fun i acc u ->
+        if acc then
+          match Univ.Level.var_index u with
+          | None -> false
+          | Some l -> l = i
+        else false) true u
+  else
+    false
+
+let dump_bytecodes init code fvs =
+  let open Pp in
+    (str "code =" ++ fnl () ++
+     pp_bytecodes init ++ fnl () ++
+     pp_bytecodes code ++ fnl () ++
+     str "fv = " ++
+     prlist_with_sep (fun () -> str "; ") pp_fv_elem fvs ++
+     fnl ())
+
+let compile fail_on_error ?universes:(universes=0) env c =
   set_global_env env;
   init_fun_code ();
   Label.reset_label_counter ();
-  let reloc = empty_comp_env () in
-  try 
-    let init_code = compile_constr reloc c 0 [Kstop] in
+  let cont = [Kstop] in
+  try
+    let reloc, init_code =
+      if Int.equal universes 0 then
+        let reloc = empty_comp_env () in
+        reloc, compile_constr reloc c 0 cont
+      else
+        (* We are going to generate a lambda, but merge the universe closure
+         * with the function closure if it exists.
+         *)
+        let reloc = empty_comp_env () in
+        let arity , body =
+          match kind_of_term c with
+          | Lambda _ ->
+            let params, body = decompose_lam c in
+            List.length params , body
+          | _ -> 0 , c
+        in
+        let full_arity = arity + universes in
+        let r_fun = comp_env_fun ~univs:universes arity in
+        let lbl_fun = Label.create () in
+        let cont_fun =
+          compile_constr r_fun body full_arity [Kreturn full_arity]
+        in
+        fun_code := [Ksequence(add_grab full_arity lbl_fun cont_fun,!fun_code)];
+        let fv = fv r_fun in
+        reloc, compile_fv reloc fv.fv_rev 0 (Kclosure(lbl_fun,fv.size) :: cont)
+    in
     let fv = List.rev (!(reloc.in_env).fv_rev) in
-(*  draw_instr init_code;
-  draw_instr !fun_code;
-  Format.print_string "fv = ";
-  List.iter (fun v ->
-    match v with
-    | FVnamed id -> Format.print_string ((Id.to_string id)^"; ")
-    | FVrel i -> Format.print_string ((string_of_int i)^"; ")) fv;  Format
-    .print_string "\n";
-  Format.print_flush();  *)
-      Some (init_code,!fun_code, Array.of_list fv)
+    (if !Flags.dump_bytecode then
+      Pp.msg_debug (dump_bytecodes init_code !fun_code fv)) ;
+    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
@@ -789,28 +913,33 @@ let compile fail_on_error env c =
 	    Id.print tname ++ str str_max_constructors));
        None)
 
-let compile_constant_body fail_on_error env = function
+let compile_constant_body fail_on_error env univs = function
   | Undef _ | OpaqueDef _ -> Some BCconstant
   | Def sb ->
       let body = Mod_subst.force_constr sb in
+      let instance_size =
+        match univs with
+        | None -> 0
+        | Some univ -> Univ.UContext.size univ
+      in
       match kind_of_term body with
-	| Const (kn',u) ->
+	| Const (kn',u) when is_univ_copy instance_size u ->
 	    (* we use the canonical name of the constant*)
 	    let con= constant_of_kn (canonical_con kn') in
-	      Some (BCallias (get_allias env (con,u)))
+	      Some (BCalias (get_alias env con))
 	| _ ->
-	    let res = compile fail_on_error env body in
+	    let res = compile fail_on_error ~universes:instance_size env body in
 	      Option.map (fun x -> BCdefined (to_memory x)) res
 
 (* Shortcut of the previous function used during module strengthening *)
 
-let compile_alias (kn,u) = BCallias (constant_of_kn (canonical_con kn), u)
+let compile_alias kn = BCalias (constant_of_kn (canonical_con kn))
 
 (* spiwack: additional function which allow different part of compilation of the
       31-bit integers *)
 
 let make_areconst n else_lbl cont =
-  if n <=0 then
+  if n <= 0 then
     cont
   else
     Kareconst (n, else_lbl)::cont
@@ -867,7 +996,7 @@ let op2_compilation op =
          Kareconst(2, else_lbl):: Kacc 0:: Kpop 1::
           op:: Kreturn 0:: Klabel else_lbl::
          (* works as comp_app with nargs = 2 and tailcall cont [Kreturn 0]*)
-          (*Kgetglobal (get_allias !global_env kn):: *)
+          (*Kgetglobal (get_alias !global_env kn):: *)
           normal::
           Kappterm(2, 2):: [] (* = discard_dead_code [Kreturn 0] *)
      in
@@ -886,7 +1015,7 @@ let op2_compilation op =
            (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
            (op::escape::Klabel else_lbl::Kpush::
            (* works as comp_app with nargs = 2 and non-tailcall cont*)
-           (*Kgetglobal (get_allias !global_env kn):: *)
+           (*Kgetglobal (get_alias !global_env kn):: *)
            normal::
            Kapply 2::labeled_cont)))
   else if nargs=0 then
@@ -900,16 +1029,16 @@ let op2_compilation op =
   1/ checks if all the arguments are constants (i.e. non-block values)
   2/ if they are, uses the "op" instruction to execute
   3/ if at least one is not, branches to the normal behavior:
-      Kgetglobal (get_allias !global_env kn) *)
+      Kgetglobal (get_alias !global_env kn) *)
 let op_compilation n op =
-  let code_construct kn cont =
+  let code_construct reloc kn sz cont =
      let f_cont =
          let else_lbl = Label.create () in
          Kareconst(n, else_lbl):: Kacc 0:: Kpop 1::
           op:: Kreturn 0:: Klabel else_lbl::
          (* works as comp_app with nargs = n and tailcall cont [Kreturn 0]*)
-          Kgetglobal (get_allias !global_env kn)::
-          Kappterm(n, n):: [] (* = discard_dead_code [Kreturn 0] *)
+          compile_get_global reloc kn sz (
+            Kappterm(n, n):: []) (* = discard_dead_code [Kreturn 0] *)
      in
      let lbl = Label.create () in
      fun_code := [Ksequence (add_grab n lbl f_cont, !fun_code)];
@@ -926,12 +1055,11 @@ let op_compilation n op =
            (*Kaddint31::escape::Klabel else_lbl::Kpush::*)
            (op::escape::Klabel else_lbl::Kpush::
            (* works as comp_app with nargs = n and non-tailcall cont*)
-           Kgetglobal (get_allias !global_env kn)::
-           Kapply n::labeled_cont)))
+           compile_get_global reloc kn sz (Kapply n::labeled_cont))))
   else if Int.equal nargs 0 then
-    code_construct kn cont
+    code_construct reloc kn sz cont
   else
-    comp_app (fun _ _ _ cont -> code_construct kn cont)
+    comp_app (fun reloc _ sz cont -> code_construct reloc kn sz cont)
       compile_constr reloc () args sz cont
 
 let int31_escape_before_match fc cont =
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index 1128f0d0..c0f48641 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -4,17 +4,17 @@ open Term
 open Declarations
 open Pre_env
 
-
+(** Should only be used for monomorphic terms *)
 val compile : bool -> (* Fail on error with a nice user message, otherwise simply a warning *)
-	      env -> constr -> (bytecodes * bytecodes * fv) option
+	      ?universes:int -> env -> constr -> (bytecodes * bytecodes * fv) option
 (** init, fun, fv *)
 
-val compile_constant_body : bool -> 
-			    env -> constant_def -> body_code option
+val compile_constant_body : bool ->
+			    env -> constant_universes option -> constant_def -> body_code option
 
 (** Shortcut of the previous function used during module strengthening *)
 
-val compile_alias : pconstant -> body_code
+val compile_alias : Names.constant -> body_code
 
 (** spiwack: this function contains the information needed to perform
             the static compilation of int31 (trying and obtaining
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 2535a64d..ef0c9af4 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -19,7 +19,7 @@ open Mod_subst
 type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
-  | Reloc_getglobal of pconstant
+  | Reloc_getglobal of Names.constant
 
 type patch = reloc_info * int
 
@@ -127,11 +127,11 @@ let slot_for_const c =
   enter (Reloc_const c);
   out_int 0
 
-and slot_for_annot a =
+let slot_for_annot a =
   enter (Reloc_annot a);
   out_int 0
 
-and slot_for_getglobal p =
+let slot_for_getglobal p =
   enter (Reloc_getglobal p);
   out_int 0
 
@@ -190,7 +190,7 @@ let emit_instr = function
       Array.iter (out_label_with_orig org) lbl_bodies
   | Kgetglobal q ->
       out opGETGLOBAL; slot_for_getglobal q
-  | Kconst((Const_b0 i)) ->
+  | Kconst (Const_b0 i) ->
       if i >= 0 && i <= 3
           then out (opCONST0 + i)
           else (out opCONSTINT; out_int i)
@@ -225,6 +225,7 @@ let emit_instr = function
       if n <= 1 then out (opSETFIELD0+n)
       else (out opSETFIELD;out_int n)
   | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
+  | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p)
   (* spiwack *)
   | Kbranch lbl -> out opBRANCH; out_label lbl
   | Kaddint31 -> out opADDINT31
@@ -306,9 +307,10 @@ type to_patch = emitcodes * (patch list) * fv
 (* Substitution *)
 let rec subst_strcst s sc =
   match sc with
-  | Const_sorts _ | Const_b0 _ -> sc
+  | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> sc
+  | Const_proj p -> Const_proj (subst_constant s p)
   | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
-  | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u)
+  | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
 
 let subst_patch s (ri,pos) =
   match ri with
@@ -317,7 +319,7 @@ let subst_patch s (ri,pos) =
       let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in
       (Reloc_annot {a with ci = ci},pos)
   | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
-  | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos)
+  | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos)
 
 let subst_to_patch s (code,pl,fv) =
   code,List.rev_map (subst_patch s) pl,fv
@@ -326,36 +328,36 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
 
 type body_code =
   | BCdefined of to_patch
-  | BCallias of pconstant
+  | BCalias of Names.constant
   | BCconstant
 
 type to_patch_substituted =
 | PBCdefined of to_patch substituted
-| PBCallias of pconstant substituted
+| PBCalias of Names.constant substituted
 | PBCconstant
 
 let from_val = function
 | BCdefined tp -> PBCdefined (from_val tp)
-| BCallias cu -> PBCallias (from_val cu)
+| BCalias cu -> PBCalias (from_val cu)
 | BCconstant -> PBCconstant
 
 let force = function
 | PBCdefined tp -> BCdefined (force subst_to_patch tp)
-| PBCallias cu -> BCallias (force subst_pconstant cu)
+| PBCalias cu -> BCalias (force subst_constant cu)
 | PBCconstant -> BCconstant
 
 let subst_to_patch_subst s = function
 | PBCdefined tp -> PBCdefined (subst_substituted s tp)
-| PBCallias cu -> PBCallias (subst_substituted s cu)
+| PBCalias cu -> PBCalias (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 ->
+| PBCalias cu ->
   let (s, cu) = repr_substituted cu in
-  (s, BCallias cu)
+  (s, BCalias cu)
 | PBCconstant -> (None, BCconstant)
 
 let to_memory (init_code, fun_code, fv) =
@@ -371,8 +373,3 @@ let to_memory (init_code, fun_code, fv) =
     | Label_undefined patchlist ->
 	assert (patchlist = []))) !label_table;
   (code, reloc, fv)
-
-
-
-
-
diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index cec90130..10f3a608 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -4,7 +4,7 @@ open Cbytecodes
 type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
-  | Reloc_getglobal of constant Univ.puniverses
+  | Reloc_getglobal of constant
 
 type patch = reloc_info * int
 
@@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
 
 type body_code =
   | BCdefined of to_patch
-  | BCallias of constant Univ.puniverses
+  | BCalias of constant
   | BCconstant
 
 
diff --git a/kernel/constr.ml b/kernel/constr.ml
index e823c01b..e2b1d3fd 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -475,7 +475,7 @@ let map_with_binders g f l c0 = match kind c0 with
    optimisation that physically equal arrays are equals (hence the
    calls to {!Array.equal_norefl}). *)
 
-let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
+let compare_head_gen_leq_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
@@ -512,13 +512,19 @@ let compare_head_gen_with kind1 kind2 eq_universes leq_sorts eq leq t1 t2 =
    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_leq_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,
+(* [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 *)
+   not taken into account.
+
+   [compare_head_gen_with] is a variant taking kind-of-term functions,
+   to expose subterms of [c1] and [c2], as arguments. *)
+
+let compare_head_gen_with kind1 kind2 eq_universes eq_sorts eq t1 t2 =
+  compare_head_gen_leq_with kind1 kind2 eq_universes eq_sorts eq eq t1 t2
 
 let compare_head_gen eq_universes eq_sorts eq t1 t2 =
   compare_head_gen_leq eq_universes eq_sorts eq eq t1 t2
@@ -536,14 +542,6 @@ 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 
@@ -567,7 +565,7 @@ let leq_constr_univs univs m n =
     let rec compare_leq 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
+    compare_leq m n
 
 let eq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
@@ -578,16 +576,16 @@ let eq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
-	  else
-	    (cstrs := Univ.enforce_eq u1 u2 !cstrs;
-	     true)
+	if Univ.check_eq univs u1 u2 then true
+	else
+	  (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+	   true)
     in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
     in
     let res = compare_head_gen eq_universes eq_sorts eq_constr' m n in
-      res, !cstrs
+    res, !cstrs
 
 let leq_constr_univs_infer univs m n =
   if m == n then true, Constraint.empty
@@ -598,18 +596,18 @@ let leq_constr_univs_infer univs m n =
       if Sorts.equal s1 s2 then true
       else
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_eq univs u1 u2 then true
-	  else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
-		true)
+	if Univ.check_eq univs u1 u2 then true
+	else (cstrs := Univ.enforce_eq u1 u2 !cstrs;
+	      true)
     in
     let leq_sorts s1 s2 = 
       if Sorts.equal s1 s2 then true
       else 
 	let u1 = Sorts.univ_of_sort s1 and u2 = Sorts.univ_of_sort s2 in
-	  if Univ.check_leq univs u1 u2 then true
-	  else
-	    (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
-	     true)
+	if Univ.check_leq univs u1 u2 then true
+	else
+	  (cstrs := Univ.enforce_leq u1 u2 !cstrs; 
+	   true)
     in
     let rec eq_constr' m n = 
       m == n ||	compare_head_gen eq_universes eq_sorts eq_constr' m n
@@ -618,7 +616,7 @@ let leq_constr_univs_infer univs 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
+    res, !cstrs
 
 let always_true _ _ = true
 
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 67d1aded..e6a3e71f 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -203,14 +203,6 @@ 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
@@ -293,6 +285,18 @@ val compare_head_gen : (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
   (constr -> constr -> bool) ->
   constr -> constr -> bool
 
+(** [compare_head_gen_with k1 k2 u s f c1 c2] compares [c1] and [c2]
+    like [compare_head_gen u s f c1 c2], except that [k1] (resp. [k2])
+    is used,rather than {!kind}, to expose the immediate subterms of
+    [c1] (resp. [c2]). *)
+val compare_head_gen_with :
+  (constr -> (constr,types) kind_of_term) ->
+  (constr -> (constr,types) kind_of_term) ->
+  (bool -> Univ.Instance.t -> Univ.Instance.t -> bool) ->
+  (Sorts.t -> Sorts.t -> bool) ->
+  (constr -> constr -> bool) ->
+  constr -> constr -> bool
+
 (** [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
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 3b01538b..ec2c334b 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -82,12 +82,17 @@ let fold_strategy f { var_opacity; cst_opacity; } accu =
 let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate)
 
 (* Unfold the first constant only if it is "more transparent" than the
-   second one. In case of tie, expand the second one. *)
+   second one. In case of tie, use the recommended default. *)
 let oracle_order f o l2r k1 k2 =
   match get_strategy o f k1, get_strategy o f k2 with
-    | Expand, _ -> true
-    | Level n1, Opaque -> true
-    | Level n1, Level n2 -> n1 < n2
-    | _ -> l2r (* use recommended default *)
+  | Expand, Expand -> l2r
+  | Expand, (Opaque | Level _) -> true
+  | (Opaque | Level _), Expand -> false
+  | Opaque, Opaque -> l2r
+  | Level _, Opaque -> true
+  | Opaque, Level _ -> false
+  | Level n1, Level n2 ->
+     if Int.equal n1 n2 then l2r
+     else n1 < n2
 
 let get_strategy o = get_strategy o (fun x -> x)
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index b29f06c6..28f0fa4f 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -57,22 +57,34 @@ let set_global v =
 
 let rec eq_structured_constant c1 c2 = match c1, c2 with
 | Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2
-| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
+| Const_sorts _, _ -> false
+| Const_ind i1, Const_ind i2 -> eq_ind i1 i2
+| Const_ind _, _ -> false
+| Const_proj p1, Const_proj p2 -> Constant.equal p1 p2
+| Const_proj _, _ -> false
 | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2
+| Const_b0 _, _ -> false
 | Const_bn (t1, a1), Const_bn (t2, a2) ->
   Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
-| _ -> false
+| Const_bn _, _ -> false
+| Const_univ_level l1 , Const_univ_level l2 -> Univ.eq_levels l1 l2
+| Const_univ_level _ , _ -> false
+| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2
+| Const_type _ , _ -> false
 
 let rec hash_structured_constant c =
   let open Hashset.Combine in
   match c with
   | Const_sorts s -> combinesmall 1 (Sorts.hash s)
-  | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u))
-  | Const_b0 t -> combinesmall 3 (Int.hash t)
+  | Const_ind i -> combinesmall 2 (ind_hash i)
+  | Const_proj p -> combinesmall 3 (Constant.hash p)
+  | Const_b0 t -> combinesmall 4 (Int.hash t)
   | Const_bn (t, a) ->
     let fold h c = combine h (hash_structured_constant c) in
     let h = Array.fold_left fold 0 a in
-    combinesmall 4 (combine (Int.hash t) h)
+    combinesmall 5 (combine (Int.hash t) h)
+  | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l)
+  | Const_type u -> combinesmall 7 (Univ.Universe.hash u)
 
 module SConstTable = Hashtbl.Make (struct
   type t = structured_constant
@@ -118,7 +130,7 @@ exception NotEvaluated
 let key rk =
   match !rk with
   | None -> raise NotEvaluated
-  | Some k -> (*Pp.msgnl (str"found at: "++int k);*)
+  | Some k ->
       try Ephemeron.get k
       with Ephemeron.InvalidKey -> raise NotEvaluated
 
@@ -142,23 +154,22 @@ let slot_for_annot key =
     AnnotTable.add annot_tbl key n;
     n
 
-let rec slot_for_getglobal env (kn,u) =
+let rec slot_for_getglobal env kn =
   let (cb,(_,rk)) = lookup_constant_key kn env in
   try key rk
   with NotEvaluated ->
 (*    Pp.msgnl(str"not yet evaluated");*)
     let pos =
       match cb.const_body_code with
-      | None -> set_global (val_of_constant (kn,u))
+      | None -> set_global (val_of_constant kn)
       | 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
+           let v = eval_to_patch env (code,pl,fv) in
+           set_global v
+	 | BCalias kn' -> slot_for_getglobal env kn'
+	 | BCconstant -> set_global (val_of_constant kn)
+    in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
     rk := Some (Ephemeron.create pos);
     pos
@@ -191,6 +202,8 @@ and slot_for_fv env fv =
           fill_fv_cache rv i val_of_rel env_of_rel b
       | Some (v, _) -> v
       end
+  | FVuniv_var idu ->
+    assert false
 
 and eval_to_patch env (buff,pl,fv) =
   (* copy code *before* patching because of nested evaluations:
@@ -208,7 +221,6 @@ and eval_to_patch env (buff,pl,fv) =
   List.iter patch pl;
   let vm_env = Array.map (slot_for_fv env) fv in
   let tc = tcode_of_code buff (length buff) in
-(*Pp.msgnl (str"execute code");*)
   eval_tcode tc vm_env
 
 and val_of_constr env c =
@@ -226,5 +238,3 @@ and val_of_constr env c =
 
 let set_transparent_const kn = () (* !?! *)
 let set_opaque_const kn = () (* !?! *)
-
-
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 27c1c3f3..dc5c17a7 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -14,7 +14,10 @@ open Context
    declarations. This includes global constants/axioms, mutual
    inductive definitions, modules and module types *)
 
-type engagement = ImpredicativeSet
+type set_predicativity = ImpredicativeSet | PredicativeSet
+type type_hierarchy = TypeInType | StratifiedType
+
+type engagement = set_predicativity * type_hierarchy
 
 (** {6 Representation of constants (Definition/Axiom) } *)
 
@@ -76,12 +79,6 @@ type constant_body = {
     const_proj : projection_body option;
     const_inline_code : bool }
 
-type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
-
-type side_effect =
-  | SEsubproof of constant * constant_body * seff_env
-  | SEscheme of (inductive * constant * constant_body * seff_env) list * string
-    
 (** {6 Representation of mutual inductive types in the kernel } *)
 
 type recarg =
@@ -142,12 +139,10 @@ type one_inductive_body = {
     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)
-    (not used in the kernel) *)
+ (** Number of expected proper arguments of the constructors (w/o params) *)
 
     mind_consnrealdecls : int array;
- (** Length of the signature of the constructors (with let, w/o params)
-    (not used in the kernel) *)
+ (** Length of the signature of the constructors (with let, w/o params) *)
 
     mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *)
 
@@ -245,8 +240,8 @@ and module_body =
     mod_type : module_signature; (** expanded type *)
     (** algebraic type, kept if it's relevant for extraction *)
     mod_type_alg : module_expression option;
-    (** set of all constraints in the module  *)
-    mod_constraints : Univ.constraints;
+    (** set of all universes constraints in the module  *)
+    mod_constraints : Univ.ContextSet.t;
     (** quotiented set of equivalent constants and inductive names *)
     mod_delta : Mod_subst.delta_resolver;
     mod_retroknowledge : Retroknowledge.action list }
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index a7051d5c..248504c1 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -304,17 +304,7 @@ let hcons_mind mib =
 
 (** {6 Stm machinery } *)
 
-let string_of_side_effect = function
-  | SEsubproof (c,_,_) -> Names.string_of_con c
-  | SEscheme (cl,_) ->
-      String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl)
-type side_effects = side_effect list
-let no_seff = ([] : side_effects)
-let iter_side_effects f l = List.iter f (List.rev l)
-let fold_side_effects f a l = List.fold_left f a l
-let uniquize_side_effects l = List.rev (CList.uniquize (List.rev l))
-let union_side_effects l1 l2 = l1 @ l2
-let flatten_side_effects l = List.flatten l
-let side_effects_of_list l = l
-let cons_side_effects x l = x :: l
-let side_effects_is_empty = List.is_empty
+let string_of_side_effect { Entries.eff } = match eff with
+  | Entries.SEsubproof (c,_,_) -> "P(" ^ Names.string_of_con c ^ ")"
+  | Entries.SEscheme (cl,_) ->
+      "S(" ^ String.concat ", " (List.map (fun (_,c,_,_) -> Names.string_of_con c) cl) ^ ")"
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index ce65af97..1b870095 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -9,6 +9,7 @@
 open Declarations
 open Mod_subst
 open Univ
+open Entries
 
 (** Operations concerning types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -49,17 +50,6 @@ val is_opaque : constant_body -> bool
 
 val string_of_side_effect : side_effect -> string
 
-type side_effects
-val no_seff : side_effects
-val iter_side_effects : (side_effect -> unit) -> side_effects -> unit
-val fold_side_effects : ('a -> side_effect -> 'a) -> 'a -> side_effects -> 'a
-val uniquize_side_effects : side_effects -> side_effects
-val union_side_effects : side_effects -> side_effects -> side_effects
-val flatten_side_effects : side_effects list -> side_effects
-val side_effects_of_list : side_effect list -> side_effects
-val cons_side_effects : side_effect -> side_effects -> side_effects
-val side_effects_is_empty : side_effects -> bool
-
 (** {6 Inductive types} *)
 
 val eq_recarg : recarg -> recarg -> bool
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 303d27d3..e058519e 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -54,11 +54,11 @@ type mutual_inductive_entry = {
   mind_entry_private : bool option }
 
 (** {6 Constants (Definition/Axiom) } *)
-type proof_output = constr Univ.in_universe_context_set * Declareops.side_effects
-type const_entry_body = proof_output Future.computation
+type 'a proof_output = constr Univ.in_universe_context_set * 'a
+type 'a const_entry_body = 'a proof_output Future.computation
 
-type definition_entry = {
-  const_entry_body   : const_entry_body;
+type 'a definition_entry = {
+  const_entry_body   : 'a const_entry_body;
   (* List of section variables *)
   const_entry_secctx : Context.section_context option;
   (* State id on which the completion of type checking is reported *)
@@ -78,8 +78,8 @@ type projection_entry = {
   proj_entry_ind : mutual_inductive;
   proj_entry_arg : int }
 
-type constant_entry =
-  | DefinitionEntry of definition_entry
+type 'a constant_entry =
+  | DefinitionEntry of 'a definition_entry
   | ParameterEntry of parameter_entry
   | ProjectionEntry of projection_entry
 
@@ -96,3 +96,16 @@ type module_entry =
   | MType of module_params_entry * module_struct_entry
   | MExpr of
       module_params_entry * module_struct_entry * module_struct_entry option
+
+type seff_env = [ `Nothing | `Opaque of Constr.t * Univ.universe_context_set ]
+
+type side_eff =
+  | SEsubproof of constant * Declarations.constant_body * seff_env
+  | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string
+
+type side_effect = {
+  from_env : Declarations.structure_body Ephemeron.key;
+  eff      : side_eff;
+}
+
+type side_effects = side_effect list
diff --git a/kernel/environ.ml b/kernel/environ.ml
index a79abbb7..429aba4f 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -46,11 +46,14 @@ let empty_env = empty_env
 
 let engagement env = env.env_stratification.env_engagement
 
-let type_in_type env = env.env_stratification.env_type_in_type
-
 let is_impredicative_set env = 
-  match engagement env with
-  | Some ImpredicativeSet -> true
+  match fst (engagement env) with
+  | ImpredicativeSet -> true
+  | _ -> false
+
+let type_in_type env =
+  match snd (engagement env) with
+  | TypeInType -> true
   | _ -> false
 
 let universes env = env.env_stratification.env_universes
@@ -159,7 +162,7 @@ let reset_context = reset_with_named_context empty_named_context_val
 let pop_rel_context n env =
   let ctxt = env.env_rel_context in
   { env with
-    env_rel_context = List.firstn (List.length ctxt - n) ctxt;
+    env_rel_context = List.skipn n ctxt;
     env_nb_rel = env.env_nb_rel - n }
 
 let fold_named_context f env ~init =
@@ -178,30 +181,44 @@ let fold_named_context_reverse f ~init env =
 
 (* Universe constraints *)
 
-let add_constraints c env =
-  if Univ.Constraint.is_empty c then
-    env
-  else
-    let s = env.env_stratification in
+let map_universes f env =
+  let s = env.env_stratification in
     { env with env_stratification =
-      { s with env_universes = Univ.merge_constraints c s.env_universes } }
+	 { s with env_universes = f s.env_universes } }
+				     
+let add_constraints c env =
+  if Univ.Constraint.is_empty c then env
+  else map_universes (Univ.merge_constraints c) env
 
 let check_constraints c env =
   Univ.check_constraints c env.env_stratification.env_universes
 
-let set_engagement c env = (* Unsafe *)
-  { env with env_stratification =
-    { env.env_stratification with env_engagement = Some c } }
-
-let set_type_in_type env =
-  { env with env_stratification =
-    { env.env_stratification with env_type_in_type = true } }
-
 let push_constraints_to_env (_,univs) env =
   add_constraints univs env
 
-let push_context ctx env = add_constraints (Univ.UContext.constraints ctx) env
-let push_context_set ctx env = add_constraints (Univ.ContextSet.constraints ctx) env
+let add_universes strict ctx g =
+  let g = Array.fold_left
+	    (* Be lenient, module typing reintroduces universes and constraints due to includes *)
+	    (fun g v -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+	    g (Univ.Instance.to_array (Univ.UContext.instance ctx))
+  in
+    Univ.merge_constraints (Univ.UContext.constraints ctx) g
+			   
+let push_context ?(strict=false) ctx env =
+  map_universes (add_universes strict ctx) env
+
+let add_universes_set strict ctx g =
+  let g = Univ.LSet.fold
+	    (fun v g -> try Univ.add_universe v strict g with Univ.AlreadyDeclared -> g)
+	    (Univ.ContextSet.levels ctx) g
+  in Univ.merge_constraints (Univ.ContextSet.constraints ctx) g
+
+let push_context_set ?(strict=false) ctx env =
+  map_universes (add_universes_set strict ctx) env
+
+let set_engagement c env = (* Unsafe *)
+  { env with env_stratification =
+    { env.env_stratification with env_engagement = c } }
 
 (* Global constants *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index ede356e6..dfe6cc85 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -50,10 +50,9 @@ val opaque_tables : env -> Opaqueproof.opaquetab
 val set_opaque_tables : env -> Opaqueproof.opaquetab -> env
 
 
-val engagement    : env -> engagement option
+val engagement    : env -> engagement
 val is_impredicative_set : env -> bool
-
-val type_in_type  : env -> bool
+val type_in_type : env -> bool
 
 (** is the local context empty *)
 val empty_context : env -> bool
@@ -209,14 +208,12 @@ val add_constraints : Univ.constraints -> env -> env
 
 (** Check constraints are satifiable in the environment. *)
 val check_constraints : Univ.constraints -> env -> bool
-val push_context : Univ.universe_context -> env -> env
-val push_context_set : Univ.universe_context_set -> env -> env
+val push_context : ?strict:bool -> Univ.universe_context -> env -> env
+val push_context_set : ?strict:bool -> Univ.universe_context_set -> env -> env
 val push_constraints_to_env : 'a Univ.constrained -> env -> env
 
 val set_engagement : engagement -> env -> env
 
-val set_type_in_type : env -> env
-
 (** {6 Sets of referred section variables }
    [global_vars_set env c] returns the list of [id]'s occurring either
    directly as [Var id] in [c] or indirectly as a section variable
@@ -253,7 +250,7 @@ type unsafe_type_judgment = {
 
 (** {6 Compilation of global declaration } *)
 
-val compile_constant_body : env -> constant_def -> Cemitcodes.body_code option
+val compile_constant_body : env -> constant_universes option -> constant_def -> Cemitcodes.body_code option
 
 exception Hyp_not_found
 
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index 86fb1b64..063c9cf1 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -182,14 +182,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Universe.sup Universe.type0 u1)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
@@ -229,7 +227,7 @@ let judge_of_cast env c ct k expected_type =
       default_conv ~l2r:true CUMUL env ct expected_type
     | NATIVEcast ->
       let sigma = Nativelambda.empty_evars in
-      native_conv CUMUL sigma env ct expected_type
+      Nativeconv.native_conv CUMUL sigma env ct expected_type
   with NotConvertible ->
     error_actual_type env (make_judge c ct) expected_type
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 6b909824..8b03df64 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -173,38 +173,21 @@ let cumulate_arity_large_levels env sign =
     sign (Universe.type0m,env))
 
 let is_impredicative env u =
-  is_type0m_univ u || (is_type0_univ u && engagement env = Some ImpredicativeSet)
+  is_type0m_univ u || (is_type0_univ u && is_impredicative_set env)
 
+(* Returns the list [x_1, ..., x_n] of levels contributing to template
+   polymorphism. The elements x_k is None if the k-th parameter (starting
+   from the most recent and ignoring let-definitions) is not contributing 
+   or is Some u_k if its level is u_k and is contributing. *)
 let param_ccls params =
-  let has_some_univ u = function
-    | Some v when Univ.Level.equal u v -> true
-    | _ -> false
+  let fold acc = function (_, None, p) -> 
+      (let c = strip_prod_assum p in
+      match kind_of_term c with
+        | Sort (Type u) -> Univ.Universe.level u
+        | _ -> None) :: acc
+    | _ -> acc 
   in
-  let remove_some_univ u = function
-    | Some v when Univ.Level.equal u v -> None
-    | x -> x
-  in
-  let fold l (_, b, p) = match b with
-  | None ->
-    (* Parameter contributes to polymorphism only if explicit Type *)
-    let c = strip_prod_assum p in
-    (* Add Type levels to the ordered list of parameters contributing to *)
-    (* polymorphism unless there is aliasing (i.e. non distinct levels) *)
-    begin match kind_of_term c with
-    | Sort (Type u) ->
-      (match Univ.Universe.level u with
-      | Some u ->
-	if List.exists (has_some_univ u) l then
-          None :: List.map (remove_some_univ u) l
-	else
-          Some u :: l
-      | None -> None :: l)
-    | _ ->
-      None :: l
-    end
-  | _ -> l
-  in
-    List.fold_left fold [] params
+  List.fold_left fold [] params
 
 (* Type-check an inductive definition. Does not check positivity
    conditions. *)
@@ -302,8 +285,7 @@ let typecheck_inductive env mie =
       let full_polymorphic () = 
 	let defu = Term.univ_of_sort def_level in
 	let is_natural =
-	  type_in_type env || (check_leq (universes env') infu defu &&
-	    not (is_type0m_univ defu && not is_unit))
+	  type_in_type env || (check_leq (universes env') infu defu)
 	in
 	let _ =
 	  (** Impredicative sort, always allow *)
@@ -356,7 +338,7 @@ type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
   | LocalNotConstructor
-  | LocalNonPar of int * int
+  | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
 
@@ -377,9 +359,9 @@ let explain_ind_err id ntyp env nbpar c nargs err =
     | LocalNotConstructor ->
 	raise (InductiveError
 		 (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nbpar,nargs)))
-    | LocalNonPar (n,l) ->
+    | LocalNonPar (n,i,l) ->
 	raise (InductiveError
-		 (NonPar (env,c',n,mkRel (nbpar-n+1), mkRel (l+nbpar))))
+		 (NonPar (env,c',n,mkRel i, mkRel (l+nbpar))))
 
 let failwith_non_pos n ntypes c =
   for k = n to n + ntypes - 1 do
@@ -408,7 +390,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs =
     | _::hyps ->
         match kind_of_term (whd_betadeltaiota env lpar.(k)) with
 	  | Rel w when Int.equal w index -> check (k-1) (index+1) hyps
-	  | _ -> raise (IllFormedInd (LocalNonPar (k+1,l)))
+	  | _ -> raise (IllFormedInd (LocalNonPar (k+1, index-n+nhyps+1, l)))
   in check (nparams-1) (n-nhyps) hyps;
   if not (Array.for_all (noccur_between n ntypes) largs') then
     failwith_non_pos_vect n ntypes largs'
@@ -663,10 +645,28 @@ exception UndefinableExpansion
     build an expansion function.
     The term built is expecting to be substituted first by 
     a substitution of the form [params, x : ind params] *)
-let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
-    mind_consnrealdecls mind_consnrealargs ctx =
+let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
+    mind_consnrealdecls mind_consnrealargs paramslet ctx =
   let mp, dp, l = repr_mind kn in
-  let rp = mkApp (mkIndU indsp, rel_vect 0 nparamargs) in
+  (** We build a substitution smashing the lets in the record parameters so
+      that typechecking projections requires just a substitution and not
+      matching with a parameter context. *)
+  let indty, paramsletsubst =
+    let subst, inst = 
+      List.fold_right
+	(fun (na, b, t) (subst, inst) ->
+	 match b with
+	 | None -> (mkRel 1 :: List.map (lift 1) subst,
+		   mkRel 1 :: List.map (lift 1) inst)
+	 | Some b -> (substl subst b) :: subst, List.map (lift 1) inst)
+	paramslet ([], [])
+    in
+    let subst = (* For the record parameter: *)
+      mkRel 1 :: List.map (lift 1) subst
+    in
+    let ty = mkApp (mkIndU indu, CArray.rev_of_list inst) in
+      ty, subst
+  in
   let ci = 
     let print_info =
       { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
@@ -679,34 +679,39 @@ let compute_projections ((kn, _ as ind), u as indsp) n x nparamargs params
   let len = List.length ctx in
   let x = Name x in
   let compat_body ccl i = 
-    (* [ccl] is defined in context [params;x:rp] *)
-    (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+    (* [ccl] is defined in context [params;x:indty] *)
+    (* [ccl'] is defined in context [params;x:indty;x:indty] *)
     let ccl' = liftn 1 2 ccl in
-    let p = mkLambda (x, lift 1 rp, ccl') in
+    let p = mkLambda (x, lift 1 indty, ccl') in
     let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
     let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
-      it_mkLambda_or_LetIn (mkLambda (x,rp,body)) params
+      it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
   in
-  let projections (na, b, t) (i, j, kns, pbs, subst) =
+  let projections (na, b, t) (i, j, kns, pbs, subst, letsubst) =
     match b with
-    | Some c -> (i, j+1, kns, pbs, substl subst c :: subst)
+    | Some c -> (i, j+1, kns, pbs, substl subst c :: subst,
+		substl letsubst c :: subst)
     | None ->
       match na with
       | Name id ->
 	let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in
+	let projty = substl letsubst (liftn 1 j t) in
 	let ty = substl subst (liftn 1 j t) in
 	let term = mkProj (Projection.make kn true, mkRel 1) in
 	let fterm = mkProj (Projection.make kn false, mkRel 1) in
 	let compat = compat_body ty (j - 1) in
-	let etab = it_mkLambda_or_LetIn (mkLambda (x, rp, term)) params in
-	let etat = it_mkProd_or_LetIn (mkProd (x, rp, ty)) params in
+	let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
+	let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
 	let body = { proj_ind = fst ind; proj_npars = nparamargs;
-		     proj_arg = i; proj_type = ty; proj_eta = etab, etat; 
+		     proj_arg = i; proj_type = projty; proj_eta = etab, etat; 
 		     proj_body = compat } in
-	  (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: subst)
+	  (i + 1, j + 1, kn :: kns, body :: pbs,
+	   fterm :: subst, fterm :: letsubst)
       | Anonymous -> raise UndefinableExpansion
   in
-  let (_, _, kns, pbs, subst) = List.fold_right projections ctx (0, 1, [], [], []) in
+  let (_, _, kns, pbs, subst, letsubst) =
+    List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst)
+  in
     Array.of_list (List.rev kns),
     Array.of_list (List.rev pbs)
 
@@ -792,12 +797,12 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
 	else Univ.Instance.empty 
       in
       let indsp = ((kn, 0), u) in
-      let rctx, _ = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
+      let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
 	(try 
-	   let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
+	   let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
 	   let kns, projs = 
 	     compute_projections indsp pkt.mind_typename rid nparamargs params
-	       pkt.mind_consnrealdecls pkt.mind_consnrealargs fields
+	       pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
 	   in Some (Some (rid, kns, projs))
 	 with UndefinableExpansion -> Some None)
     | Some _ -> Some None
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7774e52e..01acdce5 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -43,5 +43,5 @@ val is_indices_matter : unit -> bool
 
 val compute_projections : pinductive -> Id.t -> Id.t ->
   int -> Context.rel_context -> int array -> int array -> 
-  Context.rel_context -> 
+  Context.rel_context -> Context.rel_context -> 
   (constant array * projection_body array)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index ca814f49..1f870665 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -73,7 +73,7 @@ let constructor_instantiate mind u mib c =
   let s = ind_subst mind mib u in
     substl s (subst_instance_constr u c)
 
-let instantiate_params full t args sign =
+let instantiate_params full t u args sign =
   let fail () =
     anomaly ~label:"instantiate_params" (Pp.str "type, ctxt and args mismatch") in
   let (rem_args, subs, ty) =
@@ -81,7 +81,8 @@ let instantiate_params full t args sign =
       (fun (_,copt,_) (largs,subs,ty) ->
         match (copt, largs, kind_of_term ty) with
           | (None, a::args, Prod(_,_,t)) -> (args, a::subs, t)
-          | (Some b,_,LetIn(_,_,_,t))    -> (largs, (substl subs b)::subs, t)
+          | (Some b,_,LetIn(_,_,_,t))    ->
+	     (largs, (substl subs (subst_instance_constr u b))::subs, t)
 	  | (_,[],_)                -> if full then fail() else ([], subs, ty)
 	  | _                       -> fail ())
       sign
@@ -92,15 +93,13 @@ let instantiate_params full t args sign =
 
 let full_inductive_instantiate mib u params sign =
   let dummy = prop_sort in
-  let t = mkArity (sign,dummy) in
-  let ar = fst (destArity (instantiate_params true t params mib.mind_params_ctxt)) in
-    Vars.subst_instance_context u ar
-
-let full_constructor_instantiate ((mind,_),u,(mib,_),params) =
-  let inst_ind = constructor_instantiate mind u mib in
-  (fun t ->
-    instantiate_params true (inst_ind t) params mib.mind_params_ctxt)
+  let t = mkArity (Vars.subst_instance_context u sign,dummy) in
+    fst (destArity (instantiate_params true t u params mib.mind_params_ctxt))
 
+let full_constructor_instantiate ((mind,_),u,(mib,_),params) t =
+  let inst_ind = constructor_instantiate mind u mib t in
+   instantiate_params true inst_ind u params mib.mind_params_ctxt
+		      
 (************************************************************************)
 (************************************************************************)
 
@@ -134,46 +133,60 @@ let sort_as_univ = function
 
 (* Template polymorphism *)
 
+(* cons_subst add the mapping [u |-> su] in subst if [u] is not *)
+(* in the domain or add [u |-> sup x su] if [u] is already mapped *)
+(* to [x]. *)
 let cons_subst u su subst =
-  Univ.LMap.add u su subst
+  try
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> Univ.LMap.add u su subst
+
+(* remember_subst updates the mapping [u |-> x] by [u |-> sup x u] *)
+(* if it is presents and returns the substitution unchanged if not.*)
+let remember_subst u subst =
+  try
+    let su = Universe.make u in
+    Univ.LMap.add u (Univ.sup (Univ.LMap.find u subst) su) subst
+  with Not_found -> subst
 
 (* Bind expected levels of parameters to actual levels *)
 (* Propagate the new levels in the signature *)
-let rec make_subst env = function
-  | (_,Some _,_ as t)::sign, exp, args ->
-      let ctx,subst = make_subst env (sign, exp, args) in
-      t::ctx, subst
-  | d::sign, None::exp, args ->
-      let args = match args with _::args -> args | [] -> [] in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, subst
-  | d::sign, Some u::exp, a::args ->
-      (* We recover the level of the argument, but we don't change the *)
-      (* level in the corresponding type in the arity; this level in the *)
-      (* arity is a global level which, at typing time, will be enforce *)
-      (* to be greater than the level of the argument; this is probably *)
-      (* a useless extra constraint *)
-      let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
-      let ctx,subst = make_subst env (sign, exp, args) in
-      d::ctx, cons_subst u s subst
-  | (na,None,t as d)::sign, Some u::exp, [] ->
-      (* No more argument here: we instantiate the type with a fresh level *)
-      (* which is first propagated to the corresponding premise in the arity *)
-      (* (actualize_decl_level), then to the conclusion of the arity (via *)
-      (* the substitution) *)
-      let ctx,subst = make_subst env (sign, exp, []) in
-	d::ctx, subst
-  | sign, [], _ ->
-      (* Uniform parameters are exhausted *)
-      sign, Univ.LMap.empty
-  | [], _, _ ->
-      assert false
+let rec make_subst env =
+  let rec make subst = function
+    | (_,Some _,_)::sign, exp, args ->
+        make subst (sign, exp, args)
+    | d::sign, None::exp, args ->
+        let args = match args with _::args -> args | [] -> [] in
+        make subst (sign, exp, args)
+    | d::sign, Some u::exp, a::args ->
+        (* We recover the level of the argument, but we don't change the *)
+        (* level in the corresponding type in the arity; this level in the *)
+        (* arity is a global level which, at typing time, will be enforce *)
+        (* to be greater than the level of the argument; this is probably *)
+        (* a useless extra constraint *)
+        let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
+          make (cons_subst u s subst) (sign, exp, args)
+    | (na,None,t)::sign, Some u::exp, [] ->
+        (* No more argument here: we add the remaining universes to the *)
+        (* substitution (when [u] is distinct from all other universes in the *)
+        (* template, it is identity substitution  otherwise (ie. when u is *)
+        (* already in the domain of the substitution) [remember_subst] will *)
+        (* update its image [x] by [sup x u] in order not to forget the *)
+        (* dependency in [u] that remains to be fullfilled. *)
+        make (remember_subst u subst) (sign, exp, [])
+    | sign, [], _ ->
+        (* Uniform parameters are exhausted *)
+        subst
+    | [], _, _ ->
+        assert false
+  in
+  make Univ.LMap.empty
 
 exception SingletonInductiveBecomesProp of Id.t
 
 let instantiate_universes env ctx ar argsorts =
   let args = Array.to_list argsorts in
-  let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in
+  let subst = make_subst env (ctx,ar.template_param_levels,args) in
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
@@ -213,8 +226,8 @@ let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) a
   let cst = instantiate_inductive_constraints mib u in
     (ty, cst)
 
-let type_of_inductive_knowing_parameters env ?(polyprop=false) mip args = 
-  type_of_inductive_gen env mip args
+let type_of_inductive_knowing_parameters env ?(polyprop=true) mip args =
+  type_of_inductive_gen ~polyprop env mip args
 
 (* The max of an array of universes *)
 
@@ -331,13 +344,13 @@ let is_correct_arity env c pj ind specif params =
       | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *)
 	 let env' = push_rel (na1,None,a1) env in
 	 let ksort = match kind_of_term (whd_betadeltaiota env' a2) with
-       | Sort s -> family_of_sort s
-       | _ -> raise (LocalArity None) in
+	 | Sort s -> family_of_sort s
+	 | _ -> raise (LocalArity None) in
 	 let dep_ind = build_dependent_inductive ind specif params in
 	 let _ =
            try conv env a1 dep_ind
            with NotConvertible -> raise (LocalArity None) in
-	 check_allowed_sort ksort specif
+	   check_allowed_sort ksort specif
       | _, (_,Some _,_ as d)::ar' ->
 	  srec (push_rel d env) (lift 1 pt') ar'
       | _ ->
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index f7ae30e7..ba14f65d 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -122,7 +122,7 @@ let add_kn_delta_resolver kn kn' =
 
 let add_mp_delta_resolver mp1 mp2 = Deltamap.add_mp mp1 mp2
 
-(** Extending a [substitution] *)
+(** Extending a [substitution] without sequential composition *)
 
 let add_mbid mbid mp resolve s = Umap.add_mbi mbid (mp,resolve) s
 let add_mp mp1 mp2 resolve s = Umap.add_mp mp1 (mp2,resolve) s
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index fc2b0441..cd9fa792 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -68,8 +68,9 @@ val empty_subst : substitution
 
 val is_empty_subst : substitution -> bool
 
-(** add_* add [arg2/arg1]\{arg3\} to the substitution with no
-   sequential composition  *)
+(** add_* add [arg2/arg1]\{arg3\} to the substitution with no sequential
+   composition. Most often this is not what you want. For sequential
+   composition, try [join (map_mbid mp delta) subs] **)
 val add_mbid :
   MBId.t -> module_path -> delta_resolver  -> substitution -> substitution
 val add_mp :
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 26dd45f5..bd7ee7b3 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -21,7 +21,7 @@ open Modops
 open Mod_subst
 
 type 'alg translation =
-  module_signature * 'alg option * delta_resolver * Univ.constraints
+  module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
 
 let rec mp_from_mexpr = function
   | MEident mp -> mp
@@ -52,7 +52,7 @@ let rec rebuild_mp mp l =
   | []-> mp
   | i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r
 
-let (+++) = Univ.Constraint.union
+let (+++) = Univ.ContextSet.union
 
 let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
   let lab,idl = match idl with
@@ -72,33 +72,71 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
       (* In the spirit of subtyping.check_constant, we accept
          any implementations of parameters and opaques terms,
 	 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')
-	    j.uj_type typ in
-	  j.uj_val,cst' +++ cst
-	| Def cs ->
-	  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' +++ cst
-	    else cst' +++ cst
+      let uctx = Declareops.universes_of_constant (opaque_tables env) cb in
+      let uctx = (* Context of the spec *)
+	if cb.const_polymorphic then
+	  Univ.instantiate_univ_context uctx
+	else uctx
+      in
+      let c', univs, ctx' = 
+	if not cb.const_polymorphic then
+	  let env' = Environ.push_context ~strict:true uctx env' in
+	  let env' = Environ.push_context ~strict:true ctx 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')
+						j.uj_type typ in
+	      j.uj_val, cst'
+	    | Def cs ->
+	       let c' = Mod_subst.force_constr cs in
+	         c, Reduction.infer_conv env' (Environ.universes env') c c'
+	  in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+	else
+	  let cus, ccst = Univ.UContext.dest uctx in
+	  let newus, cst = Univ.UContext.dest ctx in
+	  let () =
+	    if not (Univ.Instance.length cus == Univ.Instance.length newus) then
+	      error_incorrect_with_constraint lab
+	  in
+	  let inst = Univ.Instance.append cus newus in
+	  let csti = Univ.enforce_eq_instances cus newus cst in
+	  let csta = Univ.Constraint.union csti ccst in
+	  let env' = Environ.push_context ~strict:false (Univ.UContext.make (inst, csta)) env in
+	  let () = if not (Univ.check_constraints cst (Environ.universes env')) then
+		     error_incorrect_with_constraint lab
+	  in
+	  let 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 typ = Vars.subst_instance_constr cus typ in
+	      let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+						j.uj_type typ in
+	      cst'
+	    | Def cs ->
+	       let c' = Vars.subst_instance_constr cus (Mod_subst.force_constr cs) in
+	       let cst' = Reduction.infer_conv env' (Environ.universes env') c c' in
+	        cst'
 	  in
-            c, cst
+	    if not (Univ.Constraint.is_empty cst) then
+	      error_incorrect_with_constraint lab;
+	    let subst, ctx = Univ.abstract_universes true ctx in
+	      Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty
       in
       let def = Def (Mod_subst.from_val c') in
-      let ctx' = Univ.UContext.make (newus, cst) in
+(*      let ctx' = Univ.UContext.make (newus, cst) in *)
+      let univs =
+        if cb.const_polymorphic then Some cb.const_universes
+        else None
+      in
       let cb' =
 	{ cb with
 	  const_body = def;
-	  const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def);
-	  const_universes = ctx' }
+          const_universes = ctx ;
+	  const_body_code = Option.map Cemitcodes.from_val
+                              (compile_constant_body env' univs def) }
       in
       before@(lab,SFBconst(cb'))::after, c', ctx'
     else
@@ -145,8 +183,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
 	  begin
             try
               let mtb_old = module_type_of_module old in
-              Subtyping.check_subtypes env' mtb_mp1 mtb_old
-                +++ old.mod_constraints
+              Univ.ContextSet.add_constraints (Subtyping.check_subtypes env' mtb_mp1 mtb_old) old.mod_constraints
 	    with Failure _ -> error_incorrect_with_constraint lab
 	  end
 	| Algebraic (NoFunctor (MEident(mp'))) ->
@@ -194,7 +231,7 @@ let rec check_with_mod env struc (idl,mp1) mp equiv =
       | Algebraic (NoFunctor (MEident mp0)) ->
 	let mpnew = rebuild_mp mp0 idl in
 	check_modpath_equiv env' mpnew mp;
-	before@(lab,spec)::after, equiv, Univ.Constraint.empty
+	before@(lab,spec)::after, equiv, Univ.ContextSet.empty
       | _ -> error_generative_module_expected lab
       end
   with
@@ -207,8 +244,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',cst'))) in
-    (NoFunctor struc'),alg',reso, cst+++(Univ.UContext.constraints cst')
+    let alg' = mk_alg_with alg (WithDef (idl,(c',Univ.ContextSet.to_context cst'))) in
+    (NoFunctor struc'),alg',reso, cst+++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
@@ -238,7 +275,7 @@ let rec translate_mse env mpo inl = function
         let mtb = lookup_modtype mp1 env in
         mtb.mod_type, mtb.mod_delta
     in
-    sign,Some (MEident mp1),reso,Univ.Constraint.empty
+    sign,Some (MEident mp1),reso,Univ.ContextSet.empty
   |MEapply (fe,mp1) ->
     translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
   |MEwith(me, with_decl) ->
@@ -256,7 +293,7 @@ and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
   let body = subst_signature subst fbody_b in
   let alg' = mkalg alg mp1 in
   let reso' = subst_codom_delta_resolver subst reso in
-  body,alg',reso', cst1 +++ cst2
+  body,alg',reso', Univ.ContextSet.add_constraints cst2 cst1
 
 let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
   | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
@@ -301,13 +338,15 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
     mk_mod mp impl sign None cst reso
   |Some (params_mte,inl) ->
     let res_mtb = translate_modtype env mp inl params_mte in
-    let auto_mtb = mk_modtype mp sign Univ.Constraint.empty reso in
+    let auto_mtb = mk_modtype mp sign Univ.ContextSet.empty reso in
     let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in
     let impl = match alg with Some e -> Algebraic e | None -> Struct sign in
     { res_mtb with
       mod_mp = mp;
       mod_expr = impl;
-      mod_constraints = cst +++ cst' }
+      (** cst from module body typing, cst' from subtyping, 
+          and constraints from module type. *)
+      mod_constraints = Univ.ContextSet.add_constraints cst' (cst +++ res_mtb.mod_constraints) }
 
 let translate_module env mp inl = function
   |MType (params,ty) ->
@@ -318,12 +357,20 @@ let translate_module env mp inl = function
     let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
     finalize_module env mp t restype
 
-let rec translate_mse_incl env mp inl = function
+let rec translate_mse_inclmod env mp inl = function
   |MEident mp1 ->
     let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
     let sign = clean_bounded_mod_expr mb.mod_type in
-    sign,None,mb.mod_delta,Univ.Constraint.empty
+    sign,None,mb.mod_delta,Univ.ContextSet.empty
   |MEapply (fe,arg) ->
-    let ftrans = translate_mse_incl env mp inl fe in
+    let ftrans = translate_mse_inclmod env mp inl fe in
     translate_apply env inl ftrans arg (fun _ _ -> None)
-  |_ -> Modops.error_higher_order_include ()
+  |MEwith _ -> assert false (* No 'with' syntax for modules *)
+
+let translate_mse_incl is_mod env mp inl me =
+  if is_mod then
+    translate_mse_inclmod env mp inl me
+  else
+    let mtb = translate_modtype env mp inl ([],me) in
+    let sign = clean_bounded_mod_expr mtb.mod_type in
+    sign,None,mtb.mod_delta,mtb.mod_constraints
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index b39e8212..bc0e2020 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -30,17 +30,20 @@ val translate_modtype :
 *)
 
 type 'alg translation =
-  module_signature * 'alg option * delta_resolver * Univ.constraints
+  module_signature * 'alg option * delta_resolver * Univ.ContextSet.t
 
 val translate_mse :
   env -> module_path option -> inline -> module_struct_entry ->
     module_alg_expr translation
 
-val translate_mse_incl :
-  env -> module_path -> inline -> module_struct_entry ->
-    module_alg_expr translation
-
 val finalize_module :
   env -> module_path -> module_expression translation ->
   (module_type_entry * inline) option ->
   module_body
+
+(** [translate_mse_incl] translate the mse of a module or
+    module type given to an Include *)
+
+val translate_mse_incl :
+  bool -> env -> module_path -> inline -> module_struct_entry ->
+    module_alg_expr translation
diff --git a/kernel/modops.ml b/kernel/modops.ml
index d52fe611..cbb79633 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -67,7 +67,6 @@ type module_typing_error =
   | IncorrectWithConstraint of Label.t
   | GenerativeModuleExpected of Label.t
   | LabelMissing of Label.t * string
-  | HigherOrderInclude
 
 exception ModuleTypingError of module_typing_error
 
@@ -113,9 +112,6 @@ let error_generative_module_expected l =
 let error_no_such_label_sub l l1 =
   raise (ModuleTypingError (LabelMissing (l,l1)))
 
-let error_higher_order_include () =
-  raise (ModuleTypingError HigherOrderInclude)
-
 (** {6 Operations on functors } *)
 
 let is_functor = function
@@ -331,13 +327,15 @@ let strengthen_const mp_from l cb resolver =
     let kn = KerName.make2 mp_from l in
     let con = constant_of_delta_kn resolver kn in
     let u = 
-      if cb.const_polymorphic then 
-	Univ.UContext.instance cb.const_universes
+      if cb.const_polymorphic then
+	let u = Univ.UContext.instance cb.const_universes in
+	let s = Univ.make_instance_subst u in
+	  Univ.subst_univs_level_instance s u
       else Univ.Instance.empty
     in
       { cb with
 	const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
-	const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias (con,u))) }
+	const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
 
 let rec strengthen_mod mp_from mp_to mb =
   if mp_in_delta mb.mod_mp mb.mod_delta then mb
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 6fbcd81d..a335ad9b 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -126,7 +126,6 @@ type module_typing_error =
   | IncorrectWithConstraint of Label.t
   | GenerativeModuleExpected of Label.t
   | LabelMissing of Label.t * string
-  | HigherOrderInclude
 
 exception ModuleTypingError of module_typing_error
 
@@ -153,5 +152,3 @@ val error_incorrect_with_constraint : Label.t -> 'a
 val error_generative_module_expected : Label.t -> 'a
 
 val error_no_such_label_sub : Label.t->string->'a
-
-val error_higher_order_include : unit -> 'a
diff --git a/kernel/names.ml b/kernel/names.ml
index 480b37e8..ae2b3b63 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -453,6 +453,9 @@ module KNset = KNmap.Set
     - when user and canonical parts differ, we cannot be in a section
       anymore, hence the dirpath must be empty
     - two pairs with the same user part should have the same canonical part
+      in a given environment (though with backtracking, the hash-table can
+      contains pairs with same user part but different canonical part from
+      a previous state of the session)
 
    Note: since most of the time the canonical and user parts are equal,
    we handle this case with a particular constructor to spare some memory *)
@@ -504,7 +507,7 @@ module KerPair = struct
   let debug_print kp = str (debug_to_string kp)
 
   (** For ordering kernel pairs, both user or canonical parts may make
-      sense, according to your needs : user for the environments, canonical
+      sense, according to your needs: user for the environments, canonical
       for other uses (ex: non-logical things). *)
 
   module UserOrd = struct
@@ -521,16 +524,9 @@ module KerPair = struct
     let hash x = KerName.hash (canonical x)
   end
 
-  (** Default comparison is on the canonical part *)
+  (** Default (logical) comparison and hash is on the canonical part *)
   let equal = CanOrd.equal
-
-  (** Hash-consing : we discriminate only on the user part, since having
-      the same user part implies having the same canonical part
-      (invariant of the system). *)
-
-  let hash = function
-  | Same kn -> KerName.hash kn
-  | Dual (kn, _) -> KerName.hash kn
+  let hash = CanOrd.hash
 
   module Self_Hashcons =
     struct
@@ -539,8 +535,20 @@ module KerPair = struct
       let hashcons hkn = function
         | Same kn -> Same (hkn kn)
         | Dual (knu,knc) -> make (hkn knu) (hkn knc)
-      let equal x y = (user x) == (user y)
-      let hash = hash
+      let equal x y = (* physical comparison on subterms *)
+        x == y ||
+        match x,y with
+        | Same x, Same y -> x == y
+        | Dual (ux,cx), Dual (uy,cy) -> ux == uy && cx == cy
+        | (Same _ | Dual _), _ -> false
+      (** Hash-consing (despite having the same user part implies having
+          the same canonical part is a logical invariant of the system, it
+          is not necessarily an invariant in memory, so we treat kernel
+          names as they are syntactically for hash-consing) *)
+      let hash = function
+      | Same kn -> KerName.hash kn
+      | Dual (knu, knc) ->
+        Hashset.Combine.combine (KerName.hash knu) (KerName.hash knc)
     end
 
   module HashKP = Hashcons.Make(Self_Hashcons)
@@ -819,6 +827,10 @@ struct
   let map f (c, b as x) =
     let c' = f c in
       if c' == c then x else (c', b)
+
+  let to_string p = Constant.to_string (constant p)
+  let print p = Constant.print (constant p)
+
 end
 
 type projection = Projection.t
diff --git a/kernel/names.mli b/kernel/names.mli
index 92ee58f2..7cc44437 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -652,6 +652,10 @@ module Projection : sig
   val compare : t -> t -> int
     
   val map : (constant -> constant) -> t -> t
+
+  val to_string : t -> string
+  val print : t -> Pp.std_ppcmds
+
 end
 
 type projection = Projection.t
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index ada7ae73..98b2d6d2 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -195,7 +195,11 @@ module HashtblSymbol = Hashtbl.Make(HashedTypeSymbol)
 
 let symb_tbl = HashtblSymbol.create 211
 
-let clear_symb_tbl () = HashtblSymbol.clear symb_tbl
+let clear_symbols () = HashtblSymbol.clear symb_tbl
+
+type symbols = symbol array
+
+let empty_symbols = [||]
 
 let get_value tbl i =
   match tbl.(i) with
@@ -250,7 +254,7 @@ let push_symbol x =
 
 let symbols_tbl_name = Ginternal "symbols_tbl"
 
-let get_symbols_tbl () =
+let get_symbols () =
   let tbl = Array.make (HashtblSymbol.length symb_tbl) dummy_symb in
   HashtblSymbol.iter (fun x i -> tbl.(i) <- x) symb_tbl; tbl
 
@@ -477,7 +481,7 @@ and eq_mllam_branches gn1 gn2 n env1 env2 br1 br2 =
   in
   Array.equal eq_branch br1 br2
 
-(* hash_mllambda gn n env t computes the hash for t ignoring occurences of gn *)
+(* hash_mllambda gn n env t computes the hash for t ignoring occurrences of gn *)
 let rec hash_mllambda gn n env t =
   match t with
   | MLlocal ln -> combinesmall 1 (LNmap.find ln env)
@@ -975,7 +979,7 @@ let compile_prim decl cond paux =
 	let args = Array.map opt_prim_aux args in
 	app_prim (Coq_primitive(op,None)) args
 (*
-    TODO: check if this inling was useful
+    TODO: check if this inlining was useful
 	begin match op with
         | Int31lt -> 
            if Sys.word_size = 64 then
@@ -2008,16 +2012,20 @@ let rec compile_deps env sigma prefix ~interactive init t =
   match kind_of_term t with
   | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind
   | Const c ->
-      let c,u = get_allias env c in
+      let c,u = get_alias env c in
       let cb,(nameref,_) = lookup_constant_key c env in
       let (_, (_, const_updates)) = init in
       if is_code_loaded ~interactive nameref
         || (Cmap_env.mem c const_updates)
       then init
       else
-      let comp_stack, (mind_updates, const_updates) = match cb.const_body with
-        | Def t ->
+      let comp_stack, (mind_updates, const_updates) =
+	match cb.const_proj, cb.const_body with
+        | None, Def t ->
 	   compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t)
+	| Some pb, _ ->
+	   let mind = pb.proj_ind in
+	   compile_mind_deps env prefix ~interactive init mind
         | _ -> init
       in
       let code, name =
@@ -2054,7 +2062,7 @@ let mk_internal_let s code =
 
 (* ML Code for conversion function *)
 let mk_conv_code env sigma prefix t1 t2 =
-  clear_symb_tbl ();
+  clear_symbols ();
   clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
@@ -2076,12 +2084,12 @@ let mk_conv_code env sigma prefix t1 t2 =
   let setref2 = Glet(Ginternal "_", MLsetref("rt2",g2)) in
   let gl = List.rev (setref2 :: setref1 :: t2 :: t1 :: gl) in
   let header = Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_symbols"),
       [|MLglobal (Ginternal "()")|])) in
   header::gl, (mind_updates, const_updates)
 
 let mk_norm_code env sigma prefix t =
-  clear_symb_tbl ();
+  clear_symbols ();
   clear_global_tbl ();
   let gl, (mind_updates, const_updates) =
     let init = ([], empty_updates) in
@@ -2094,14 +2102,14 @@ let mk_norm_code env sigma prefix t =
   let setref = Glet(Ginternal "_", MLsetref("rt1",g1)) in
   let gl = List.rev (setref :: t1 :: gl) in
   let header = Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_symbols"),
       [|MLglobal (Ginternal "()")|])) in
   header::gl, (mind_updates, const_updates)
 
 let mk_library_header dir =
   let libname = Format.sprintf "(str_decode \"%s\")" (str_encode dir) in
   [Glet(Ginternal "symbols_tbl",
-    MLapp (MLglobal (Ginternal "get_library_symbols_tbl"),
+    MLapp (MLglobal (Ginternal "get_library_native_symbols"),
     [|MLglobal (Ginternal libname)|]))]
 
 let update_location (r,v) = r := v
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 893db92d..5d4c9e1e 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -22,29 +22,33 @@ val pp_global : Format.formatter -> global -> unit
 
 val mk_open : string -> global
 
+(* Precomputed values for a compilation unit *)
 type symbol
+type symbols
 
-val clear_symb_tbl : unit -> unit
+val empty_symbols : symbols
 
-val get_value : symbol array -> int -> Nativevalues.t
+val clear_symbols : unit -> unit
 
-val get_sort : symbol array -> int -> sorts
+val get_value : symbols -> int -> Nativevalues.t
 
-val get_name : symbol array -> int -> name
+val get_sort : symbols -> int -> sorts
 
-val get_const : symbol array -> int -> constant
+val get_name : symbols -> int -> name
 
-val get_match : symbol array -> int -> Nativevalues.annot_sw
+val get_const : symbols -> int -> constant
 
-val get_ind : symbol array -> int -> inductive
+val get_match : symbols -> int -> Nativevalues.annot_sw
 
-val get_meta : symbol array -> int -> metavariable
+val get_ind : symbols -> int -> inductive
 
-val get_evar : symbol array -> int -> existential
+val get_meta : symbols -> int -> metavariable
 
-val get_level : symbol array -> int -> Univ.Level.t
+val get_evar : symbols -> int -> existential
 
-val get_symbols_tbl : unit -> symbol array
+val get_level : symbols -> int -> Univ.Level.t
+
+val get_symbols : unit -> symbols
 
 type code_location_update
 type code_location_updates
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 75a3fc45..0242fd46 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -16,17 +16,21 @@ open Nativecode
 
 (** This module implements the conversion test by compiling to OCaml code *)
 
-let rec conv_val env pb lvl cu v1 v2 = 
-  if v1 == v2 then ()
+let rec conv_val env pb lvl v1 v2 cu =
+  if v1 == v2 then cu
   else
     match kind_of_value v1, kind_of_value v2 with
-    | Vaccu k1, Vaccu k2 ->
-	conv_accu env pb lvl cu k1 k2
     | Vfun f1, Vfun f2 ->
 	let v = mk_rel_accu lvl in
-	conv_val env CONV (lvl+1) cu (f1 v) (f2 v)
+	conv_val env CONV (lvl+1) (f1 v) (f2 v) cu
+    | Vfun f1, _ ->
+	conv_val env CONV lvl v1 (fun x -> v2 x) cu
+    | _, Vfun f2 ->
+	conv_val env CONV lvl (fun x -> v1 x) v2 cu
+    | Vaccu k1, Vaccu k2 ->
+	conv_accu env pb lvl k1 k2 cu
     | Vconst i1, Vconst i2 -> 
-	if not (Int.equal i1 i2) then raise NotConvertible
+	if Int.equal i1 i2 then cu else raise NotConvertible
     | Vblock b1, Vblock b2 ->
 	let n1 = block_size b1 in
         let n2 = block_size b2 in
@@ -34,77 +38,81 @@ let rec conv_val env pb lvl cu v1 v2 =
 	  raise NotConvertible;
 	let rec aux lvl max b1 b2 i cu =
 	  if Int.equal i max then 
-	    conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i)
+	    conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu
 	  else
-	      (conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i);
-	    aux lvl max b1 b2 (i+1) cu)
+	    let cu = conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in
+	    aux lvl max b1 b2 (i+1) cu
 	in
 	aux lvl (n1-1) b1 b2 0 cu
-    | Vfun f1, _ -> 
-	conv_val env CONV lvl cu v1 (fun x -> v2 x)
-    | _, Vfun f2 ->
-	conv_val env CONV lvl cu (fun x -> v1 x) v2
-    | _, _ -> raise NotConvertible
+    | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible
 
-and conv_accu env pb lvl cu k1 k2 = 
+and conv_accu env pb lvl k1 k2 cu =
   let n1 = accu_nargs k1 in
   let n2 = accu_nargs k2 in
   if not (Int.equal n1 n2) then raise NotConvertible;
   if Int.equal n1 0 then 
     conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu
   else
-    (conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu;
-    List.iter2 (conv_val env CONV lvl cu) (args_of_accu k1) (args_of_accu k2))
+    let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in
+    List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu
 
 and conv_atom env pb lvl a1 a2 cu =
-  if a1 == a2 then ()
+  if a1 == a2 then cu
   else
     match a1, a2 with
+    | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false
     | Arel i1, Arel i2 -> 
-	if not (Int.equal i1 i2) then raise NotConvertible
-    | Aind ind1, Aind ind2 ->
-	if not (eq_puniverses eq_ind ind1 ind2) then raise NotConvertible
-    | Aconstant c1, Aconstant c2 ->
-	if not (eq_puniverses eq_constant c1 c2) then raise NotConvertible
+	if Int.equal i1 i2 then cu else raise NotConvertible
+    | Aind (ind1,u1), Aind (ind2,u2) ->
+       if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu
+       else raise NotConvertible
+    | Aconstant (c1,u1), Aconstant (c2,u2) ->
+       if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu
+       else raise NotConvertible
     | Asort s1, Asort s2 -> 
-        check_sort_cmp_universes env pb s1 s2 cu
+        sort_cmp_universes env pb s1 s2 cu
     | Avar id1, Avar id2 ->
-	if not (Id.equal id1 id2) then raise NotConvertible
+	if Id.equal id1 id2 then cu else raise NotConvertible
     | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) ->
 	if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible;
-	conv_accu env CONV lvl cu ac1 ac2;
+	let cu = conv_accu env CONV lvl ac1 ac2 cu in
 	let tbl = a1.asw_reloc in
 	let len = Array.length tbl in
-	if Int.equal len 0 then conv_val env CONV lvl cu p1 p2
+	if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu
 	else begin
-	  conv_val env CONV lvl cu p1 p2;
-	  let max = len - 1 in
-	  let rec aux i =
-	    let tag,arity = tbl.(i) in
-	    let ci = 
-	      if Int.equal arity 0 then mk_const tag
-	      else mk_block tag (mk_rels_accu lvl arity) in
-	    let bi1 = bs1 ci and bi2 = bs2 ci in
-	    if Int.equal i max then conv_val env CONV (lvl + arity) cu bi1 bi2
-	    else (conv_val env CONV (lvl + arity) cu bi1 bi2; aux (i+1)) in
-	  aux 0
+	    let cu = conv_val env CONV lvl p1 p2 cu in
+	    let max = len - 1 in
+	    let rec aux i cu =
+	      let tag,arity = tbl.(i) in
+	      let ci =
+		if Int.equal arity 0 then mk_const tag
+		else mk_block tag (mk_rels_accu lvl arity) in
+	      let bi1 = bs1 ci and bi2 = bs2 ci in
+	      if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu
+	      else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in
+	    aux 0 cu
 	  end
     | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) ->
 	if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible;
-	if f1 == f2 then ()
+	if f1 == f2 then cu
 	else conv_fix env lvl t1 f1 t2 f2 cu
     | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)),
       (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) ->
 	if not (Int.equal s1 s2) then raise NotConvertible;
-	if f1 == f2 then ()
+	if f1 == f2 then cu
 	else
 	  if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible
 	  else conv_fix env lvl t1 f1 t2 f2 cu 
     | Aprod(_,d1,c1), Aprod(_,d2,c2) ->
-	conv_val env CONV lvl cu d1 d2;
-	let v = mk_rel_accu lvl in
-	conv_val env pb (lvl + 1) cu (d1 v) (d2 v)
-    | _, _ -> raise NotConvertible
+       let cu = conv_val env CONV lvl d1 d2 cu in
+       let v = mk_rel_accu lvl in
+       conv_val env pb (lvl + 1) (d1 v) (d2 v) cu
+    | Aproj(p1,ac1), Aproj(p2,ac2) ->
+       if not (Constant.equal p1 p2) then raise NotConvertible
+       else conv_accu env CONV lvl ac1 ac2 cu
+    | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
+    | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
+    | Aproj _, _ -> raise NotConvertible
 
 (* Precondition length t1 = length f1 = length f2 = length t2 *)
 and conv_fix env lvl t1 f1 t2 f2 cu =
@@ -112,22 +120,15 @@ and conv_fix env lvl t1 f1 t2 f2 cu =
   let max = len - 1 in
   let fargs = mk_rels_accu lvl len in
   let flvl = lvl + len in
-  let rec aux i =
-    conv_val env CONV lvl cu t1.(i) t2.(i);
+  let rec aux i cu =
+    let cu = conv_val env CONV lvl t1.(i) t2.(i) cu in
     let fi1 = napply f1.(i) fargs in
     let fi2 = napply f2.(i) fargs in
-    if Int.equal i max then conv_val env CONV flvl cu fi1 fi2
-    else (conv_val env CONV flvl cu fi1 fi2; aux (i+1)) in
-  aux 0
+    if Int.equal i max then conv_val env CONV flvl fi1 fi2 cu
+    else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in
+  aux 0 cu
 
-let native_conv pb sigma env t1 t2 =
-  if !Flags.no_native_compiler then begin
-    let msg = "Native compiler is disabled, "^
-    "falling back to VM conversion test." in
-    Pp.msg_warning (Pp.str msg);
-    vm_conv pb env t1 t2
-  end
-  else
+let native_conv_gen pb sigma env univs t1 t2 =
   let penv = Environ.pre_env env in 
   let ml_filename, prefix = get_ml_filename () in
   let code, upds = mk_conv_code penv sigma prefix t1 t2 in
@@ -141,8 +142,25 @@ let native_conv pb sigma env t1 t2 =
         let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in
         if !Flags.debug then Pp.msg_debug (Pp.str time_info);
         (* TODO change 0 when we can have deBruijn *)
-        conv_val env pb 0 (Environ.universes env) !rt1 !rt2
+        fst (conv_val env pb 0 !rt1 !rt2 univs)
       end
   | _ -> anomaly (Pp.str "Compilation failure") 
 
-let _ = set_nat_conv native_conv
+(* Wrapper for [native_conv] above *)
+let native_conv cv_pb sigma env t1 t2 =
+  if Coq_config.no_native_compiler then begin
+    let msg = "Native compiler is disabled, falling back to VM conversion test." in
+    Pp.msg_warning (Pp.str msg);
+    vm_conv cv_pb env t1 t2
+  end
+  else
+  let univs = Environ.universes env in
+  let b =
+    if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2
+    else Constr.eq_constr_univs univs t1 t2
+  in
+  if not b then
+    let univs = (univs, checked_universes) in
+    let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in
+    let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in
+    let _ = native_conv_gen cv_pb sigma env univs t1 t2 in ()
diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
index 318a7d83..4dddb9fd 100644
--- a/kernel/nativeconv.mli
+++ b/kernel/nativeconv.mli
@@ -12,3 +12,7 @@ open Nativelambda
 (** This module implements the conversion test by compiling to OCaml code *)
 
 val native_conv : conv_pb -> evars -> types conversion_function
+
+(** A conversion function parametrized by a universe comparator. Used outside of
+    the kernel. *)
+val native_conv_gen : conv_pb -> evars -> (types, 'a) generic_conversion_function
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 383f8102..4d033bc9 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -277,7 +277,7 @@ and reduce_lapp substf lids body substa largs =
   | [], _::_ -> simplify_app substf body substa (Array.of_list largs)
 
 
-(* [occurence kind k lam]:
+(* [occurrence kind k lam]:
    If [kind] is [true] return [true] if the variable [k] does not appear in 
    [lam], return [false] if the variable appear one time and not
    under a lambda, a fixpoint, a cofixpoint; else raise Not_found.
@@ -285,7 +285,7 @@ and reduce_lapp substf lids body substa largs =
    else raise [Not_found]
 *)
 
-let rec occurence k kind lam =   
+let rec occurrence k kind lam =
   match lam with
   | Lrel (_,n) -> 
       if Int.equal n k then 
@@ -294,35 +294,35 @@ let rec occurence k kind lam =
   | Lvar _  | Lconst _  | Lproj _ | Luint _ | Lval _ | Lsort _ | Lind _
   | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind
   | Lprod(dom, codom) ->
-      occurence k (occurence k kind dom) codom
+      occurrence k (occurrence k kind dom) codom
   | Llam(ids,body) ->
-      let _ = occurence (k+Array.length ids) false body in kind
+      let _ = occurrence (k+Array.length ids) false body in kind
   | Llet(_,def,body) ->
-      occurence (k+1) (occurence k kind def) body
+      occurrence (k+1) (occurrence k kind def) body
   | Lapp(f, args) ->
-      occurence_args k (occurence k kind f) args
+      occurrence_args k (occurrence k kind f) args
   | Lprim(_,_,_,args) | Lmakeblock(_,_,_,args) ->
-      occurence_args k kind args
+      occurrence_args k kind args
   | Lcase(_,t,a,br) ->
-      let kind = occurence k (occurence k kind t) a in
+      let kind = occurrence k (occurrence k kind t) a in
       let r = ref kind in
       Array.iter (fun (_,ids,c) -> 
-	r := occurence (k+Array.length ids) kind c && !r) br;
+	r := occurrence (k+Array.length ids) kind c && !r) br;
       !r 
   | Lif (t, bt, bf) ->
-      let kind = occurence k kind t in
-      kind && occurence k kind bt && occurence k kind bf
+      let kind = occurrence k kind t in
+      kind && occurrence k kind bt && occurrence k kind bf
   | Lfix(_,(ids,ltypes,lbodies)) 
   | Lcofix(_,(ids,ltypes,lbodies)) ->
-      let kind = occurence_args k kind ltypes in
-      let _ = occurence_args (k+Array.length ids) false lbodies in
+      let kind = occurrence_args k kind ltypes in
+      let _ = occurrence_args (k+Array.length ids) false lbodies in
       kind 
 
-and occurence_args k kind args = 
-  Array.fold_left (occurence k) kind args
+and occurrence_args k kind args =
+  Array.fold_left (occurrence k) kind args
     
 let occur_once lam = 
-  try let _ = occurence 1 true lam in true
+  try let _ = occurrence 1 true lam in true
   with Not_found -> false
       
 (* [remove_let lam] remove let expression in [lam] if the variable is *)
@@ -373,13 +373,13 @@ let makeblock env cn u tag args =
 
 (* Translation of constants *)
 
-let rec get_allias env (kn, u as p) =
+let rec get_alias env (kn, u as p) =
   let tps = (lookup_constant kn env).const_body_code in
     match tps with
     | None -> p
     | Some tps ->
        match Cemitcodes.force tps with
-       | Cemitcodes.BCallias kn' -> get_allias env kn'
+       | Cemitcodes.BCalias kn' -> get_alias env (kn', u)
        | _ -> p
 
 (*i Global environment *)
@@ -651,7 +651,7 @@ let rec lambda_of_constr env sigma c =
 and lambda_of_app env sigma f args =
   match kind_of_term f with
   | Const (kn,u as c) ->
-      let kn,u = get_allias !global_env c in
+      let kn,u = get_alias !global_env c in
       let cb = lookup_constant kn !global_env in
       (try
           let prefix = get_const_prefix !global_env kn in
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index ccf2888b..3b6fafbb 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -26,7 +26,7 @@ val mk_lazy : lambda -> lambda
 
 val get_mind_prefix : env -> mutual_inductive -> string
 
-val get_allias : env -> pconstant -> pconstant
+val get_alias : env -> pconstant -> pconstant
 
 val lambda_of_constr : env -> evars -> Constr.constr -> lambda
 
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 605c1225..b2142b43 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -94,7 +94,10 @@ let compile_library dir code fn =
   let basename = Filename.basename fn in
   let dirname = Filename.dirname fn in
   let dirname = dirname / output_dir in
-  if not (Sys.file_exists dirname) then Unix.mkdir dirname 0o755;
+  let () =
+    try Unix.mkdir dirname 0o755
+    with Unix.Unix_error (Unix.EEXIST, _, _) -> ()
+  in
   let fn = dirname / basename in
   write_ml_code fn ~header code;
   let r = fst (call_compiler fn) in
@@ -102,22 +105,25 @@ let compile_library dir code fn =
   r
 
 (* call_linker links dynamically the code for constants in environment or a  *)
-(* conversion test. Silently fails if the file does not exist in bytecode    *)
-(* mode, since the standard library is not compiled to bytecode with default *)
-(* settings.                                                                 *)
+(* conversion test. *)
 let call_linker ?(fatal=true) prefix f upds =
   rt1 := dummy_value ();
   rt2 := dummy_value ();
-  if Dynlink.is_native || Sys.file_exists f then
+  if not (Sys.file_exists f) then
+    begin
+      let msg = "Cannot find native compiler file " ^ f in
+      if fatal then Errors.error msg
+      else if !Flags.debug then Pp.msg_debug (Pp.str msg)
+    end
+  else
   (try
     if Dynlink.is_native then Dynlink.loadfile f else !load_obj f;
     register_native_file prefix
-   with | Dynlink.Error e ->
-          let msg = "Dynlink error, " ^ Dynlink.error_message e in
-          if fatal then anomaly (Pp.str msg) else Pp.msg_warning (Pp.str msg)
-        | e when Errors.noncritical e ->
-          if fatal then anomaly (Errors.print e)
-	  else Pp.msg_warning (Errors.print_no_report e));
+   with Dynlink.Error e as exn ->
+     let exn = Errors.push exn in
+     let msg = "Dynlink error, " ^ Dynlink.error_message e in
+     if fatal then (Pp.msg_error (Pp.str msg); iraise exn)
+     else if !Flags.debug then Pp.msg_debug (Pp.str msg));
   match upds with Some upds -> update_locations upds | _ -> ()
 
 let link_library ~prefix ~dirname ~basename =
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 0b8662ff..443cd8c2 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -62,12 +62,12 @@ let dump_library mp dp env mod_expr =
       let prefix = mod_uid_of_dirpath dp ^ "." in
       let t0 = Sys.time () in
       clear_global_tbl ();
-      clear_symb_tbl ();
+      clear_symbols ();
       let mlcode =
         List.fold_left (translate_field prefix mp env) [] struc
       in
       let t1 = Sys.time () in
       let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
       let mlcode = add_header_comment (List.rev mlcode) time_info in
-      mlcode, get_symbols_tbl ()
+      mlcode, get_symbols ()
   | _ -> assert false
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index a66fb715..29368d14 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -14,4 +14,4 @@ open Nativecode
 compiler *)
 
 val dump_library : module_path -> dir_path -> env -> module_signature ->
-  global list * symbol array
+  global list * symbols
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index e4a77999..40bef4bc 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -10,7 +10,7 @@ open Names
 open Errors
 open Util
 
-(** This modules defines the representation of values internally used by
+(** This module defines the representation of values internally used by
 the native compiler *)
 
 type t = t -> t
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 9f4361f4..badb15b5 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -43,7 +43,10 @@ let set_indirect_univ_accessor f = (get_univ := f)
 let create cu = Direct ([],cu)
 
 let turn_indirect dp o (prfs,odp) = match o with
-  | Indirect _ -> Errors.anomaly (Pp.str "Already an indirect opaque")
+  | Indirect (_,_,i) ->
+      if not (Int.Map.mem i prfs)
+      then Errors.anomaly (Pp.str "Indirect in a different table")
+      else Errors.anomaly (Pp.str "Already an indirect opaque")
   | Direct (d,cu) ->
       let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
       let id = Int.Map.cardinal prfs in
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 557ed3d7..5f3f559a 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -46,8 +46,7 @@ type globals = {
 
 type stratification = {
   env_universes : universes;
-  env_engagement : engagement option;
-  env_type_in_type : bool
+  env_engagement : engagement
 }
 
 type val_kind =
@@ -95,8 +94,7 @@ let empty_env = {
   env_nb_rel = 0;
   env_stratification = {
     env_universes = initial_universes;
-    env_engagement = None;
-    env_type_in_type = false};
+    env_engagement = (PredicativeSet,StratifiedType) };
   env_conv_oracle = Conv_oracle.empty;
   retroknowledge = Retroknowledge.initial_retroknowledge;
   indirect_pterms = Opaqueproof.empty_opaquetab }
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 03ac41b4..0ce0bed2 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -33,8 +33,7 @@ type globals = {
 
 type stratification = {
   env_universes : universes;
-  env_engagement : engagement option;
-  env_type_in_type : bool
+  env_engagement : engagement
 }
 
 type lazy_val
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b09367dd..892557ac 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -26,8 +26,6 @@ open Environ
 open Closure
 open Esubst
 
-let left2right = ref false
-
 let rec is_empty_stack = function
   [] -> true
   | Zupdate _::s -> is_empty_stack s
@@ -175,7 +173,7 @@ let is_cumul = function CUMUL -> true | CONV -> false
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
-    compare_instances: bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+    compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
   } 
 
 type 'a universe_state = 'a * 'a universe_compare
@@ -187,8 +185,10 @@ type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.co
 let sort_cmp_universes env pb s0 s1 (u, check) =
   (check.compare env pb s0 s1 u, check)
 
-let convert_instances flex u u' (s, check) =
-  (check.compare_instances flex u u' s, check)
+(* [flex] should be true for constants, false for inductive types and
+   constructors. *)
+let convert_instances ~flex u u' (s, check) =
+  (check.compare_instances ~flex u u' s, check)
 
 let conv_table_key infos k1 k2 cuniv =
   if k1 == k2 then cuniv else
@@ -198,7 +198,7 @@ let conv_table_key infos k1 k2 cuniv =
     else 
       let flex = evaluable_constant cst (info_env infos) 
 	&& RedFlags.red_set (info_flags infos) (RedFlags.fCONST cst)
-      in convert_instances flex u u' cuniv
+      in convert_instances ~flex u u' cuniv
   | VarKey id, VarKey id' when Id.equal id id' -> cuniv
   | RelKey n, RelKey n' when Int.equal n n' -> cuniv
   | _ -> raise NotConvertible
@@ -210,9 +210,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv =
           let cu1 = cmp_rec s1 s2 cuniv in
           (match (z1,z2) with
             | (Zlapp a1,Zlapp a2) -> 
-	      if !left2right then
-		Array.fold_left2 (fun cu x y -> f x y cu) cu1 a1 a2
-	      else Array.fold_right2 f a1 a2 cu1
+	       Array.fold_right2 f a1 a2 cu1
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
 	      if not (eq_constant c1 c2) then 
 		raise NotConvertible
@@ -594,7 +592,7 @@ let check_sort_cmp_universes env pb s0 s1 univs =
 let checked_sort_cmp_universes env pb s0 s1 univs =
   check_sort_cmp_universes env pb s0 s1 univs; univs
 
-let check_convert_instances _flex u u' univs =
+let check_convert_instances ~flex u u' univs =
   if Univ.Instance.check_eq univs u u' then univs
   else raise NotConvertible
 
@@ -634,10 +632,10 @@ let infer_cmp_universes env pb s0 s1 univs =
 	| CONV -> infer_eq univs u1 u2)
         else univs
 
-let infer_convert_instances flex u u' (univs,cstrs) =
+let infer_convert_instances ~flex u u' (univs,cstrs) =
   (univs, Univ.enforce_eq_instances u u' cstrs)
 
-let infered_universes : (Univ.universes * Univ.Constraint.t) universe_compare = 
+let inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare =
   { compare = infer_cmp_universes;
     compare_instances = infer_convert_instances }
 
@@ -670,7 +668,7 @@ let trans_conv_universes ?(l2r=false) ?(evars=fun _->None) reds =
 let trans_conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = 
   trans_fconv_universes reds CUMUL l2r evars
 
-let fconv = trans_fconv (Id.Pred.full, Cpred.full)
+let fconv = trans_fconv full_transparent_state
 
 let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None)
 let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars
@@ -685,7 +683,7 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 =
     v1
     v2
 
-let generic_conv cv_pb l2r evars reds env univs t1 t2 =
+let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
   let (s, _) = 
     clos_fconv reds cv_pb l2r evars env univs t1 t2 
   in s
@@ -697,7 +695,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 =
   in
     if b then cstrs
     else
-      let univs = ((univs, Univ.Constraint.empty), infered_universes) in
+      let univs = ((univs, Univ.Constraint.empty), inferred_universes) in
       let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in
 	cstrs
 
@@ -716,39 +714,19 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta
     env univs t1 t2 = 
   infer_conv_universes CUMUL l2r evars ts env univs t1 t2
 
-(* option for conversion *)
-let nat_conv = ref (fun cv_pb sigma ->
-		    fconv cv_pb false (sigma.Nativelambda.evars_val))
-let set_nat_conv f = nat_conv := f
-
-let native_conv cv_pb sigma env t1 t2 =
-  if eq_constr t1 t2 then ()
-  else begin
-    let t1 = (it_mkLambda_or_LetIn t1 (rel_context env)) in
-    let t2 = (it_mkLambda_or_LetIn t2 (rel_context env)) in
-    !nat_conv cv_pb sigma env t1 t2 
-  end
-
+(* This reference avoids always having to link C code with the kernel *)
 let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
 let set_vm_conv f = vm_conv := f
 let vm_conv cv_pb env t1 t2 =
   try
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
-      (* If compilation fails, fall-back to closure conversion *)
-      fconv cv_pb false (fun _->None) env t1 t2
-
-
-let default_conv = ref (fun cv_pb ?(l2r=false) -> fconv cv_pb l2r (fun _->None))
-
-let set_default_conv f = default_conv := f
+    (Pp.msg_warning
+      (Pp.str "Bytecode compilation failed, falling back to default conversion");
+     fconv cv_pb false (fun _->None) env t1 t2)
 
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
-  try
-    !default_conv ~l2r cv_pb env t1 t2
-  with Not_found | Invalid_argument _ ->
-      (* If compilation fails, fall-back to closure conversion *)
-      fconv cv_pb false (fun _->None) env t1 t2
+    fconv cv_pb false (fun _ -> None) env t1 t2
 
 let default_conv_leq = default_conv CUMUL
 (*
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 6ced5c49..0df26d62 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -10,8 +10,6 @@ open Term
 open Context
 open Environ
 
-val left2right : bool ref
-
 (***********************************************************************
   s Reduction functions *)
 
@@ -39,7 +37,7 @@ type conv_pb = CONV | CUMUL
 type 'a universe_compare = 
   { (* Might raise NotConvertible *)
     compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
-    compare_instances: bool (* Instance of a flexible constant? *) -> 
+    compare_instances: flex:bool -> 
 		       Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
   } 
 
@@ -49,14 +47,16 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a
 
 type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints
 
-val check_sort_cmp_universes :
-  env -> conv_pb -> sorts -> sorts -> Univ.universes -> unit
+val sort_cmp_universes : env -> conv_pb -> sorts -> sorts ->
+  'a * 'a universe_compare -> 'a * 'a universe_compare
 
-(* val sort_cmp : *)
-(*     conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *)
+(* [flex] should be true for constants, false for inductive types and
+constructors. *)
+val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t ->
+  'a * 'a universe_compare -> 'a * 'a universe_compare
 
-(* val conv_sort      : sorts conversion_function *)
-(* val conv_sort_leq  : sorts conversion_function *)
+val checked_universes : Univ.universes universe_compare
+val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare
 
 val trans_conv_cmp       : ?l2r:bool -> conv_pb -> constr trans_conversion_function
 val trans_conv           :
@@ -77,23 +77,20 @@ val conv_leq       :
 val conv_leq_vecti :
   ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function
 
+(** These conversion functions are used by module subtyping, which needs to infer
+    universe constraints inside the kernel *)
 val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> 
   ?ts:Names.transparent_state -> constr infer_conversion_function
 val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> 
   ?ts:Names.transparent_state -> types infer_conversion_function
 
-val generic_conv : conv_pb -> bool -> (existential->constr option) -> 
+val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) ->
   Names.transparent_state -> (constr,'a) generic_conversion_function
 
 (** option for conversion *)
 val set_vm_conv : (conv_pb -> types conversion_function) -> unit
 val vm_conv : conv_pb -> types conversion_function
 
-val set_nat_conv :
-  (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit
-val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function
-
-val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit
 val default_conv     : conv_pb -> ?l2r:bool -> types conversion_function
 val default_conv_leq : ?l2r:bool -> types conversion_function
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d762a246..e0a07dcc 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -81,8 +81,7 @@ open Declarations
       These fields could be deduced from [revstruct], but they allow faster
       name freshness checks.
  - [univ] and [future_cst] : current and future universe constraints
- - [engagement] : are we Set-impredicative?
- - [type_in_type] : does the universe hierarchy collapse?
+ - [engagement] : are we Set-impredicative? does the universe hierarchy collapse?
  - [required] : names and digests of Require'd libraries since big-bang.
       This field will only grow
  - [loads] : list of libraries Require'd inside the current module.
@@ -119,13 +118,13 @@ type safe_environment =
     revstruct : structure_body;
     modlabels : Label.Set.t;
     objlabels : Label.Set.t;
-    univ : Univ.constraints;
-    future_cst : Univ.constraints Future.computation list;
+    univ : Univ.ContextSet.t;
+    future_cst : Univ.ContextSet.t Future.computation list;
     engagement : engagement option;
-    type_in_type : bool;
     required : vodigest DPMap.t;
     loads : (module_path * module_body) list;
-    local_retroknowledge : Retroknowledge.action list }
+    local_retroknowledge : Retroknowledge.action list;
+    native_symbols : Nativecode.symbols DPMap.t }
 
 and modvariant =
   | NONE
@@ -149,12 +148,12 @@ let empty_environment =
     modlabels = Label.Set.empty;
     objlabels = Label.Set.empty;
     future_cst = [];
-    univ = Univ.Constraint.empty;
+    univ = Univ.ContextSet.empty;
     engagement = None;
-    type_in_type = false;
     required = DPMap.empty;
     loads = [];
-    local_retroknowledge = [] }
+    local_retroknowledge = [];
+    native_symbols = DPMap.empty }
 
 let is_initial senv =
   match senv.revstruct, senv.modvariant with
@@ -182,16 +181,20 @@ let set_engagement c senv =
 
 (** Check that the engagement [c] expected by a library matches
     the current (initial) one *)
-let check_engagement env c =
-  match Environ.engagement env, c with
-  | None, Some ImpredicativeSet ->
-    Errors.error "Needs option -impredicative-set."
-  | _ -> ()
-
-let set_type_in_type senv = 
-  { senv with
-    env = Environ.set_type_in_type senv.env;
-    type_in_type = true }
+let check_engagement env (expected_impredicative_set,expected_type_in_type) =
+  let impredicative_set,type_in_type = Environ.engagement env in
+  begin
+    match impredicative_set, expected_impredicative_set with
+    | PredicativeSet, ImpredicativeSet ->
+        Errors.error "Needs option -impredicative-set."
+    | _ -> ()
+  end;
+  begin
+    match type_in_type, expected_type_in_type with
+    | StratifiedType, TypeInType ->
+        Errors.error "Needs option -type-in-type."
+    | _ -> ()
+  end
 
 (** {6 Stm machinery } *)
 
@@ -204,36 +207,79 @@ let get_opaque_body env cbo =
         (Opaqueproof.force_proof (Environ.opaque_tables env) opaque,
          Opaqueproof.force_constraints (Environ.opaque_tables env) opaque)
 
-let sideff_of_con env c =
+type private_constant = Entries.side_effect
+type private_constants = private_constant list
+
+type private_constant_role = Term_typing.side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+let empty_private_constants = []
+let add_private x xs = x :: xs
+let concat_private xs ys = xs @ ys
+let mk_pure_proof = Term_typing.mk_pure_proof
+let inline_private_constants_in_constr = Term_typing.inline_side_effects
+let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects
+let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
+
+let constant_entry_of_private_constant = function
+  | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
+      [ kn, Term_typing.constant_entry_of_side_effect cb eff_env ]
+  | { Entries.eff = Entries.SEscheme (l,_) } ->
+      List.map (fun (_,kn,cb,eff_env) ->
+        kn, Term_typing.constant_entry_of_side_effect cb eff_env) l
+
+let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
-  SEsubproof (c, cbo, get_opaque_body env.env cbo)
-let sideff_of_scheme kind env cl =
-  SEscheme(
-    List.map (fun (i,c) ->
-      let cbo = Environ.lookup_constant c env.env in
-      i, c, cbo, get_opaque_body env.env cbo) cl,
-    kind)
+  { Entries.from_env = Ephemeron.create env.revstruct;
+    Entries.eff      = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) }
+
+let private_con_of_scheme ~kind env cl =
+  { Entries.from_env = Ephemeron.create env.revstruct;
+    Entries.eff      = Entries.SEscheme(
+      List.map (fun (i,c) ->
+        let cbo = Environ.lookup_constant c env.env in
+        i, c, cbo, get_opaque_body env.env cbo) cl,
+      kind) }
+
+let universes_of_private eff =
+  let open Declarations in
+  List.fold_left (fun acc { Entries.eff } ->
+     match eff with
+     | Entries.SEscheme (l,s) ->
+        List.fold_left (fun acc (_,_,cb,c) ->
+          let acc = match c with
+            | `Nothing -> acc
+            | `Opaque (_, ctx) -> ctx :: acc in
+          if cb.const_polymorphic then acc
+          else (Univ.ContextSet.of_context cb.const_universes) :: acc)
+        acc l
+     | Entries.SEsubproof (c, cb, e) ->
+	if cb.const_polymorphic then acc
+	else Univ.ContextSet.of_context cb.const_universes :: acc)
+   [] eff
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
 
 type constraints_addition =
-  Now of Univ.constraints | Later of Univ.constraints Future.computation
+  | Now of bool * Univ.ContextSet.t
+  | Later of Univ.ContextSet.t Future.computation
 
 let add_constraints cst senv =
   match cst with
   | Later fc -> 
     {senv with future_cst = fc :: senv.future_cst}
-  | Now cst ->
+  | Now (poly,cst) ->
   { senv with
-    env = Environ.add_constraints cst senv.env;
-    univ = Univ.Constraint.union cst senv.univ }
+    env = Environ.push_context_set ~strict:(not poly) cst senv.env;
+    univ = Univ.ContextSet.union cst senv.univ }
 
 let add_constraints_list cst senv =
-  List.fold_right add_constraints cst senv
+  List.fold_left (fun acc c -> add_constraints c acc) senv cst
 
-let push_context_set ctx = add_constraints (Now (Univ.ContextSet.constraints ctx))
-let push_context ctx = add_constraints (Now (Univ.UContext.constraints ctx))
+let push_context_set poly ctx = add_constraints (Now (poly,ctx))
+let push_context poly ctx = add_constraints (Now (poly,Univ.ContextSet.of_context ctx))
 
 let is_curmod_library senv =
   match senv.modvariant with LIBRARY -> true | _ -> false
@@ -243,9 +289,11 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e =
   List.fold_left
     (fun e fc ->
        if Future.UUIDSet.mem (Future.uuid fc) except then e
-       else add_constraints (Now (Future.join fc)) e)
+       else add_constraints (Now (false, Future.join fc)) e)
     {e with future_cst = []} e.future_cst
 
+let is_joined_environment e = List.is_empty e.future_cst 
+
 (** {6 Various checks } *)
 
 let exists_modlabel l senv = Label.Set.mem l senv.modlabels
@@ -331,21 +379,22 @@ let safe_push_named (id,_,_ as d) env =
 
 
 let push_named_def (id,de) senv =
-  let c,typ,univs = Term_typing.translate_local_def senv.env id de in
-  let senv' = push_context univs senv in
-  let c, senv' = match c with
-    | Def c -> Mod_subst.force_constr c, senv'
+  let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
+  let poly = de.Entries.const_entry_polymorphic in
+  let univs = Univ.ContextSet.of_context univs in
+  let c, univs = match c with
+    | Def c -> Mod_subst.force_constr c, univs
     | OpaqueDef o ->
-        Opaqueproof.force_proof (Environ.opaque_tables senv'.env) o,
-        push_context_set
-          (Opaqueproof.force_constraints (Environ.opaque_tables senv'.env) o)
-          senv'
+        Opaqueproof.force_proof (Environ.opaque_tables senv.env) o,
+        Univ.ContextSet.union univs 
+	(Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o)
     | _ -> assert false in
+  let senv' = push_context_set poly univs senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
-    {senv' with env=env''}
+    univs, {senv' with env=env''}
 
-let push_named_assum ((id,t),ctx) senv =
-  let senv' = push_context_set ctx senv in
+let push_named_assum ((id,t,poly),ctx) senv =
+  let senv' = push_context_set poly ctx senv in
   let t = Term_typing.translate_local_assum senv'.env t in
   let env'' = safe_push_named (id,None,t) senv'.env in
     {senv' with env=env''}
@@ -368,10 +417,10 @@ let labels_of_mib mib =
 
 let globalize_constant_universes env cb =
   if cb.const_polymorphic then
-    [Now Univ.Constraint.empty]
+    [Now (true, Univ.ContextSet.empty)]
   else
-    let cstrs = Univ.UContext.constraints cb.const_universes in
-      Now cstrs ::  
+    let cstrs = Univ.ContextSet.of_context cb.const_universes in
+      Now (false, cstrs) ::  
 	(match cb.const_body with
 	| (Undef _ | Def _) -> []
 	| OpaqueDef lc ->
@@ -379,23 +428,21 @@ let globalize_constant_universes env cb =
 	  | None -> []
 	  | Some fc ->
             match Future.peek_val fc with
-            | None -> [Later (Future.chain
-                 ~greedy:(not (Future.is_exn fc))
-                 ~pure:true fc Univ.ContextSet.constraints)]
-            | Some c -> [Now (Univ.ContextSet.constraints c)])
+            | None -> [Later fc]
+            | Some c -> [Now (false, c)])
       
 let globalize_mind_universes mb =
   if mb.mind_polymorphic then
-    [Now Univ.Constraint.empty]
+    [Now (true, Univ.ContextSet.empty)]
   else
-    [Now (Univ.UContext.constraints mb.mind_universes)]
+    [Now (false, Univ.ContextSet.of_context mb.mind_universes)]
 
 let constraints_of_sfb env sfb = 
   match sfb with
   | SFBconst cb -> globalize_constant_universes env cb
   | SFBmind mib -> globalize_mind_universes mib
-  | SFBmodtype mtb -> [Now mtb.mod_constraints]
-  | SFBmodule mb -> [Now mb.mod_constraints]
+  | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)]
+  | SFBmodule mb -> [Now (false, mb.mod_constraints)]
 
 (** A generic function for adding a new field in a same environment.
     It also performs the corresponding [add_constraints]. *)
@@ -437,19 +484,16 @@ let update_resolver f senv = { senv with modresolver = f senv.modresolver }
 
 (** Insertion of constants and parameters in environment *)
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry
+  | ConstantEntry of bool * private_constants Entries.constant_entry
   | GlobalRecipe of Cooking.recipe
 
-let add_constant dir l decl senv =
-  let kn = make_con senv.modpath dir l in
-  let cb = match decl with
-    | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce
-    | GlobalRecipe r ->
-      let cb = Term_typing.translate_recipe senv.env kn r in
-      if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
-  in
+type exported_private_constant = 
+  constant * private_constants Entries.constant_entry * private_constant_role
+
+let add_constant_aux no_section senv (kn, cb) =
+  let l = pi3 (Constant.repr3 kn) in
   let cb, otab = match cb.const_body with
-    | OpaqueDef lc when DirPath.is_empty dir ->
+    | OpaqueDef lc when no_section ->
       (* In coqc, opaque constants outside sections will be stored
          indirectly in a specific table *)
       let od, otab =
@@ -466,7 +510,32 @@ let add_constant dir l decl senv =
         (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv'
     | _ -> senv'
   in
-  kn, senv''
+  senv''
+
+let add_constant dir l decl senv =
+  let kn = make_con senv.modpath dir l in
+  let no_section = DirPath.is_empty dir in
+  let seff_to_export, decl =
+    match decl with
+    | ConstantEntry (true, ce) ->
+        let exports, ce =
+          Term_typing.export_side_effects senv.revstruct senv.env ce in
+        exports, ConstantEntry (false, ce)
+    | _ -> [], decl
+  in
+  let senv =
+    List.fold_left (add_constant_aux no_section) senv
+      (List.map (fun (kn,cb,_,_) -> kn, cb) seff_to_export) in
+  let senv =
+    let cb = 
+      match decl with
+      | ConstantEntry (export_seff,ce) ->
+        Term_typing.translate_constant senv.revstruct senv.env kn ce
+      | GlobalRecipe r ->
+        let cb = Term_typing.translate_recipe senv.env kn r in
+        if no_section then Declareops.hcons_const_body cb else cb in
+    add_constant_aux no_section senv (kn, cb) in
+  (kn, List.map (fun (kn,_,ce,r) -> kn, ce, r) seff_to_export), senv
 
 (** Insertion of inductive types *)
 
@@ -498,13 +567,13 @@ let add_modtype l params_mte inl senv =
 (** full_add_module adds module with universes and constraints *)
 
 let full_add_module mb senv =
-  let senv = add_constraints (Now mb.mod_constraints) senv in
+  let senv = add_constraints (Now (false, mb.mod_constraints)) senv in
   let dp = ModPath.dp mb.mod_mp in
   let linkinfo = Nativecode.link_info_of_dirpath dp in
   { senv with env = Modops.add_linked_module mb linkinfo senv.env }
 
 let full_add_module_type mp mt senv =
-  let senv = add_constraints (Now mt.mod_constraints) senv in
+  let senv = add_constraints (Now (false, mt.mod_constraints)) senv in
   { senv with env = Modops.add_module_type mp mt senv.env }
 
 (** Insertion of modules *)
@@ -612,8 +681,8 @@ let propagate_senv newdef newenv newresolver senv oldsenv =
     modlabels = Label.Set.add (fst newdef) oldsenv.modlabels;
     univ =
       List.fold_left (fun acc cst ->
-        Univ.Constraint.union acc (Future.force cst))
-      (Univ.Constraint.union senv.univ oldsenv.univ)
+        Univ.ContextSet.union acc (Future.force cst))
+      (Univ.ContextSet.union senv.univ oldsenv.univ)
       now_cst;
     future_cst = later_cst @ oldsenv.future_cst;
     (* engagement is propagated to the upper level *)
@@ -621,7 +690,8 @@ let propagate_senv newdef newenv newresolver senv oldsenv =
     required = senv.required;
     loads = senv.loads@oldsenv.loads;
     local_retroknowledge =
-            senv.local_retroknowledge@oldsenv.local_retroknowledge }
+            senv.local_retroknowledge@oldsenv.local_retroknowledge;
+    native_symbols = senv.native_symbols}
 
 let end_module l restype senv =
   let mp = senv.modpath in
@@ -635,8 +705,8 @@ let end_module l restype senv =
   let senv'=
     propagate_loads { senv with
       env = newenv;
-      univ = Univ.Constraint.union senv.univ mb.mod_constraints} in
-  let newenv = Environ.add_constraints mb.mod_constraints senv'.env in
+      univ = Univ.ContextSet.union senv.univ mb.mod_constraints} in
+  let newenv = Environ.push_context_set ~strict:true mb.mod_constraints senv'.env in
   let newenv = Modops.add_module mb newenv in
   let newresolver =
     if Modops.is_functor mb.mod_type then oldsenv.modresolver
@@ -661,7 +731,7 @@ let end_modtype l senv =
   let () = check_empty_context senv in
   let mbids = List.rev_map fst params in
   let newenv = Environ.set_opaque_tables oldsenv.env (Environ.opaque_tables senv.env) in
-  let newenv = Environ.add_constraints senv.univ newenv in
+  let newenv = Environ.push_context_set ~strict:true senv.univ newenv in
   let newenv = set_engagement_opt newenv senv.engagement in
   let senv' = propagate_loads {senv with env=newenv} in
   let auto_tb = functorize params (NoFunctor (List.rev senv.revstruct)) in
@@ -676,38 +746,32 @@ let end_modtype l senv =
 let add_include me is_module inl senv =
   let open Mod_typing in
   let mp_sup = senv.modpath in
-  let sign,cst,resolver =
-    if is_module then
-      let sign,_,reso,cst = translate_mse_incl senv.env mp_sup inl me in
-      sign,cst,reso
-    else
-      let mtb = translate_modtype senv.env mp_sup inl ([],me) in
-      mtb.mod_type,mtb.mod_constraints,mtb.mod_delta
+  let sign,_,resolver,cst =
+    translate_mse_incl is_module senv.env mp_sup inl me
   in
-  let senv = add_constraints (Now cst) senv in
+  let senv = add_constraints (Now (false, cst)) senv in
   (* Include Self support  *)
   let rec compute_sign sign mb resolver senv =
     match sign with
     | MoreFunctor(mbid,mtb,str) ->
       let cst_sub = Subtyping.check_subtypes senv.env mb mtb in
-      let senv = add_constraints (Now cst_sub) senv in
+      let senv =
+	add_constraints
+	  (Now (false, Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty))
+	  senv in
       let mpsup_delta =
 	Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta
       in
       let subst = Mod_subst.map_mbid mbid mp_sup mpsup_delta in
       let resolver = Mod_subst.subst_codom_delta_resolver subst resolver in
       compute_sign (Modops.subst_signature subst str) mb resolver senv
-    | str -> resolver,str,senv
+    | NoFunctor str -> resolver,str,senv
   in
-  let resolver,sign,senv =
+  let resolver,str,senv =
     let struc = NoFunctor (List.rev senv.revstruct) in
-    let mtb = build_mtb mp_sup struc Univ.Constraint.empty senv.modresolver in
+    let mtb = build_mtb mp_sup struc Univ.ContextSet.empty senv.modresolver in
     compute_sign sign mtb resolver senv
   in
-  let str = match sign with
-    | NoFunctor struc -> struc
-    | MoreFunctor _ -> Modops.error_higher_order_include ()
-  in
   let senv = update_resolver (Mod_subst.add_delta_resolver resolver) senv
   in
   let add senv ((l,elem) as field) =
@@ -729,12 +793,15 @@ type compiled_library = {
   comp_name : DirPath.t;
   comp_mod : module_body;
   comp_deps : library_info array;
-  comp_enga : engagement option;
-  comp_natsymbs : Nativecode.symbol array
+  comp_enga : engagement;
+  comp_natsymbs : Nativecode.symbols
 }
 
 type native_library = Nativecode.global list
 
+let get_library_native_symbols senv dir =
+  DPMap.find dir senv.native_symbols
+
 (** FIXME: MS: remove?*)
 let current_modpath senv = senv.modpath
 let current_dirpath senv = Names.ModPath.dp (current_modpath senv)
@@ -771,17 +838,17 @@ let export ?except senv dir =
       mod_retroknowledge = senv.local_retroknowledge
     }
   in
-  let ast, values =
-    if !Flags.no_native_compiler then [], [||]
-    else
+  let ast, symbols =
+    if !Flags.native_compiler then
       Nativelibrary.dump_library mp dir senv.env str
+    else [], Nativecode.empty_symbols
   in
   let lib = {
     comp_name = dir;
     comp_mod = mb;
     comp_deps = Array.of_list (DPMap.bindings senv.required);
     comp_enga = Environ.engagement senv.env;
-    comp_natsymbs = values }
+    comp_natsymbs = symbols }
   in
   mp, lib, ast
 
@@ -792,9 +859,11 @@ let import lib cst vodigest senv =
   check_engagement senv.env lib.comp_enga;
   let mp = MPfile lib.comp_name in
   let mb = lib.comp_mod in
-  let env = Environ.add_constraints mb.mod_constraints senv.env in
-  let env = Environ.push_context_set cst env in
-  (mp, lib.comp_natsymbs),
+  let env = Environ.push_context_set ~strict:true
+				     (Univ.ContextSet.union mb.mod_constraints cst)
+				     senv.env
+  in
+  mp,
   { senv with
     env =
       (let linkinfo =
@@ -803,7 +872,8 @@ let import lib cst vodigest senv =
        Modops.add_linked_module mb linkinfo env);
     modresolver = Mod_subst.add_delta_resolver mb.mod_delta senv.modresolver;
     required = DPMap.add lib.comp_name vodigest senv.required;
-    loads = (mp,mb)::senv.loads }
+    loads = (mp,mb)::senv.loads;
+    native_symbols = DPMap.add lib.comp_name lib.comp_natsymbs senv.native_symbols }
 
 (** {6 Safe typing } *)
 
@@ -845,7 +915,9 @@ let register_inline kn senv =
   let env = { env with env_globals = new_globals } in
   { senv with env = env_of_pre_env env }
 
-let add_constraints c = add_constraints (Now c)
+let add_constraints c =
+  add_constraints
+    (Now (false, Univ.ContextSet.add_constraints c Univ.ContextSet.empty))
 
 
 (* NB: The next old comment probably refers to [propagate_loads] above.
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index abd5cd7a..2214cf8b 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -39,10 +39,30 @@ type 'a safe_transformer = safe_environment -> 'a * safe_environment
 
 (** {6 Stm machinery } *)
 
-val sideff_of_con : safe_environment -> constant -> Declarations.side_effect
-val sideff_of_scheme :
-  string -> safe_environment -> (inductive * constant) list ->
-    Declarations.side_effect
+type private_constant
+type private_constants
+
+type private_constant_role =
+  | Subproof
+  | Schema of inductive * string
+
+val side_effects_of_private_constants :
+  private_constants -> Entries.side_effects
+
+val empty_private_constants : private_constants
+val add_private : private_constant -> private_constants -> private_constants
+val concat_private : private_constants -> private_constants -> private_constants
+
+val private_con_of_con : safe_environment -> constant -> private_constant
+val private_con_of_scheme : kind:string -> safe_environment -> (inductive * constant) list -> private_constant
+
+val mk_pure_proof : Constr.constr -> private_constants Entries.proof_output
+val inline_private_constants_in_constr :
+  Environ.env -> Constr.constr -> private_constants -> Constr.constr
+val inline_private_constants_in_definition_entry :
+  Environ.env -> private_constants Entries.definition_entry -> private_constants Entries.definition_entry
+
+val universes_of_private : private_constants -> Univ.universe_context_set list
 
 val is_curmod_library : safe_environment -> bool
 
@@ -51,23 +71,35 @@ val is_curmod_library : safe_environment -> bool
 val join_safe_environment :
   ?except:Future.UUIDSet.t -> safe_environment -> safe_environment
 
+val is_joined_environment : safe_environment -> bool
 (** {6 Enriching a safe environment } *)
 
 (** Insertion of local declarations (Local or Variables) *)
 
 val push_named_assum :
-  (Id.t * Term.types) Univ.in_universe_context_set -> safe_transformer0
+  (Id.t * Term.types * bool (* polymorphic *))
+    Univ.in_universe_context_set -> safe_transformer0
+
+(** Returns the full universe context necessary to typecheck the definition
+  (futures are forced) *)
 val push_named_def :
-  Id.t * Entries.definition_entry -> safe_transformer0
+  Id.t * private_constants Entries.definition_entry -> Univ.universe_context_set safe_transformer
 
 (** Insertion of global axioms or definitions *)
 
 type global_declaration =
-  | ConstantEntry of Entries.constant_entry
+                  (* bool: export private constants *)
+  | ConstantEntry of bool * private_constants Entries.constant_entry
   | GlobalRecipe of Cooking.recipe
 
+type exported_private_constant = 
+  constant * private_constants Entries.constant_entry * private_constant_role
+
+(** returns the main constant plus a list of auxiliary constants (empty
+    unless one requires the side effects to be exported) *)
 val add_constant :
-  DirPath.t -> Label.t -> global_declaration -> constant safe_transformer
+  DirPath.t -> Label.t -> global_declaration ->
+    (constant * exported_private_constant list) safe_transformer
 
 (** Adding an inductive type *)
 
@@ -87,10 +119,10 @@ val add_modtype :
 (** Adding universe constraints *)
 
 val push_context_set :
-  Univ.universe_context_set -> safe_transformer0
+  bool -> Univ.universe_context_set -> safe_transformer0
 
 val push_context :
-  Univ.universe_context -> safe_transformer0
+  bool -> Univ.universe_context -> safe_transformer0
 
 val add_constraints :
   Univ.constraints -> safe_transformer0
@@ -98,12 +130,9 @@ val add_constraints :
 (* (\** Generator of universes *\) *)
 (* val next_universe : int safe_transformer *)
 
-(** Setting the strongly constructive or classical logical engagement *)
+(** Setting the type theory flavor *)
 val set_engagement : Declarations.engagement -> safe_transformer0
 
-(** Collapsing the type hierarchy *)
-val set_type_in_type : safe_transformer0
-
 (** {6 Interactive module functions } *)
 
 val start_module : Label.t -> module_path safe_transformer
@@ -136,6 +165,8 @@ type compiled_library
 
 type native_library = Nativecode.global list
 
+val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols
+
 val start_library : DirPath.t -> module_path safe_transformer
 
 val export :
@@ -145,7 +176,7 @@ val export :
 
 (* Constraints are non empty iff the file is a vi2vo *)
 val import : compiled_library -> Univ.universe_context_set -> vodigest ->
-  (module_path * Nativecode.symbol array) safe_transformer
+  module_path safe_transformer
 
 (** {6 Safe typing judgments } *)
 
diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index ae86d686..e2854abf 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -26,8 +26,8 @@ let univ_of_sort = function
   | Prop Null -> Universe.type0m
 
 let sort_of_univ u =
-  if is_type0m_univ u then Prop Null
-  else if is_type0_univ u then Prop Pos
+  if is_type0m_univ u then prop
+  else if is_type0_univ u then set
   else Type u
 
 let compare s1 s2 =
@@ -62,6 +62,8 @@ let is_small = function
 let family = function
   | Prop Null -> InProp
   | Prop Pos -> InSet
+  | Type u when is_type0m_univ u -> InProp
+  | Type u when is_type0_univ u -> InSet
   | Type _ -> InType
 
 let family_equal = (==)
@@ -76,7 +78,7 @@ let hash = function
   in
   combinesmall 1 h
 | Type u ->
-  let h = Hashtbl.hash u in (** FIXME *)
+ let h = Univ.Universe.hash u in
   combinesmall 2 h
 
 module List = struct
@@ -101,7 +103,7 @@ module Hsorts =
         | (Type u1, Type u2) -> u1 == u2
         |_ -> false
 
-      let hash = Hashtbl.hash (** FIXME *)
+      let hash = hash
     end)
 
 let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index db155e6c..58f3bcdf 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -311,15 +311,19 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
 		try 
 		  (* The environment with the expected universes plus equality 
 		     of the body instances with the expected instance *)
-		  let env = Environ.add_constraints cstrs env in
-		    (* Check that the given definition does not add any constraint over
-		       the expected ones, so that it can be used in place of the original. *)
+		  let ctxi = Univ.Instance.append inst1 inst2 in
+		  let ctx = Univ.UContext.make (ctxi, cstrs) in
+		  let env = Environ.push_context ctx env in
+		  (* Check that the given definition does not add any constraint over
+		     the expected ones, so that it can be used in place of 
+                     the original. *)
 		    if Univ.check_constraints ctx1 (Environ.universes env) then
 		      cstrs, env, inst2
 		    else error (IncompatibleConstraints ctx1)
 		with Univ.UniverseInconsistency incon -> 
 		  error (IncompatibleUniverses incon)
-	else cst, env, Univ.Instance.empty
+	else
+	  cst, env, Univ.Instance.empty
       in
       (* Now check types *)
       let typ1 = Typeops.type_of_constant_type env' cb1.const_type in
@@ -456,6 +460,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
 
 let check_subtypes env sup super =
   let env = add_module_type sup.mod_mp sup env in
+  let env = Environ.push_context_set ~strict:true super.mod_constraints env in
   check_modtypes Univ.Constraint.empty env
     (strengthen sup sup.mod_mp) super empty_subst
     (map_mp super.mod_mp sup.mod_mp sup.mod_delta) false
diff --git a/kernel/term.ml b/kernel/term.ml
index 7bf4c818..33ed25fe 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -566,8 +566,10 @@ let decompose_lam_assum =
   in
   lamdec_rec empty_rel_context
 
-(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T
-   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+(* Given a positive integer n, decompose a product or let-in term
+   of the form [forall (x1:T1)..(xi:=ci:Ti)..(xn:Tn), T] into the pair
+   of the quantifying context [(xn,None,Tn);..;(xi,Some
+   ci,Ti);..;(x1,None,T1)] and of the inner type [T]) *)
 let decompose_prod_n_assum n =
   if n < 0 then
     error "decompose_prod_n_assum: integer parameter must be positive";
@@ -581,10 +583,12 @@ let decompose_prod_n_assum n =
   in
   prodec_rec empty_rel_context n
 
-(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T
-   into the pair ([(xn,Tn);...;(x1,T1)],T)
+(* Given a positive integer n, decompose a lambda or let-in term [fun
+   (x1:T1)..(xi:=ci:Ti)..(xn:Tn) => T] into the pair of the abstracted
+   context [(xn,None,Tn);...;(xi,Some ci,Ti);...;(x1,None,T1)] and of
+   the inner body [T].
    Lets in between are not expanded but turn into local definitions,
-   but n is the actual number of destructurated lambdas.  *)
+   but n is the actual number of destructurated lambdas. *)
 let decompose_lam_n_assum n =
   if n < 0 then
     error "decompose_lam_n_assum: integer parameter must be positive";
@@ -598,6 +602,20 @@ let decompose_lam_n_assum n =
   in
   lamdec_rec empty_rel_context n
 
+(* Same, counting let-in *)
+let decompose_lam_n_decls n =
+  if n < 0 then
+    error "decompose_lam_n_decls: integer parameter must be positive";
+  let rec lamdec_rec l n c =
+    if Int.equal n 0 then l,c
+    else match kind_of_term c with
+    | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
+    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+    | Cast (c,_,_)      -> lamdec_rec l n c
+    | c -> error "decompose_lam_n_decls: not enough abstractions"
+  in
+  lamdec_rec empty_rel_context n
+
 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
  * gives n (casts are ignored) *)
 let nb_lam =
diff --git a/kernel/term.mli b/kernel/term.mli
index 501aaf74..d6071641 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -281,13 +281,15 @@ val decompose_prod : constr -> (Name.t*constr) list * constr
    {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *)
 val decompose_lam : constr -> (Name.t*constr) list * constr
 
-(** Given a positive integer n, transforms a product term
+(** Given a positive integer n, decompose a product term
    {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %}
-   into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *)
+   into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}.
+   Raise a user error if not enough products. *)
 val decompose_prod_n : int -> constr -> (Name.t * constr) list * constr
 
-(** Given a positive integer {% $ %}n{% $ %}, transforms a lambda term
-   {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %} *)
+(** Given a positive integer {% $ %}n{% $ %}, decompose a lambda term
+   {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}.
+   Raise a user error if not enough lambdas. *)
 val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
 
 (** Extract the premisses and the conclusion of a term of the form
@@ -297,10 +299,15 @@ val decompose_prod_assum : types -> rel_context * types
 (** Idem with lambda's *)
 val decompose_lam_assum : constr -> rel_context * constr
 
-(** Idem but extract the first [n] premisses *)
+(** Idem but extract the first [n] premisses, counting let-ins. *)
 val decompose_prod_n_assum : int -> types -> rel_context * types
+
+(** Idem for lambdas, _not_ counting let-ins *)
 val decompose_lam_n_assum : int -> constr -> rel_context * constr
 
+(** Idem, counting let-ins *)
+val decompose_lam_n_decls : int -> constr -> rel_context * constr
+
 (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
    gives {% $ %}n{% $ %} (casts are ignored) *)
 val nb_lam : constr -> int
@@ -308,12 +315,14 @@ val nb_lam : constr -> int
 (** Similar to [nb_lam], but gives the number of products instead *)
 val nb_prod : constr -> int
 
-(** Returns the premisses/parameters of a type/term (let-in included) *)
+(** Return the premisses/parameters of a type/term (let-in included) *)
 val prod_assum : types -> rel_context
 val lam_assum : constr -> rel_context
 
-(** Returns the first n-th premisses/parameters of a type/term (let included)*)
+(** Return the first n-th premisses/parameters of a type (let included and counted) *)
 val prod_n_assum : int -> types -> rel_context
+
+(** Return the first n-th premisses/parameters of a term (let included but not counted) *)
 val lam_n_assum : int -> constr -> rel_context
 
 (** Remove the premisses/parameters of a type/term *)
@@ -328,11 +337,11 @@ val strip_lam_n : int -> constr -> constr
 val strip_prod_assum : types -> types
 val strip_lam_assum : constr -> constr
 
-(** flattens application lists *)
+(** Flattens application lists *)
 val collapse_appl : constr -> constr
 
 
-(** Removes recursively the casts around a term i.e.
+(** Remove recursively the casts around a term i.e.
    [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
 val strip_outer_cast : constr -> constr
 
@@ -352,10 +361,10 @@ type arity = rel_context * sorts
 (** Build an "arity" from its canonical form *)
 val mkArity : arity -> types
 
-(** Destructs an "arity" into its canonical form *)
+(** Destruct an "arity" into its canonical form *)
 val destArity : types -> arity
 
-(** Tells if a term has the form of an arity *)
+(** Tell if a term has the form of an arity *)
 val isArity : types -> bool
 
 (** {5 Kind of type} *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index a316b449..a566028d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -43,10 +43,29 @@ let map_option_typ = function None -> `None | Some x -> `Some x
 
 (* Insertion of constants and parameters in environment. *)
 
-let mk_pure_proof c = (c, Univ.ContextSet.empty), Declareops.no_seff
+let mk_pure_proof c = (c, Univ.ContextSet.empty), []
 
-let handle_side_effects env body side_eff =
-  let handle_sideff t se =
+let equal_eff e1 e2 =
+  let open Entries in
+  match e1, e2 with
+  | { eff = SEsubproof (c1,_,_) }, { eff = SEsubproof (c2,_,_) } ->
+        Names.Constant.equal c1 c2
+  | { eff = SEscheme (cl1,_) }, { eff = SEscheme (cl2,_) } ->
+        CList.for_all2eq
+          (fun (_,c1,_,_) (_,c2,_,_) -> Names.Constant.equal c1 c2)
+          cl1 cl2
+  | _ -> false
+
+let rec uniq_seff = function
+  | [] -> []
+  | x :: xs -> x :: uniq_seff (List.filter (fun y -> not (equal_eff x y)) xs)
+(* The list of side effects is in reverse order (most recent first).
+ * To keep the "topological" order between effects we have to uniq-ize from
+ * the tail *)
+let uniq_seff l = List.rev (uniq_seff (List.rev l))
+
+let inline_side_effects env body ctx side_eff =
+  let handle_sideff (t,ctx,sl) { eff = se; from_env = mb } =
     let cbl = match se with
       | SEsubproof (c,cb,b) -> [c,cb,b]
       | SEscheme (cl,_) -> List.map (fun (_,c,cb,b) -> c,cb,b) cl in
@@ -65,8 +84,8 @@ let handle_side_effects env body side_eff =
     let rec sub_body c u b i x = match kind_of_term x with
       | Const (c',u') when eq_constant c c' -> 
 	Vars.subst_instance_constr u' b
-      | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in
-    let fix_body (c,cb,b) t =
+      | _ -> map_constr_with_binders ((+) 1) (sub_body c u b) i x in
+    let fix_body (c,cb,b) (t,ctx) =
       match cb.const_body, b with
       | Def b, _ ->
           let b = Mod_subst.force_constr b in
@@ -74,37 +93,86 @@ let handle_side_effects env body side_eff =
 	    if not poly then
               let b_ty = Typeops.type_of_constant_type env cb.const_type in
               let t = sub c 1 (Vars.lift 1 t) in
-		mkLetIn (cname c, b, b_ty, t)
+	        mkLetIn (cname c, b, b_ty, t),
+		Univ.ContextSet.union ctx
+		  (Univ.ContextSet.of_context cb.const_universes)
 	    else 
 	      let univs = cb.const_universes in
-		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
       | OpaqueDef _, `Opaque (b,_) -> 
 	  let poly = cb.const_polymorphic in
 	    if not poly then
               let b_ty = Typeops.type_of_constant_type env cb.const_type in
               let t = sub c 1 (Vars.lift 1 t) in
-		mkApp (mkLambda (cname c, b_ty, t), [|b|]) 
+	        mkApp (mkLambda (cname c, b_ty, t), [|b|]),
+		Univ.ContextSet.union ctx
+		  (Univ.ContextSet.of_context cb.const_universes)
 	    else
 	      let univs = cb.const_universes in
-		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t), ctx
       | _ -> assert false
     in
-      List.fold_right fix_body cbl t
+    let t, ctx = List.fold_right fix_body cbl (t,ctx) in
+    t, ctx, (mb,List.length cbl) :: sl
   in
   (* CAVEAT: we assure a proper order *)
-  Declareops.fold_side_effects handle_sideff body
-    (Declareops.uniquize_side_effects side_eff)
+  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
+
+(* Given the list of signatures of side effects, checks if they match.
+ * I.e. if they are ordered descendants of the current revstruct *)
+let check_signatures curmb sl =
+  let is_direct_ancestor (sl, curmb) (mb, how_many) =
+    match curmb with
+    | None -> None, None
+    | Some curmb ->
+        try
+          let mb = Ephemeron.get mb in
+          match sl with
+          | None -> sl, None
+          | Some n ->
+              if List.length mb >= how_many && CList.skipn how_many mb == curmb
+              then Some (n + how_many), Some mb
+              else None, None
+        with Ephemeron.InvalidKey -> None, None in
+  let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
+  sl
+
+let skip_trusted_seff sl b e =
+  let rec aux sl b e acc =
+    match sl, kind_of_term b with
+    | (None|Some 0), _ -> b, e, acc
+    | Some sl, LetIn (n,c,ty,bo) ->
+       aux (Some (sl-1)) bo
+         (Environ.push_rel (n,Some c,ty) e) (`Let(n,c,ty)::acc)
+    | Some sl, App(hd,arg) ->
+       begin match kind_of_term hd with
+       | Lambda (n,ty,bo) ->
+           aux (Some (sl-1)) bo
+             (Environ.push_rel (n,None,ty) e) (`Cut(n,ty,arg)::acc)
+       | _ -> assert false
+       end
+    | _ -> assert false
+    in
+  aux sl b e []
+
+let rec unzip ctx j =
+  match ctx with
+  | [] -> j
+  | `Let (n,c,ty) :: ctx ->
+      unzip ctx { j with uj_val = mkLetIn (n,c,ty,j.uj_val) }
+  | `Cut (n,ty,arg) :: ctx ->
+      unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }
 
 let hcons_j j =
   { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 
 
 let feedback_completion_typecheck =
   Option.iter (fun state_id -> Pp.feedback ~state_id Feedback.Complete)
-
-let infer_declaration env kn dcl =
+	      
+let infer_declaration ~trust env kn dcl =
   match dcl with
   | ParameterEntry (ctx,poly,(t,uctx),nl) ->
-      let env = push_context uctx env in
+      let env = push_context ~strict:(not poly) uctx env in
       let j = infer env t in
       let abstract = poly && not (Option.is_empty kn) in
       let usubst, univs = Univ.abstract_universes abstract uctx in
@@ -115,34 +183,41 @@ let infer_declaration env kn dcl =
   | DefinitionEntry ({ const_entry_type = Some typ;
                        const_entry_opaque = true;
 		       const_entry_polymorphic = false} as c) ->
-      let env = push_context c.const_entry_universes env in
+      let env = push_context ~strict:true c.const_entry_universes env in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let tyj = infer_type env typ in
       let proofterm =
-        Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
-          let body = handle_side_effects env body side_eff in
-	  let env' = push_context_set ctx env in
-          let j = infer env' body in
+        Future.chain ~greedy:true ~pure:true body (fun ((body,uctx),side_eff) ->
+          let body, uctx, signatures =
+            inline_side_effects env body uctx side_eff in
+          let valid_signatures = check_signatures trust signatures in
+	  let env' = push_context_set uctx env in
+          let j =
+            let body,env',ectx = skip_trusted_seff valid_signatures body env' in
+            let j = infer env' body in
+            unzip ectx j in
           let j = hcons_j j in
 	  let subst = Univ.LMap.empty in
           let _typ = constrain_type env' j c.const_entry_polymorphic subst
 	    (`SomeWJ (typ,tyj)) in
           feedback_completion_typecheck feedback_id;
-          j.uj_val, ctx) in
+          j.uj_val, uctx) in
       let def = OpaqueDef (Opaqueproof.create proofterm) in
       def, RegularArity typ, None, c.const_entry_polymorphic, 
 	c.const_entry_universes,
 	c.const_entry_inline_code, c.const_entry_secctx
 
   | DefinitionEntry c ->
-      let env = push_context c.const_entry_universes env in
       let { const_entry_type = typ; const_entry_opaque = opaque } = c in
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
-      assert(Univ.ContextSet.is_empty ctx);
-      let body = handle_side_effects env body side_eff in
+      let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
+      let body, ctx, _ = inline_side_effects env body
+        (Univ.ContextSet.union univsctx ctx) side_eff in
+      let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
       let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
-      let usubst, univs = Univ.abstract_universes abstract c.const_entry_universes in
+      let usubst, univs =
+	Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in      
       let j = infer env body in
       let typ = constrain_type env j c.const_entry_polymorphic usubst (map_option_typ typ) in
       let def = hcons_constr (Vars.subst_univs_level_constr usubst j.uj_val) in
@@ -176,14 +251,17 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
-let record_aux env s1 s2 =
+let record_aux env s_ty s_bo suggested_expr =
+  let in_ty = keep_hyps env s_ty in
   let v =
     String.concat " "
-      (List.map (fun (id, _,_) -> Id.to_string id)
-        (keep_hyps env (Id.Set.union s1 s2))) in
-  Aux_file.record_in_aux "context_used" v
+      (CList.map_filter (fun (id, _,_) ->
+          if List.exists (fun (id',_,_) -> Id.equal id id') in_ty then None
+          else Some (Id.to_string id))
+        (keep_hyps env s_bo)) in
+  Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
 
-let suggest_proof_using = ref (fun _ _ _ _ _ -> ())
+let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
 let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
@@ -198,6 +276,10 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         str " " ++ str (String.conjugate_verb_to_be n) ++
         str " used but not declared:" ++
         fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
+  let sort evn l =
+    List.filter (fun (id,_,_) ->
+      List.exists (fun (id',_,_) -> Names.Id.equal id id') l)
+    (named_context env) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
     let context_ids = List.map pi1 (named_context env) in
@@ -215,19 +297,21 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
                 (Opaqueproof.force_proof (opaque_tables env) lc) in
             (* we force so that cst are added to the env immediately after *)
             ignore(Opaqueproof.force_constraints (opaque_tables env) lc);
-            !suggest_proof_using kn env vars ids_typ context_ids;
+            let expr =
+              !suggest_proof_using (Constant.to_string kn)
+                env vars ids_typ context_ids in
             if !Flags.compilation_mode = Flags.BuildVo then
-              record_aux env ids_typ vars;
+              record_aux env ids_typ vars expr;
             vars
         in
         keep_hyps env (Idset.union ids_typ ids_def), def
     | None ->
         if !Flags.compilation_mode = Flags.BuildVo then
-          record_aux env Id.Set.empty Id.Set.empty;
+          record_aux env Id.Set.empty Id.Set.empty "";
         [], def (* Empty section context: no need to check *)
     | Some declared ->
         (* We use the declared set and chain a check of correctness *)
-        declared,
+        sort env declared,
         match def with
         | Undef _ as x -> x (* nothing to check *)
         | Def cs as x ->
@@ -243,16 +327,30 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
               let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
               check declared inferred) lc) in
   let tps = 
-    (* FIXME: incompleteness of the bytecode vm: we compile polymorphic 
-       constants like opaque definitions. *)
-    if poly then Some (Cemitcodes.from_val Cemitcodes.BCconstant)
-    else
-      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
+    let res =
+      let comp_univs = if poly then Some univs else None in
+      match proj with
+      | None -> compile_constant_body env comp_univs def
+      | Some pb ->
+	(* The compilation of primitive projections is a bit tricky, because
+           they refer to themselves (the body of p looks like fun c =>
+           Proj(p,c)). We break the cycle by building an ad-hoc compilation
+           environment. A cleaner solution would be that kernel projections are
+           simply Proj(i,c) with i an int and c a constr, but we would have to
+           get rid of the compatibility layer. *)
+	let cb =
+	  { const_hyps = hyps;
+	    const_body = def;
+	    const_type = typ;
+	    const_proj = proj;
+	    const_body_code = None;
+	    const_polymorphic = poly;
+	    const_universes = univs;
+	    const_inline_code = inline_code }
+	in
+	let env = add_constant kn cb env in
+	compile_constant_body env comp_univs def
+    in Option.map Cemitcodes.from_val res
   in
   { const_hyps = hyps;
     const_body = def;
@@ -263,11 +361,95 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
     const_universes = univs;
     const_inline_code = inline_code }
 
-
 (*s Global and local constant declaration. *)
 
-let translate_constant env kn ce =
-  build_constant_declaration kn env (infer_declaration env (Some kn) ce)
+let translate_constant mb env kn ce =
+  build_constant_declaration kn env
+    (infer_declaration ~trust:mb env (Some kn) ce)
+
+let constant_entry_of_side_effect cb u =
+  let pt =
+    match cb.const_body, u with
+    | OpaqueDef _, `Opaque (b, c) -> b, c
+    | Def b, `Nothing -> Mod_subst.force_constr b, Univ.ContextSet.empty
+    | _ -> assert false in
+  DefinitionEntry {
+    const_entry_body = Future.from_val (pt, []);
+    const_entry_secctx = None;
+    const_entry_feedback = None;
+    const_entry_type =
+      (match cb.const_type with RegularArity t -> Some t | _ -> None);
+    const_entry_polymorphic = cb.const_polymorphic;
+    const_entry_universes = cb.const_universes;
+    const_entry_opaque = Declareops.is_opaque cb;
+    const_entry_inline_code = cb.const_inline_code }
+;;
+
+let turn_direct (kn,cb,u,r as orig) =
+  match cb.const_body, u with
+  | OpaqueDef _, `Opaque (b,c) ->
+      let pt = Future.from_val (b,c) in
+      kn, { cb with const_body = OpaqueDef (Opaqueproof.create pt) }, u, r
+   | _ -> orig
+;;
+
+type side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+type exported_side_effect = 
+  constant * constant_body * side_effects constant_entry * side_effect_role
+
+let export_side_effects mb env ce =
+  match ce with
+  | ParameterEntry _ | ProjectionEntry _ -> [], ce
+  | DefinitionEntry c ->
+      let { const_entry_body = body } = c in
+      let _, eff = Future.force body in
+      let ce = DefinitionEntry { c with
+        const_entry_body = Future.chain ~greedy:true ~pure:true body
+          (fun (b_ctx, _) -> b_ctx, []) } in
+      let not_exists (c,_,_,_) =
+        try ignore(Environ.lookup_constant c env); false
+        with Not_found -> true in 
+      let aux (acc,sl) { eff = se; from_env = mb } =
+        let cbl = match se with
+          | SEsubproof (c,cb,b) -> [c,cb,b,Subproof]
+          | SEscheme (cl,k) ->
+              List.map (fun (i,c,cb,b) -> c,cb,b,Schema(i,k)) cl in
+        let cbl = List.filter not_exists cbl in
+        if cbl = [] then acc, sl
+        else cbl :: acc, (mb,List.length cbl) :: sl in
+      let seff, signatures = List.fold_left aux ([],[]) (uniq_seff eff) in
+      let trusted = check_signatures mb signatures in
+      let push_seff env = function
+        | kn, cb, `Nothing, _ ->
+            Environ.add_constant kn cb env
+        | kn, cb, `Opaque(_, ctx), _ -> 
+            let env = Environ.add_constant kn cb env in
+            Environ.push_context_set
+              ~strict:(not cb.const_polymorphic) ctx env in
+      let rec translate_seff sl seff acc env =
+        match sl, seff with
+        | _, [] -> List.rev acc, ce
+        | (None | Some 0), cbs :: rest ->
+           let env, cbs =
+             List.fold_left (fun (env,cbs) (kn, ocb, u, r) ->
+               let ce = constant_entry_of_side_effect ocb u in
+               let cb = translate_constant mb env kn ce in
+               (push_seff env (kn, cb,`Nothing, Subproof),(kn,cb,ce,r) :: cbs)) 
+             (env,[]) cbs in
+           translate_seff sl rest (cbs @ acc) env
+        | Some sl, cbs :: rest ->
+           let cbs_len = List.length cbs in
+           let cbs = List.map turn_direct cbs in
+           let env = List.fold_left push_seff env cbs in
+           let ecbs = List.map (fun (kn,cb,u,r) ->
+             kn, cb, constant_entry_of_side_effect cb u, r) cbs in
+           translate_seff (Some (sl-cbs_len)) rest (ecbs @ acc) env
+     in
+       translate_seff trusted seff [] env
+;;
 
 let translate_local_assum env t =
   let j = infer env t in
@@ -277,18 +459,36 @@ let translate_local_assum env t =
 let translate_recipe env kn r =
   build_constant_declaration kn env (Cooking.cook_constant env r)
 
-let translate_local_def env id centry =
+let translate_local_def mb env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =
-    infer_declaration env None (DefinitionEntry centry) in
+    infer_declaration ~trust:mb env None (DefinitionEntry centry) in
   let typ = type_of_constant_type env typ in
+  if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
+    match def with
+    | Undef _ -> ()
+    | Def _ -> ()
+    | OpaqueDef lc ->
+       let context_ids = List.map pi1 (named_context env) in
+       let ids_typ = global_vars_set env typ in
+       let ids_def = global_vars_set env
+         (Opaqueproof.force_proof (opaque_tables env) lc) in
+       let expr =
+         !suggest_proof_using (Id.to_string id)
+           env ids_def ids_typ context_ids in
+       record_aux env ids_typ ids_def expr
+  end;
   def, typ, univs
 
 (* Insertion of inductive types. *)
 
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 
-let handle_entry_side_effects env ce = { ce with
+let inline_entry_side_effects env ce = { ce with
   const_entry_body = Future.chain ~greedy:true ~pure:true
     ce.const_entry_body (fun ((body, ctx), side_eff) ->
-      (handle_side_effects env body side_eff, ctx), Declareops.no_seff);
+      let body, ctx',_ = inline_side_effects env body ctx side_eff in
+      (body, ctx'), []);
 }
+
+let inline_side_effects env body side_eff =
+  pi1 (inline_side_effects env body Univ.ContextSet.empty side_eff)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 1b54b1ea..2e6aa161 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,23 +12,46 @@ open Environ
 open Declarations
 open Entries
 
-val translate_local_def : env -> Id.t -> definition_entry ->
+val translate_local_def : structure_body -> env -> Id.t -> side_effects definition_entry ->
   constant_def * types * constant_universes
 
 val translate_local_assum : env -> types -> types
 
-val mk_pure_proof : constr -> proof_output
+val mk_pure_proof : constr -> side_effects proof_output
 
-val handle_side_effects : env -> constr -> Declareops.side_effects -> constr
+val inline_side_effects : env -> constr -> side_effects -> constr
 (** Returns the term where side effects have been turned into let-ins or beta
     redexes. *)
 
-val handle_entry_side_effects : env -> definition_entry -> definition_entry
-(** Same as {!handle_side_effects} but applied to entries. Only modifies the
+val inline_entry_side_effects :
+  env -> side_effects definition_entry -> side_effects definition_entry
+(** Same as {!inline_side_effects} but applied to entries. Only modifies the
     {!Entries.const_entry_body} field. It is meant to get a term out of a not
     yet type checked proof. *)
 
-val translate_constant : env -> constant -> constant_entry -> constant_body
+val uniq_seff : side_effects -> side_effects
+
+val translate_constant :
+  structure_body -> env -> constant -> side_effects constant_entry ->
+    constant_body
+
+type side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+type exported_side_effect = 
+  constant * constant_body * side_effects constant_entry * side_effect_role
+  
+(* Given a constant entry containing side effects it exports them (either
+ * by re-checking them or trusting them).  Returns the constant bodies to
+ * be pushed in the safe_env by safe typing.  The main constant entry
+ * needs to be translated as usual after this step. *)
+val export_side_effects :
+  structure_body -> env -> side_effects constant_entry ->
+    exported_side_effect list * side_effects constant_entry
+
+val constant_entry_of_side_effect :
+  constant_body -> seff_env -> side_effects constant_entry
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
@@ -37,11 +60,11 @@ val translate_recipe : env -> constant -> Cooking.recipe -> constant_body
 
 (** Internal functions, mentioned here for debug purpose only *)
 
-val infer_declaration : env -> constant option -> 
-  constant_entry -> Cooking.result
+val infer_declaration : trust:structure_body -> env -> constant option -> 
+  side_effects constant_entry -> Cooking.result
 
 val build_constant_declaration :
   constant -> env -> Cooking.result -> constant_body
 
 val set_suggest_proof_using :
-  (constant -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> unit) -> unit
+  (string -> env -> Id.Set.t -> Id.Set.t -> Id.t list -> string) -> unit
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 48dbacf1..4f32fdce 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -134,10 +134,16 @@ let extract_context_levels env l =
 let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
   let params, ccl = dest_prod_assum env t in
   match kind_of_term ccl with
-  | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) ->
-      let param_ccls = extract_context_levels env params in
-      let s = { template_param_levels = param_ccls; template_level = u} in
-      TemplateArity (params,s)
+  | Sort (Type u) ->
+     let ind, l = decompose_app (whd_betadeltaiota env c) in
+     if isInd ind && List.is_empty l then
+       let mis = lookup_mind_specif env (fst (destInd ind)) in
+       let nparams = Inductive.inductive_params mis in
+       let paramsl = CList.lastn nparams params in
+       let param_ccls = extract_context_levels env paramsl in
+       let s = { template_param_levels = param_ccls; template_level = u} in
+       TemplateArity (params,s)
+     else RegularArity t
   | _ ->
       RegularArity t
 
@@ -252,14 +258,12 @@ let sort_of_product env domsort rangsort =
     | (Prop _,  Prop Pos) -> rangsort
     (* Product rule (Type,Set,?) *)
     | (Type u1, Prop Pos) ->
-        begin match engagement env with
-        | Some ImpredicativeSet ->
+        if is_impredicative_set env then
           (* Rule is (Type,Set,Set) in the Set-impredicative calculus *)
           rangsort
-        | _ ->
+        else
           (* Rule is (Type_i,Set,Type_i) in the Set-predicative calculus *)
           Type (Universe.sup Universe.type0 u1)
-        end
     (* Product rule (Prop,Type_i,Type_i) *)
     | (Prop Pos,  Type u2)  -> Type (Universe.sup Universe.type0 u2)
     (* Product rule (Prop,Type_i,Type_i) *)
@@ -296,7 +300,7 @@ let judge_of_cast env cj k tj =
       match k with
       | VMcast ->
           mkCast (cj.uj_val, k, expected_type),
-          vm_conv CUMUL env cj.uj_type expected_type
+          Reduction.vm_conv CUMUL env cj.uj_type expected_type
       | DEFAULTcast ->
           mkCast (cj.uj_val, k, expected_type),
           default_conv ~l2r:false CUMUL env cj.uj_type expected_type
@@ -306,7 +310,7 @@ let judge_of_cast env cj k tj =
       | NATIVEcast ->
 	 let sigma = Nativelambda.empty_evars in
          mkCast (cj.uj_val, k, expected_type),
-         native_conv CUMUL sigma env cj.uj_type expected_type
+         Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type
     in
       { uj_val = c;
 	uj_type = expected_type }
@@ -473,7 +477,7 @@ let rec execute env cstr =
       let j' = execute env1 c3 in
         judge_of_letin env name j1 j2 j'
 
-    | Cast (c,k, t) ->
+    | Cast (c,k,t) ->
       let cj = execute env c in
       let tj = execute_type env t in
         judge_of_cast env cj k tj
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 763c0822..6c231698 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -270,8 +270,10 @@ module Level = struct
   let is_small x = 
     match data x with
     | Level _ -> false
-    | _ -> true
-
+    | Var _ -> false
+    | Prop -> true
+    | Set -> true
+ 
   let is_prop x =
     match data x with
     | Prop -> true
@@ -551,6 +553,10 @@ struct
     | Cons (l, _, Nil) -> Expr.is_level l
     | _ -> false
 
+  let rec is_levels l = match l with
+    | Cons (l, _, r) -> Expr.is_level l && is_levels r
+    | Nil -> true
+
   let level l = match l with
     | Cons (l, _, Nil) -> Expr.level l
     | _ -> None
@@ -577,7 +583,7 @@ struct
   let is_type0m x = equal type0m x
   let is_type0 x = equal type0 x
 
-  (* Returns the formal universe that lies juste above the universe variable u.
+  (* Returns the formal universe that lies just above the universe variable u.
      Used to type the sort u. *)
   let super l = 
     if is_small l then type1
@@ -655,7 +661,6 @@ type canonical_arc =
       lt: Level.t list;
       le: Level.t list;
       rank : int;
-      predicative : bool;
       mutable status : status;
       (** Guaranteed to be unset out of the [compare_neq] functions. It is used
           to do an imperative traversal of the graph, ensuring a O(1) check that
@@ -670,7 +675,7 @@ let arc_is_lt arc = match arc.status with
 | Unset | SetLe -> false
 | SetLt -> true
 
-let terminal u = {univ=u; lt=[]; le=[]; rank=0; predicative=false; status = Unset}
+let terminal u = {univ=u; lt=[]; le=[]; rank=0; status = Unset}
 
 module UMap :
 sig
@@ -720,35 +725,51 @@ let enter_arc ca g =
 
 (* Every Level.t has a unique canonical arc representative *)
 
+(** The graph always contains nodes for Prop and Set. *)
+
+let terminal_lt u v =
+  {(terminal u) with lt=[v]}
+    
+let empty_universes =
+  let g = enter_arc (terminal Level.set) UMap.empty in
+  let g = enter_arc (terminal_lt Level.prop Level.set) g in
+    g
+
 (* repr : universes -> Level.t -> canonical_arc *)
 (* canonical representative : we follow the Equiv links *)
 
-let repr g u =
-  let rec repr_rec u =
-    let a =
-      try UMap.find u g
-      with Not_found -> anomaly ~label:"Univ.repr"
-	  (str"Universe " ++ Level.pr u ++ str" undefined")
-    in
-    match a with
-      | Equiv v -> repr_rec v
-      | Canonical arc -> arc
+let rec repr g u =
+  let a =
+    try UMap.find u g
+    with Not_found -> anomaly ~label:"Univ.repr"
+        (str"Universe " ++ Level.pr u ++ str" undefined")
   in
-  repr_rec u
+  match a with
+    | Equiv v -> repr g v
+    | Canonical arc -> arc
 
-(* [safe_repr] also search for the canonical representative, but
-   if the graph doesn't contain the searched universe, we add it. *)
+let get_prop_arc g = repr g Level.prop
+let get_set_arc g = repr g Level.set
+let is_set_arc u = Level.is_set u.univ
+let is_prop_arc u = Level.is_prop u.univ
 
-let safe_repr g u =
-  let rec safe_repr_rec u =
-    match UMap.find u g with
-      | Equiv v -> safe_repr_rec v
-      | Canonical arc -> arc
-  in
-  try g, safe_repr_rec u
-  with Not_found ->
-    let can = terminal u in
-    enter_arc can g, can
+exception AlreadyDeclared
+	    
+let add_universe vlev strict g =
+  try
+    let _arcv = UMap.find vlev g in
+      raise AlreadyDeclared
+  with Not_found -> 
+    let v = terminal vlev in
+    let arc =
+      let arc = get_set_arc g in
+	if strict then
+	  { arc with lt=vlev::arc.lt}
+	else 
+	  { arc with le=vlev::arc.le}
+    in
+    let g = enter_arc arc g in
+      enter_arc v g
 
 (* reprleq : canonical_arc -> canonical_arc list *)
 (* All canonical arcv such that arcu<=arcv with arcv#arcu *)
@@ -792,7 +813,6 @@ let between g arcu arcv =
   in
   let good,_,_ = explore ([arcv],[],false) arcu in
     good
-
 (* We assume  compare(u,v) = LE with v canonical (see compare below).
    In this case List.hd(between g u v) = repr u
    Otherwise, between g u v = []
@@ -903,8 +923,9 @@ let get_explanation strict g arcu arcv =
         in
         find [] arc.lt
   in
+  let start = (* if is_prop_arc arcu then [Le, make arcv.univ] else *) [] in
   try
-    let (to_revert, c) = cmp [] [] [] [(arcu, [])] in
+    let (to_revert, c) = cmp start [] [] [(arcu, [])] in
     (** Reset all the touched arcs. *)
     let () = List.iter (fun arc -> arc.status <- Unset) to_revert in
     List.rev c
@@ -928,25 +949,8 @@ let fast_compare_neq strict g arcu arcv =
     if arc_is_lt arc then
       cmp c to_revert lt_todo le_todo
     else
-      let rec find lt_todo lt le = match le with
-      | [] ->
-        begin match lt with
-        | [] ->
-          let () = arc.status <- SetLt in
-          cmp c (arc :: to_revert) lt_todo le_todo
-        | u :: lt ->
-          let arc = repr g u in
-          if arc == arcv then
-            if strict then (to_revert, FastLT) else (to_revert, FastLE)
-          else find (arc :: lt_todo) lt le
-        end
-      | u :: le ->
-        let arc = repr g u in
-        if arc == arcv then
-          if strict then (to_revert, FastLT) else (to_revert, FastLE)
-        else find (arc :: lt_todo) lt le
-      in
-      find lt_todo arc.lt arc.le
+      let () = arc.status <- SetLt in
+      process_lt c (arc :: to_revert) lt_todo le_todo arc.lt arc.le
   | [], arc::le_todo ->
     if arc == arcv then
       (* No need to continue inspecting universes above arc:
@@ -958,22 +962,39 @@ let fast_compare_neq strict g arcu arcv =
       if arc_is_le arc then
         cmp c to_revert [] le_todo
       else
-        let rec find lt_todo lt = match lt with
-        | [] ->
-          let fold accu u =
-            let node = repr g u in
-            node :: accu
-          in
-          let le_new = List.fold_left fold le_todo arc.le in
-          let () = arc.status <- SetLe in
-          cmp c (arc :: to_revert) lt_todo le_new
-        | u :: lt ->
-          let arc = repr g u in
-          if arc == arcv then
-            if strict then (to_revert, FastLT) else (to_revert, FastLE)
-          else find (arc :: lt_todo) lt
-        in
-        find [] arc.lt
+        let () = arc.status <- SetLe in
+        process_le c (arc :: to_revert) [] le_todo arc.lt arc.le
+
+  and process_lt c to_revert lt_todo le_todo lt le = match le with
+  | [] ->
+    begin match lt with
+    | [] -> cmp c to_revert lt_todo le_todo
+    | u :: lt ->
+      let arc = repr g u in
+      if arc == arcv then
+        if strict then (to_revert, FastLT) else (to_revert, FastLE)
+      else process_lt c to_revert (arc :: lt_todo) le_todo lt le
+    end
+  | u :: le ->
+    let arc = repr g u in
+    if arc == arcv then
+      if strict then (to_revert, FastLT) else (to_revert, FastLE)
+    else process_lt c to_revert (arc :: lt_todo) le_todo lt le
+
+  and process_le c to_revert lt_todo le_todo lt le = match lt with
+  | [] ->
+    let fold accu u =
+      let node = repr g u in
+      node :: accu
+    in
+    let le_new = List.fold_left fold le_todo le in
+    cmp c to_revert lt_todo le_new
+  | u :: lt ->
+    let arc = repr g u in
+    if arc == arcv then
+      if strict then (to_revert, FastLT) else (to_revert, FastLE)
+    else process_le c to_revert (arc :: lt_todo) le_todo lt le
+
   in
   try
     let (to_revert, c) = cmp FastNLE [] [] [arcu] in
@@ -1017,24 +1038,18 @@ let is_lt g arcu arcv =
 (** First, checks on universe levels *)
 
 let check_equal g u v =
-  let g, arcu = safe_repr g u in
-  let _, arcv = safe_repr g v in
-  arcu == arcv
+  let arcu = repr g u and arcv = repr g v in
+    arcu == arcv
 
 let check_eq_level g u v = u == v || check_equal g u v
 
-let is_set_arc u = Level.is_set u.univ
-let is_prop_arc u = Level.is_prop u.univ
-let get_prop_arc g = snd (safe_repr g Level.prop)
-
 let check_smaller g strict u v =
-  let g, arcu = safe_repr g u in
-  let g, arcv = safe_repr g v in
+  let arcu = repr g u and arcv = repr g v in
   if strict then
     is_lt g arcu arcv
   else
     is_prop_arc arcu 
-    || (is_set_arc arcu && arcv.predicative) 
+    || (is_set_arc arcu && not (is_prop_arc arcv))
     || is_leq g arcu arcv
 
 (** Then, checks on universes *)
@@ -1076,19 +1091,11 @@ let check_leq g u v =
 
 (** Enforcing new constraints : [setlt], [setleq], [merge], [merge_disc] *)
 
-(** To speed up tests of Set </<= i *)
-let set_predicative g arcv = 
-  enter_arc {arcv with predicative = true} g
-
 (* setlt : Level.t -> Level.t -> reason -> unit *)
 (* forces u > v *)
 (* this is normally an update of u in g rather than a creation. *)
 let setlt g arcu arcv =
   let arcu' = {arcu with lt=arcv.univ::arcu.lt} in
-  let g = 
-    if is_set_arc arcu then set_predicative g arcv
-    else g
-  in
     enter_arc arcu' g, arcu'
 
 (* checks that non-redundant *)
@@ -1102,11 +1109,6 @@ let setlt_if (g,arcu) v =
 (* this is normally an update of u in g rather than a creation. *)
 let setleq g arcu arcv =
   let arcu' = {arcu with le=arcv.univ::arcu.le} in
-  let g = 
-    if is_set_arc arcu' then
-      set_predicative g arcv
-    else g
-  in
     enter_arc arcu' g, arcu'
 
 (* checks that non-redundant *)
@@ -1122,7 +1124,8 @@ let merge g arcu arcv =
   (* we find the arc with the biggest rank, and we redirect all others to it *)
   let arcu, g, v =
     let best_ranked (max_rank, old_max_rank, best_arc, rest) arc =
-      if Level.is_small arc.univ || arc.rank >= max_rank
+      if Level.is_small arc.univ ||
+	   (arc.rank >= max_rank && not (Level.is_small best_arc.univ))
       then (arc.rank, max_rank, arc, best_arc::rest)
       else (max_rank, old_max_rank, best_arc, arc::rest)
     in
@@ -1152,7 +1155,7 @@ let merge g arcu arcv =
 (* we assume  compare(u,v) = compare(v,u) = NLE *)
 (* merge_disc u v  forces u ~ v with repr u as canonical repr *)
 let merge_disc g arc1 arc2 =
-  let arcu, arcv = if arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
+  let arcu, arcv = if Level.is_small arc2.univ || arc1.rank < arc2.rank then arc2, arc1 else arc1, arc2 in
   let arcu, g = 
     if not (Int.equal arc1.rank arc2.rank) then arcu, g
     else
@@ -1175,12 +1178,11 @@ exception UniverseInconsistency of univ_inconsistency
 let error_inconsistency o u v (p:explanation option) =
   raise (UniverseInconsistency (o,make u,make v,p))
 
-(* enforc_univ_eq : Level.t -> Level.t -> unit *)
-(* enforc_univ_eq u v will force u=v if possible, will fail otherwise *)
+(* enforce_univ_eq : Level.t -> Level.t -> unit *)
+(* enforce_univ_eq u v will force u=v if possible, will fail otherwise *)
 
 let enforce_univ_eq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u and arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastEQ -> g
     | FastLT ->
@@ -1199,8 +1201,7 @@ let enforce_univ_eq u v g =
 (* enforce_univ_leq : Level.t -> Level.t -> unit *)
 (* enforce_univ_leq u v will force u<=v if possible, will fail otherwise *)
 let enforce_univ_leq u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u and arcv = repr g v in
   if is_leq g arcu arcv then g
   else
     match fast_compare g arcv arcu with
@@ -1213,8 +1214,7 @@ let enforce_univ_leq u v g =
 
 (* enforce_univ_lt u v will force u<v if possible, will fail otherwise *)
 let enforce_univ_lt u v g =
-  let g,arcu = safe_repr g u in
-  let g,arcv = safe_repr g v in
+  let arcu = repr g u and arcv = repr g v in
     match fast_compare g arcu arcv with
     | FastLT -> g
     | FastLE -> fst (setlt g arcu arcv)
@@ -1227,18 +1227,10 @@ let enforce_univ_lt u v g =
         let p = get_explanation false g arcv arcu  in
         error_inconsistency Lt u v p
 
-let empty_universes = UMap.empty
-
 (* Prop = Set is forbidden here. *)
-let initial_universes = enforce_univ_lt Level.prop Level.set UMap.empty
+let initial_universes = empty_universes
 
 let is_initial_universes g = UMap.equal (==) g initial_universes
-
-let add_universe vlev g = 
-  let v = terminal vlev in
-  let proparc = get_prop_arc g in
-    enter_arc {proparc with le=vlev::proparc.le}
-      (enter_arc v g)
       
 (* Constraints and sets of constraints. *)    
 
@@ -1372,10 +1364,12 @@ let check_univ_leq u v =
 
 let enforce_leq u v c =
   let open Universe.Huniv in
+  let rec aux acc v =
   match v with
-  | Cons (v, _, Nil) ->
-    fold (fun u -> constraint_add_leq u v) u c
-  | _ -> anomaly (Pp.str"A universe bound can only be a variable")
+  | Cons (v, _, l) ->
+    aux (fold (fun u -> constraint_add_leq u v) u c) l
+  | Nil -> acc
+  in aux c v
 
 let enforce_leq u v c =
   if check_univ_leq u v then c
@@ -1446,7 +1440,6 @@ let normalize_universes g =
         lt = LSet.elements lt;
         le = LSet.elements le;
 	rank = rank;
-	predicative = false;
 	status = Unset;
       }
   in
@@ -1589,9 +1582,9 @@ let sort_universes orig =
   let sorted = LMap.fold fold compact UMap.empty in
   (** Add all [Type.n] nodes *)
   let fold i accu u =
-    if 0 < i then
-      let pred = types.(i - 1) in
-      let arc = {univ = u; lt = [pred]; le = []; rank = 0; predicative = false; status = Unset; } in
+    if i < max then
+      let pred = types.(i + 1) in
+      let arc = {univ = u; lt = [pred]; le = []; rank = 0; status = Unset; } in
       UMap.add u (Canonical arc) accu
     else accu
   in
@@ -1761,7 +1754,7 @@ let eq_puniverses f (x, u) (y, u') =
   f x y && Instance.equal u u'
 
 (** A context of universe levels with universe constraints,
-    representiong local universe variables and constraints *)
+    representing local universe variables and constraints *)
 
 module UContext =
 struct
@@ -1775,7 +1768,7 @@ struct
 
   let pr prl (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      Instance.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
+      h 0 (Instance.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 
   let hcons (univs, cst) =
     (Instance.hcons univs, hcons_constraints cst)
@@ -1785,8 +1778,11 @@ struct
 
   let union (univs, cst) (univs', cst') =
     Instance.append univs univs', Constraint.union cst cst'
-      
+
   let dest x = x
+
+  let size (x,_) = Instance.length x
+
 end
 
 type universe_context = UContext.t
@@ -1804,6 +1800,9 @@ struct
   let empty = (LSet.empty, Constraint.empty)
   let is_empty (univs, cst) = LSet.is_empty univs && Constraint.is_empty cst
 
+  let equal (univs, cst as x) (univs', cst' as y) =
+    x == y || (LSet.equal univs univs' && Constraint.equal cst cst')
+									
   let of_set s = (s, Constraint.empty)
   let singleton l = of_set (LSet.singleton l)
   let of_instance i = of_set (Instance.levels i)
@@ -1843,7 +1842,7 @@ struct
 
   let pr prl (univs, cst as ctx) =
     if is_empty ctx then mt() else
-      LSet.pr prl univs ++ str " |= " ++ v 0 (Constraint.pr prl cst)
+      h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst))
 
   let constraints (univs, cst) = cst
   let levels (univs, cst) = univs
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7aaf2ffe..c926c57b 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -20,7 +20,11 @@ sig
 
   val is_small : t -> bool
   (** Is the universe set or prop? *)
-
+		       
+  val is_prop : t -> bool
+  val is_set : t -> bool
+  (** Is it specifically Prop or Set *)
+		       
   val compare : t -> t -> int
   (** Comparison function *)
 
@@ -87,6 +91,9 @@ sig
   val is_level : t -> bool
   (** Test if the universe is a level or an algebraic universe. *)
 
+  val is_levels : t -> bool
+  (** Test if the universe is a lub of levels or contains +n's. *)
+
   val level : t -> Level.t option
   (** Try to get a level out of a universe, returns [None] if it
       is an algebraic universe. *)
@@ -159,8 +166,12 @@ val is_initial_universes : universes -> bool
 
 val sort_universes : universes -> universes
 
-(** Adds a universe to the graph, ensuring it is >= Prop. *)
-val add_universe : universe_level -> universes -> universes
+(** Adds a universe to the graph, ensuring it is >= or > Set.
+   @raises AlreadyDeclared if the level is already declared in the graph. *)
+
+exception AlreadyDeclared
+
+val add_universe : universe_level -> bool -> universes -> universes
 
 (** {6 Constraints. } *)
 
@@ -332,6 +343,9 @@ sig
   (** Keeps the order of the instances *)
   val union : t -> t -> t
 
+  (* the number of universes in the context *)
+  val size : t -> int
+
 end
 
 type universe_context = UContext.t
@@ -349,6 +363,7 @@ sig
   val of_instance : Instance.t -> t
   val of_set : universe_set -> t
 
+  val equal : t -> t -> bool
   val union : t -> t -> t
 
   val append : t -> t -> t
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 88c1e103..a800e253 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -337,5 +337,5 @@ let subst_instance_context s ctx =
   if Univ.Instance.is_empty s then ctx
   else map_rel_context (fun x -> subst_instance_constr s x) ctx
 
-type id_key = pconstant tableKey
-let eq_id_key x y = Names.eq_table_key (Univ.eq_puniverses Constant.equal) x y
+type id_key = constant tableKey
+let eq_id_key x y = Names.eq_table_key Constant.equal x y
diff --git a/kernel/vars.mli b/kernel/vars.mli
index fdd4603b..c0fbeeb6 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -88,5 +88,5 @@ val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_
 val subst_instance_constr : universe_instance -> constr -> constr
 val subst_instance_context : universe_instance -> rel_context -> rel_context
 
-type id_key = pconstant tableKey
+type id_key = constant tableKey
 val eq_id_key : id_key -> id_key -> bool
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 1c31cc04..4610dbcb 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -18,8 +18,8 @@ let compare_zipper z1 z2 =
   match z1, z2 with
   | Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2)
   | Zfix(f1,args1), Zfix(f2,args2) ->  Int.equal (nargs args1) (nargs args2)
-  | Zswitch _, Zswitch _ -> true
-  | _ , _ -> false
+  | Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true
+  | Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false
 
 let rec compare_stack stk1 stk2 =
   match stk1, stk2 with
@@ -40,15 +40,20 @@ let conv_vect fconv vect1 vect2 cu =
     !rcu
   else raise NotConvertible
 
-let infos = ref (create_clos_infos betaiotazeta Environ.empty_env)
-
 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
 
 and conv_whd env pb k whd1 whd2 cu =
+(*  Pp.(msg_debug (str "conv_whd(" ++ pr_whd whd1 ++ str ", " ++ pr_whd whd2 ++ str ")")) ; *)
   match whd1, whd2 with
-  | Vsort s1, Vsort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu
+  | Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu
+  | Vuniv_level _ , _
+  | _ , Vuniv_level _ ->
+    (** Both of these are invalid since universes are handled via
+     ** special cases in the code.
+     **)
+    assert false
   | Vprod p1, Vprod p2 ->
       let cu = conv_val env CONV k (dom p1) (dom p2) cu in
       conv_fun env pb k (codom p1) (codom p2) cu
@@ -76,50 +81,53 @@ and conv_whd env pb k whd1 whd2 cu =
   | Vatom_stk(a1,stk1), Vatom_stk(a2,stk2) ->
       conv_atom env pb k a1 stk1 a2 stk2 cu
   | Vfun _, _ | _, Vfun _ ->
-      conv_val env CONV (k+1) (eta_whd k whd1) (eta_whd k whd2) cu
-  | _, Vatom_stk(Aiddef(_,v),stk) ->
-      conv_whd env pb k whd1 (force_whd v stk) cu
-  | Vatom_stk(Aiddef(_,v),stk), _ ->
-      conv_whd env pb k (force_whd v stk) whd2 cu
-  | _, _ -> raise NotConvertible
+      conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu
+
+  | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _  | Vconstr_const _, _
+  | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible
+
 
 and conv_atom env pb k a1 stk1 a2 stk2 cu =
+(*  Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *)
   match a1, a2 with
-  | Aind ind1, Aind ind2 ->
-      if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2
+  | Aind ((mi,i) as ind1) , Aind ind2 ->
+      if eq_ind ind1 ind2 && compare_stack stk1 stk2
       then
-	conv_stack env k stk1 stk2 cu
+        if Environ.polymorphic_ind ind1 env
+        then
+          let mib = Environ.lookup_mind mi env in
+	  let ulen = Univ.UContext.size mib.Declarations.mind_universes in
+          match stk1 , stk2 with
+	  | [], [] -> assert (Int.equal ulen 0); cu
+	  | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
+	     assert (ulen <= nargs args1);
+             assert (ulen <= nargs args2);
+	     let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in
+	     let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in
+	     let u1 = Univ.Instance.of_array u1 in
+	     let u2 = Univ.Instance.of_array u2 in
+	     let cu = convert_instances ~flex:false u1 u2 cu in
+             conv_arguments env ~from:ulen k args1 args2
+			    (conv_stack env k stk1' stk2' cu)
+	  | _, _ -> assert false (* Should not happen if problem is well typed *)
+        else
+	  conv_stack env k stk1 stk2 cu
       else raise NotConvertible
   | Aid ik1, Aid ik2 ->
       if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
 	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
-  | Aiddef(ik1,v1), Aiddef(ik2,v2) ->
-      begin
-	try
-	  if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
-	    conv_stack env k stk1 stk2 cu
-	  else raise NotConvertible
-	with NotConvertible ->
-	  if oracle_order Univ.out_punivs (oracle_of_infos !infos) 
-	    false ik1 ik2 then
-            conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu
-          else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu
-      end
-  | Aiddef(ik1,v1), _ ->
-      conv_whd env pb k (force_whd v1 stk1) (Vatom_stk(a2,stk2)) cu
-  | _, Aiddef(ik2,v2) ->
-      conv_whd env pb k (Vatom_stk(a1,stk1)) (force_whd v2 stk2) cu
-  | _, _ -> raise NotConvertible
+  | Atype _ , _ | _, Atype _ -> assert false
+  | Aind _, _ | Aid _, _ -> raise NotConvertible
 
-and conv_stack env k stk1 stk2 cu =
+and conv_stack env ?from:(from=0) k stk1 stk2 cu =
   match stk1, stk2 with
   | [], [] -> cu
   | Zapp args1 :: stk1, Zapp args2 :: stk2 ->
-      conv_stack env k stk1 stk2 (conv_arguments env k args1 args2 cu)
+      conv_stack env k stk1 stk2 (conv_arguments env ~from:from k args1 args2 cu)
   | Zfix(f1,args1) :: stk1, Zfix(f2,args2) :: stk2 ->
       conv_stack env k stk1 stk2
-	(conv_arguments env k args1 args2 (conv_fix env k f1 f2 cu))
+	(conv_arguments env ~from:from k args1 args2 (conv_fix env k f1 f2 cu))
   | Zswitch sw1 :: stk1, Zswitch sw2 :: stk2 ->
       if check_switch sw1 sw2 then
 	let vt1,vt2 = type_of_switch sw1, type_of_switch sw2 in
@@ -131,7 +139,11 @@ and conv_stack env k stk1 stk2 cu =
 	done;
 	conv_stack env k stk1 stk2 !rcu
       else raise NotConvertible
-  | _, _ -> raise NotConvertible
+  | Zproj p1 :: stk1, Zproj p2 :: stk2 ->
+    if Constant.equal p1 p2 then conv_stack env k stk1 stk2 cu
+    else raise NotConvertible
+  | [], _ | Zapp _ :: _, _ | Zfix _ :: _, _ | Zswitch _ :: _, _
+  | Zproj _ :: _, _ -> raise NotConvertible
 
 and conv_fun env pb k f1 f2 cu =
   if f1 == f2 then cu
@@ -159,98 +171,37 @@ and conv_cofix env k cf1 cf2 cu =
       conv_vect (conv_val env CONV (k + Array.length tcf1)) bcf1 bcf2 cu
     else raise NotConvertible
 
-and conv_arguments env k args1 args2 cu =
+and conv_arguments env ?from:(from=0) k args1 args2 cu =
   if args1 == args2 then cu
   else
     let n = nargs args1 in
     if Int.equal n (nargs args2) then
       let rcu = ref cu in
-      for i = 0 to n - 1 do
+      for i = from to n - 1 do
 	rcu := conv_val env CONV k (arg args1 i) (arg args2 i) !rcu
       done;
       !rcu
     else raise NotConvertible
 
-let rec eq_puniverses f (x,l1) (y,l2) cu =
-  if f x y then conv_universes l1 l2 cu
-  else raise NotConvertible
-
-and conv_universes l1 l2 cu =
-  if Univ.Instance.equal l1 l2 then cu else raise NotConvertible
-
-let rec conv_eq env pb t1 t2 cu =
-  if t1 == t2 then cu
-  else
-    match kind_of_term t1, kind_of_term t2 with
-    | Rel n1, Rel n2 ->
-	if Int.equal n1 n2 then cu else raise NotConvertible
-    | Meta m1, Meta m2 ->
-	if Int.equal m1 m2 then cu else raise NotConvertible
-    | Var id1, Var id2 ->
-	if Id.equal id1 id2 then cu else raise NotConvertible
-    | Sort s1, Sort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu
-    | Cast (c1,_,_), _ -> conv_eq env pb c1 t2 cu
-    | _, Cast (c2,_,_) -> conv_eq env pb t1 c2 cu
-    | Prod (_,t1,c1), Prod (_,t2,c2) ->
-	conv_eq env pb c1 c2 (conv_eq env CONV t1 t2 cu)
-    | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq env CONV c1 c2 cu
-    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) ->
-	conv_eq env pb c1 c2 (conv_eq env CONV b1 b2 cu)
-    | App (c1,l1), App (c2,l2) ->
-	conv_eq_vect env l1 l2 (conv_eq env CONV c1 c2 cu)
-    | Evar (e1,l1), Evar (e2,l2) ->
-	if Evar.equal e1 e2 then conv_eq_vect env l1 l2 cu
-	else raise NotConvertible
-    | Const c1, Const c2 -> eq_puniverses eq_constant c1 c2 cu
-    | Proj (p1,c1), Proj (p2,c2) ->
-	if eq_constant (Projection.constant p1) (Projection.constant p2) then
-	  conv_eq env pb c1 c2 cu 
-	else raise NotConvertible
-    | Ind c1, Ind c2 ->
-       eq_puniverses eq_ind c1 c2 cu
-    | Construct c1, Construct c2 ->
-       eq_puniverses eq_constructor c1 c2 cu
-    | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) ->
-	let pcu = conv_eq env CONV p1 p2 cu in
-	let ccu = conv_eq env CONV c1 c2 pcu in
-	conv_eq_vect env bl1 bl2 ccu
-    | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) ->
-	if Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu)
-	else raise NotConvertible
-    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-	if Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu)
-	else raise NotConvertible
-    | _ -> raise NotConvertible
-
-and conv_eq_vect env vt1 vt2 cu =
-  let len = Array.length vt1 in
-  if Int.equal len (Array.length vt2) then
-    let rcu = ref cu in
-    for i = 0 to len-1 do
-      rcu := conv_eq env CONV vt1.(i) vt2.(i) !rcu
-    done; !rcu
-  else raise NotConvertible
-
-let vconv pb env t1 t2 =
-  infos := create_clos_infos betaiotazeta env;
-  let _cu =
-    try conv_eq env pb t1 t2 (universes env)
-    with NotConvertible ->
-      let v1 = val_of_constr env t1 in
-      let v2 = val_of_constr env t2 in
-      let cu = conv_val env pb (nb_rel env) v1 v2 (universes env) in
-      cu
-  in ()
-
-let _ = Reduction.set_vm_conv vconv
-
-let use_vm = ref false
-
-let set_use_vm b =
-  use_vm := b;
-  if b then Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> vconv cv_pb)
-  else Reduction.set_default_conv (fun cv_pb ?(l2r=false) -> Reduction.conv_cmp cv_pb)
-
-let use_vm _ = !use_vm
-
-
+let vm_conv_gen cv_pb env univs t1 t2 =
+  try 
+    let v1 = val_of_constr env t1 in
+    let v2 = val_of_constr env t2 in
+    fst (conv_val env cv_pb (nb_rel env) v1 v2 univs)
+  with Not_found | Invalid_argument _ ->
+    (Pp.msg_warning
+      (Pp.str "Bytecode compilation failed, falling back to default conversion");
+     Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None)
+			    full_transparent_state env univs t1 t2)
+
+let vm_conv cv_pb env t1 t2 =
+  let univs = Environ.universes env in
+  let b =
+    if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2
+    else Constr.eq_constr_univs univs t1 t2
+  in
+  if not b then
+    let univs = (univs, checked_universes) in
+    let _ = vm_conv_gen cv_pb env univs t1 t2 in ()
+
+let _ = Reduction.set_vm_conv vm_conv
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 096d31ac..49e5d23e 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -12,9 +12,11 @@ open Reduction
 
 (**********************************************************************
   s conversion functions *)
-val use_vm : unit -> bool
-val set_use_vm : bool -> unit
-val vconv : conv_pb -> types conversion_function
+val vm_conv : conv_pb -> types conversion_function
 
-val val_of_constr : env -> constr -> values
+(** A conversion function parametrized by a universe comparator. Used outside of
+    the kernel. *)
+val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function
 
+(** Precompute a VM value from a constr *)
+val val_of_constr : env -> constr -> values
diff --git a/kernel/vm.ml b/kernel/vm.ml
index d4bf461b..64ddc437 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -19,8 +19,6 @@ external set_drawinstr : unit -> unit = "coq_set_drawinstr"
 external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
 external offset : Obj.t -> int = "coq_offset"
 
-let accu_tag = 0
-
 (*******************************************)
 (* Initalization of the abstract machine ***)
 (*******************************************)
@@ -29,9 +27,6 @@ external init_vm : unit -> unit = "init_coq_vm"
 
 let _ = init_vm ()
 
-external transp_values : unit -> bool = "get_coq_transp_value"
-external set_transp_values : bool -> unit = "coq_set_transp_value"
-
 (*******************************************)
 (* Machine code *** ************************)
 (*******************************************)
@@ -126,11 +121,12 @@ type vswitch = {
 (*                                                                        *)
 (* + Accumulators : At_[accumulate| accu | arg1 | ... | argn ]            *)
 (*   - representation of [accu] : tag_[....]                              *)
-(*     -- tag <= 2 : encoding atom type (sorts, free vars, etc.)          *)
-(*     -- 3_[accu|fix_app] : a fixpoint blocked by an accu                *)
-(*     -- 4_[accu|vswitch] : a match blocked by an accu                   *)
-(*     -- 5_[fcofix]       : a cofix function                             *)
-(*     -- 6_[fcofix|val]   : a cofix function, val represent the value    *)
+(*     -- tag <= 3 : encoding atom type (sorts, free vars, etc.)          *)
+(*     -- 10_[accu|proj name] : a projection blocked by an accu           *)
+(*     -- 11_[accu|fix_app] : a fixpoint blocked by an accu               *)
+(*     -- 12_[accu|vswitch] : a match blocked by an accu                  *)
+(*     -- 13_[fcofix]       : a cofix function                            *)
+(*     -- 14_[fcofix|val]   : a cofix function, val represent the value   *)
 (*        of the function applied to arg1 ... argn                        *)
 (* The [arguments] type, which is abstracted as an array, represents :    *)
 (*          tag[ _ | _ |v1|... | vn]                                      *)
@@ -140,8 +136,8 @@ type vswitch = {
 
 type atom =
   | Aid of Vars.id_key
-  | Aiddef of Vars.id_key * values
-  | Aind of pinductive
+  | Aind of inductive
+  | Atype of Univ.universe
 
 (* Zippers *)
 
@@ -149,6 +145,7 @@ type zipper =
   | Zapp of arguments
   | Zfix of vfix*arguments  (* Possibly empty *)
   | Zswitch of vswitch
+  | Zproj of Constant.t (* name of the projection *)
 
 type stack = zipper list
 
@@ -163,28 +160,112 @@ type whd =
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vatom_stk of atom * stack
+  | Vuniv_level of Univ.universe_level
+
+(************************************************)
+(* Abstract machine *****************************)
+(************************************************)
+
+(* gestion de la pile *)
+external push_ra : tcode -> unit = "coq_push_ra"
+external push_val : values -> unit = "coq_push_val"
+external push_arguments : arguments -> unit = "coq_push_arguments"
+external push_vstack : vstack -> unit = "coq_push_vstack"
+
+
+(* interpreteur *)
+external interprete : tcode -> values -> vm_env -> int -> values =
+  "coq_interprete_ml"
+
+
+
+(* Functions over arguments *)
+let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
+let arg args i =
+  if  0 <= i && i < (nargs args) then
+    val_of_obj (Obj.field (Obj.repr args) (i+2))
+  else invalid_arg
+		("Vm.arg size = "^(string_of_int (nargs args))^
+		 " acces "^(string_of_int i))
+
+(* Apply a value to arguments contained in [vargs] *)
+let apply_arguments vf vargs =
+  let n = nargs vargs in
+  if Int.equal n 0 then vf
+  else
+   begin
+     push_ra stop;
+     push_arguments vargs;
+     interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
+   end
+
+(* Apply value [vf] to an array of argument values [varray] *)
+let apply_varray vf varray =
+  let n = Array.length varray in
+  if Int.equal n 0 then vf
+  else
+    begin
+      push_ra stop;
+      push_vstack varray;
+      interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
+    end
 
 (*************************************************)
 (* Destructors ***********************************)
 (*************************************************)
 
+let uni_lvl_val (v : values) : Univ.universe_level =
+    let whd = Obj.magic v in
+    match whd with
+    | Vuniv_level lvl -> lvl
+    | _ ->
+      let pr =
+        let open Pp in
+        match whd with
+        | Vsort _ -> str "Vsort"
+        | Vprod _ -> str "Vprod"
+        | Vfun _ -> str "Vfun"
+        | Vfix _ -> str "Vfix"
+        | Vcofix _ -> str "Vcofix"
+        | Vconstr_const i -> str "Vconstr_const"
+        | Vconstr_block b -> str "Vconstr_block"
+        | Vatom_stk (a,stk) -> str "Vatom_stk"
+        | _ -> assert false
+      in
+      Errors.anomaly
+        Pp.(   strbrk "Parsing virtual machine value expected universe level, got "
+            ++ pr)
+
 let rec whd_accu a stk =
   let stk =
     if Int.equal (Obj.size a) 2 then stk
     else Zapp (Obj.obj a) :: stk in
   let at = Obj.field a 1 in
   match Obj.tag at with
-  | i when i <= 2 ->
+  | i when Int.equal i type_atom_tag ->
+     begin match stk with
+     | [Zapp args] ->
+	let u = ref (Obj.obj (Obj.field at 0)) in
+	for i = 0 to nargs args - 1 do
+	  u := Univ.Universe.sup !u (Univ.Universe.make (uni_lvl_val (arg args i)))
+	done;
+	Vsort (Type !u)
+     | _ -> assert false
+     end
+  | i when i <= max_atom_tag ->
       Vatom_stk(Obj.magic at, stk)
-  | 3 (* fix_app tag *) ->
+  | i when Int.equal i proj_tag ->
+     let zproj = Zproj (Obj.obj (Obj.field at 0)) in
+     whd_accu (Obj.field at 1) (zproj :: stk)
+  | i when Int.equal i fix_app_tag ->
       let fa = Obj.field at 1 in
       let zfix  =
 	Zfix (Obj.obj (Obj.field fa 1), Obj.obj fa) in
       whd_accu (Obj.field at 0) (zfix :: stk)
-  | 4 (* switch tag  *) ->
+  | i when Int.equal i switch_tag ->
       let zswitch = Zswitch (Obj.obj (Obj.field at 1)) in
       whd_accu (Obj.field at 0) (zswitch :: stk)
-  | 5 (* cofix_tag *) ->
+  | i when Int.equal i cofix_tag ->
       let vcfx = Obj.obj (Obj.field at 0) in
       let to_up = Obj.obj a in
       begin match stk with
@@ -192,7 +273,7 @@ let rec whd_accu a stk =
       | [Zapp args] -> Vcofix(vcfx, to_up, Some args)
       | _           -> assert false
       end
-  | 6 (* cofix_evaluated_tag *) ->
+  | i when Int.equal i cofix_evaluated_tag ->
       let vcofix = Obj.obj (Obj.field at 0) in
       let res = Obj.obj a in
       begin match stk with
@@ -200,7 +281,9 @@ let rec whd_accu a stk =
       | [Zapp args] -> Vcofix(vcofix, res, Some args)
       | _           -> assert false
       end
-  | _ -> assert false
+  | tg ->
+    Errors.anomaly
+      Pp.(strbrk "Failed to parse VM value. Tag = " ++ int tg)
 
 external kind_of_closure : Obj.t -> int = "coq_kind_of_closure"
 
@@ -213,65 +296,19 @@ let whd_val : values -> whd =
       if tag = accu_tag then
 	(
 	if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *)
-	else
+        else
 	  if is_accumulate (fun_code o) then whd_accu o []
-	  else (Vprod(Obj.obj o)))
+	  else Vprod(Obj.obj o))
       else
 	if tag = Obj.closure_tag || tag = Obj.infix_tag then
-	  (	   match kind_of_closure o with
+	  (match kind_of_closure o with
 	   | 0 -> Vfun(Obj.obj o)
 	   | 1 -> Vfix(Obj.obj o, None)
 	   | 2 -> Vfix(Obj.obj (Obj.field o 1), Some (Obj.obj o))
 	   | 3 -> Vatom_stk(Aid(RelKey(int_tcode (fun_code o) 1)), [])
 	   | _ -> Errors.anomaly ~label:"Vm.whd " (Pp.str "kind_of_closure does not work"))
-	else 
-          Vconstr_block(Obj.obj o)
-         
-(************************************************)
-(* Abstrct machine ******************************)
-(************************************************)
-
-(* gestion de la pile *)
-external push_ra : tcode -> unit = "coq_push_ra"
-external push_val : values -> unit = "coq_push_val"
-external push_arguments : arguments -> unit = "coq_push_arguments"
-external push_vstack : vstack -> unit = "coq_push_vstack"
-
-
-(* interpreteur *)
-external interprete : tcode -> values -> vm_env -> int -> values =
-  "coq_interprete_ml"
-
-
-
-(* Functions over arguments *)
-let nargs : arguments -> int = fun args -> (Obj.size (Obj.repr args)) - 2
-let arg args i =
-  if  0 <= i && i < (nargs args) then
-    val_of_obj (Obj.field (Obj.repr args) (i+2))
-  else invalid_arg
-		("Vm.arg size = "^(string_of_int (nargs args))^
-		 " acces "^(string_of_int i))
-
-let apply_arguments vf vargs =
-  let n = nargs vargs in
-  if Int.equal n 0 then vf
-  else
-   begin
-     push_ra stop;
-     push_arguments vargs;
-     interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
-   end
-
-let apply_vstack vf vstk =
-  let n = Array.length vstk in
-  if Int.equal n 0 then vf
-  else
-    begin
-      push_ra stop;
-      push_vstack vstk;
-      interprete (fun_code vf) vf (Obj.magic vf) (n - 1)
-    end
+	else
+           Vconstr_block(Obj.obj o)
 
 (**********************************************)
 (* Constructors *******************************)
@@ -289,6 +326,7 @@ let rec obj_of_str_const str =
   match str with
   | Const_sorts s -> Obj.repr (Vsort s)
   | Const_ind ind -> obj_of_atom (Aind ind)
+  | Const_proj p -> Obj.repr p
   | Const_b0 tag -> Obj.repr tag
   | Const_bn(tag, args) ->
       let len = Array.length args in
@@ -297,6 +335,8 @@ let rec obj_of_str_const str =
 	Obj.set_field res i (obj_of_str_const args.(i))
       done;
       res
+  | Const_univ_level l -> Obj.repr (Vuniv_level l)
+  | Const_type u -> obj_of_atom (Atype u)
 
 let val_of_obj o = ((Obj.obj o) : values)
 
@@ -304,13 +344,22 @@ let val_of_str_const str = val_of_obj (obj_of_str_const str)
 
 let val_of_atom a = val_of_obj (obj_of_atom a)
 
+let atom_of_proj kn v =
+  let r = Obj.new_block proj_tag 2 in
+  Obj.set_field r 0 (Obj.repr kn);
+  Obj.set_field r 1 (Obj.repr v);
+  ((Obj.obj r) : atom)
+
+let val_of_proj kn v =
+  val_of_atom (atom_of_proj kn v)
+
 module IdKeyHash =
 struct
-  type t = pconstant tableKey
-  let equal = Names.eq_table_key (Univ.eq_puniverses Constant.equal)
+  type t = constant tableKey
+  let equal = Names.eq_table_key Constant.equal
   open Hashset.Combine
   let hash = function
-  | ConstKey (c,u) -> combinesmall 1 (Constant.hash c)
+  | ConstKey c -> combinesmall 1 (Constant.hash c)
   | VarKey id -> combinesmall 2 (Id.hash id)
   | RelKey i -> combinesmall 3 (Int.hash i)
 end
@@ -354,14 +403,14 @@ external closure_arity : vfun -> int = "coq_closure_arity"
 
 let body_of_vfun k vf =
   let vargs = mkrel_vstack k 1 in
-  apply_vstack (Obj.magic vf) vargs
+  apply_varray (Obj.magic vf) vargs
 
 let decompose_vfun2 k vf1 vf2 =
   let arity = min (closure_arity vf1) (closure_arity vf2) in
   assert (0 < arity && arity < Sys.max_array_length);
   let vargs = mkrel_vstack k arity in
-  let v1 = apply_vstack (Obj.magic vf1) vargs in
-  let v2 = apply_vstack (Obj.magic vf2) vargs in
+  let v1 = apply_varray (Obj.magic vf1) vargs in
+  let v2 = apply_varray (Obj.magic vf2) vargs in
   arity, v1, v2
 
 (* Functions over fixpoint *)
@@ -491,7 +540,7 @@ let reduce_cofix k vcf =
     let self = Obj.new_block accu_tag 2 in
     Obj.set_field self 0 (Obj.repr accumulate);
     Obj.set_field self 1 (Obj.repr atom);
-    apply_vstack (Obj.obj e) [|Obj.obj self|] in
+    apply_varray (Obj.obj e) [|Obj.obj self|] in
   (Array.init ndef cofix_body, ftyp)
 
 
@@ -544,62 +593,13 @@ let branch_of_switch k sw =
   in
   Array.map eval_branch sw.sw_annot.rtbl
 
-
-
-(* Evaluation *)
-
-let rec whd_stack v stk =
-  match stk with
-  | [] -> whd_val v
-  | Zapp args :: stkt -> whd_stack (apply_arguments v args) stkt
-  | Zfix (f,args) :: stkt ->
-      let o = Obj.repr v in
-      if Obj.is_block o && Obj.tag o = accu_tag then
-	whd_accu (Obj.repr v) stk
-      else
-	let v', stkt =
-	  match stkt with
-	  | Zapp args' :: stkt ->
-	      push_ra stop;
-	      push_arguments args';
-	      push_val v;
-	      push_arguments args;
-	      let v' =
-		interprete (fun_code f) (Obj.magic f) (Obj.magic f)
-		  (nargs args+ nargs args') in
-	      v', stkt
-	  | _ ->
-	      push_ra stop;
-	      push_val v;
-	      push_arguments args;
-	      let v' =
-		interprete (fun_code f) (Obj.magic f) (Obj.magic f)
-		  (nargs args) in
-	      v', stkt
-	in
-	whd_stack v' stkt
-  | Zswitch sw :: stkt ->
-      let o = Obj.repr v in
-      if Obj.is_block o && Obj.tag o = accu_tag then
-	if Obj.tag (Obj.field o 1) < cofix_tag then whd_accu (Obj.repr v) stk
-	else
-	  let to_up =
-	    match whd_accu (Obj.repr v) [] with
-	    | Vcofix (_, to_up, _) -> to_up
-	    | _ -> assert false in
-	  whd_stack (apply_switch sw to_up) stkt
-      else whd_stack (apply_switch sw v) stkt
-
-let rec force_whd v stk =
-  match whd_stack v stk with
-  | Vatom_stk(Aiddef(_,v),stk) -> force_whd v stk
-  | res -> res
-
-
-let rec eta_stack a stk v =
+(* Apply the term represented by a under stack stk to argument v *)
+(* t = a stk --> t v *)
+let rec apply_stack a stk v =
   match stk with
-  | [] -> apply_vstack a [|v|]
-  | Zapp args :: stk -> eta_stack (apply_arguments a args) stk v
+  | [] -> apply_varray a [|v|]
+  | Zapp args :: stk -> apply_stack (apply_arguments a args) stk v
+  | Zproj kn :: stk -> apply_stack (val_of_proj kn a) stk v
   | Zfix(f,args) :: stk ->
       let a,stk = 
 	match stk with
@@ -620,11 +620,11 @@ let rec eta_stack a stk v =
 	      interprete (fun_code f) (Obj.magic f) (Obj.magic f)
 		(nargs args) in
 	    a, stk in
-      eta_stack a stk v
+      apply_stack a stk v
   | Zswitch sw :: stk ->
-      eta_stack (apply_switch sw a) stk v
+      apply_stack (apply_switch sw a) stk v
 
-let eta_whd k whd =
+let apply_whd k whd =
   let v = val_of_rel k in
   match whd with
   | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false
@@ -643,8 +643,35 @@ let eta_whd k whd =
       push_val v;
       interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0
   | Vatom_stk(a,stk) ->
-      eta_stack (val_of_atom a) stk v 
-
-
-      
-      
+      apply_stack (val_of_atom a) stk v 
+  | Vuniv_level lvl -> assert false
+
+let rec pr_atom a =
+  Pp.(match a with
+  | Aid c -> str "Aid(" ++ (match c with
+                            | ConstKey c -> Names.pr_con c
+			    | RelKey i -> str "#" ++ int i
+			    | _ -> str "...") ++ str ")"
+  | Aind (mi,i) -> str "Aind(" ++ Names.pr_mind mi ++ str "#" ++ int i ++ str ")"
+  | Atype _ -> str "Atype(")
+and pr_whd w =
+  Pp.(match w with
+  | Vsort _ -> str "Vsort"
+  | Vprod _ -> str "Vprod"
+  | Vfun _ -> str "Vfun"
+  | Vfix _ -> str "Vfix"
+  | Vcofix _ -> str "Vcofix"
+  | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")"
+  | Vconstr_block b -> str "Vconstr_block"
+  | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")"
+  | Vuniv_level _ -> assert false)
+and pr_stack stk =
+  Pp.(match stk with
+      | [] -> str "[]"
+      | s :: stk -> pr_zipper s ++ str " :: " ++ pr_stack stk)
+and pr_zipper z =
+  Pp.(match z with
+  | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")"
+  | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")"
+  | Zswitch s -> str "Zswitch(...)"
+  | Zproj c -> str "Zproj(" ++ Names.pr_con c ++ str ")")
diff --git a/kernel/vm.mli b/kernel/vm.mli
index 51903568..43a42eb9 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -2,13 +2,10 @@ open Names
 open Term
 open Cbytecodes
 
-(** Efficient Virtual Machine *)
+(** Debug printing *)
 
 val set_drawinstr : unit -> unit
 
-val transp_values : unit -> bool
-val set_transp_values : bool -> unit
-
 (** Machine code *)
 
 type tcode
@@ -25,8 +22,8 @@ type arguments
 
 type atom =
   | Aid of Vars.id_key
-  | Aiddef of Vars.id_key * values
-  | Aind of pinductive
+  | Aind of inductive
+  | Atype of Univ.universe
 
 (** Zippers *)
 
@@ -34,6 +31,7 @@ type zipper =
   | Zapp of arguments
   | Zfix of vfix * arguments  (** might be empty *)
   | Zswitch of vswitch
+  | Zproj of Constant.t (* name of the projection *)
 
 type stack = zipper list
 
@@ -48,19 +46,24 @@ type whd =
   | Vconstr_const of int
   | Vconstr_block of vblock
   | Vatom_stk of atom * stack
+  | Vuniv_level of Univ.universe_level
+
+val pr_atom : atom -> Pp.std_ppcmds
+val pr_whd : whd -> Pp.std_ppcmds
 
 (** Constructors *)
 
 val val_of_str_const : structured_constant -> values
 val val_of_rel : int -> values
 val val_of_named : Id.t -> values
-val val_of_constant : pconstant -> values
+val val_of_constant : constant -> values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
 
 (** Destructors *)
 
 val whd_val : values -> whd
+val uni_lvl_val : values -> Univ.universe_level
 
 (** Arguments *)
 
@@ -105,10 +108,6 @@ val case_info : vswitch -> case_info
 val type_of_switch : vswitch -> values
 val branch_of_switch : int -> vswitch -> (int * values) array
 
-(** Evaluation *)
-
-val whd_stack : values -> stack -> whd
-val force_whd : values -> stack -> whd
-
-val eta_whd : int -> whd -> values
+(** Apply a value *)
 
+val apply_whd : int -> whd -> values