Merge branch 'v8.5'

33 files changed, 889 insertions, 359 deletions

diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 0553a5ed7..dc571699e 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -341,6 +341,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(ENVACC){
 	print_instr("ENVACC");
+	print_int(*pc);
 	accu = Field(coq_env, *pc++);
         Next;
       }
@@ -371,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;
@@ -458,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;
@@ -481,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]);
@@ -585,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;
       }
@@ -720,6 +736,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(GETGLOBAL){
 	print_instr("GETGLOBAL");
+	print_int(*pc);
 	accu = Field(coq_global_data, *pc);
         pc++;
         Next;
@@ -732,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++;
@@ -743,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;
@@ -753,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];
@@ -764,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];
@@ -776,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];
@@ -940,6 +961,7 @@ value coq_interprete
       /* Fallthrough */
       Instruct(CONSTINT) {
 	print_instr("CONSTINT");
+	print_int(*pc);
 	accu = Val_int(*pc);
 	pc++;
 	Next;
diff --git a/kernel/byterun/coq_values.h b/kernel/byterun/coq_values.h
index 80100da71..bb0f0eb5e 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_INDUCTIVE_TAG 1
-#define ATOM_PROJ_TAG 2
-#define ATOM_FIX_TAG 3
-#define ATOM_SWITCH_TAG 4
-#define ATOM_COFIX_TAG 5
-#define ATOM_COFIXEVALUATED_TAG 6
-
-
+#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 448bf8544..0a24a75d6 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -19,13 +19,13 @@ type tag = int
 
 let accu_tag = 0
 
-let max_atom_tag = 1
-let proj_tag = 2
-let fix_app_tag = 3
-let switch_tag = 4
-let cofix_tag = 5
-let cofix_evaluated_tag = 6
-
+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 *)
@@ -33,10 +33,12 @@ 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
 
@@ -71,7 +73,8 @@ type instruction =
   | Kclosure of Label.t * int
   | Kclosurerec of int * int * Label.t array * Label.t array
   | Kclosurecofix of int * int * Label.t array * Label.t array
-  | Kgetglobal of pconstant
+                   (* nb fv, init, lbl types, lbl bodies *)
+  | Kgetglobal of constant
   | Kconst of structured_constant
   | Kmakeblock of int * tag
   | Kmakeprod
@@ -127,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
 
@@ -145,18 +151,17 @@ 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
@@ -169,14 +174,24 @@ let pp_sort s =
 
 let rec pp_struct_const = function
   | Const_sorts s -> pp_sort s
-  | Const_ind ((mind, i), u) -> pr_mind mind ++ str"#" ++ int i
+  | 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
@@ -210,8 +225,7 @@ let rec pp_instr i =
 	     prlist_with_sep spc pp_lbl (Array.to_list lblt) ++
 	     str " bodies = " ++
 	     prlist_with_sep spc pp_lbl (Array.to_list lblb))
-  | Kgetglobal (id,u) ->
-    str "getglobal " ++ pr_con id ++ str "@{" ++ Univ.Instance.pr Univ.Level.pr u ++ str "}"
+  | Kgetglobal idu -> str "getglobal " ++ pr_con idu
   | Kconst sc ->
       str "const " ++ pp_struct_const sc
   | Kmakeblock(n, m) ->
@@ -269,10 +283,6 @@ and pp_bytecodes c =
   | i :: c ->
       tab () ++ pp_instr i ++ fnl () ++ pp_bytecodes c
 
-let dump_bytecode c =
-  pperrnl (pp_bytecodes c);
-  flush_all()
-
 (*spiwack: moved this type in this file  because I needed it for
   retroknowledge which can't depend from cbytegen *)
 type block =
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 03d638305..03ae6b9cd 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -15,6 +15,7 @@ type tag = int
 
 val accu_tag : tag
 
+val type_atom_tag : tag
 val max_atom_tag : tag
 val proj_tag : tag
 val fix_app_tag : tag
@@ -22,14 +23,18 @@ 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
 
@@ -64,9 +69,11 @@ 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             (** accu = coq_global_data[c] *)
+  | Kgetglobal of constant
   | Kconst of structured_constant
-  | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block *)
+  | 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 *)
@@ -120,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
 
@@ -129,26 +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_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 *)
-                                 (** recursives =  nbr                      *)
+                                 (** (= 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 dump_bytecode : 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 3462694d6..1f7cc3c7a 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,18 +547,17 @@ let rec compile_fv reloc l sz cont =
 
 (* Compiling constants *)
 
-let rec get_alias 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
-	| BCalias (kn',u') -> get_alias 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"
@@ -552,9 +574,44 @@ let rec 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 ::
@@ -663,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
@@ -745,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
@@ -756,31 +827,84 @@ and compile_const =
                   (mkConstU (kn,u)) reloc args sz cont
   with Not_found ->
     if Int.equal nargs 0 then
-      Kgetglobal (get_alias !global_env (kn, u)) :: cont
+      compile_get_global reloc (kn,u) sz cont
     else
-      comp_app (fun _ _ _ cont ->
-                   Kgetglobal (get_alias !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 fv = List.rev (!(reloc.in_env).fv_rev) in
-    let pp_v v =
-      match v with
-      | FVnamed id -> Pp.str (Id.to_string id)
-      | FVrel i -> Pp.str (string_of_int i)
+  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 open Pp in
-    if !Flags.dump_bytecode then
-      (dump_bytecode init_code;
-       dump_bytecode !fun_code;
-       Pp.msg_debug (Pp.str "fv = " ++
-	 Pp.prlist_with_sep (fun () -> Pp.str "; ") pp_v fv ++ Pp.fnl ()));
+    let fv = List.rev (!(reloc.in_env).fv_rev) in
+    (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
@@ -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 (BCalias (get_alias 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) = BCalias (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
@@ -902,14 +1031,14 @@ let op2_compilation op =
   3/ if at least one is not, branches to the normal behavior:
       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_alias !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_alias !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 1128f0d0b..c0f48641c 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 4e64ed697..5ba93eda0 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
 
@@ -135,11 +135,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
 
@@ -198,7 +198,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)
@@ -315,10 +315,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
@@ -327,7 +327,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
@@ -336,12 +336,12 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
 
 type body_code =
   | BCdefined of to_patch
-  | BCalias of pconstant
+  | BCalias of Names.constant
   | BCconstant
 
 type to_patch_substituted =
 | PBCdefined of to_patch substituted
-| PBCalias of pconstant substituted
+| PBCalias of Names.constant substituted
 | PBCconstant
 
 let from_val = function
@@ -351,7 +351,7 @@ let from_val = function
 
 let force = function
 | PBCdefined tp -> BCdefined (force subst_to_patch tp)
-| PBCalias cu -> BCalias (force subst_pconstant cu)
+| PBCalias cu -> BCalias (force subst_constant cu)
 | PBCconstant -> BCconstant
 
 let subst_to_patch_subst s = function
@@ -383,8 +383,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 398b60eca..c80edd596 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
 
@@ -23,7 +23,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
 
 type body_code =
   | BCdefined of to_patch
-  | BCalias of constant Univ.puniverses
+  | BCalias of constant
   | BCconstant
 
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index e242449b1..aa9ef66fe 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -58,7 +58,7 @@ 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_sorts _, _ -> false
-| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2
+| 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
@@ -67,18 +67,24 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with
 | Const_bn (t1, a1), Const_bn (t2, a2) ->
   Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2
 | 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_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 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
@@ -124,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
 
@@ -148,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))
+           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,u)) in
+	 | BCconstant -> set_global (val_of_constant kn)
+    in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
     rk := Some (Ephemeron.create pos);
     pos
@@ -197,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) =
   let patch = function
@@ -208,7 +215,6 @@ and eval_to_patch env (buff,pl,fv) =
   let buff = patch_int buff patches in
   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 +232,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 7def963e7..dc5c17a75 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -79,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 =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index a7051d5c1..248504c1b 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 ce65af975..1b8700958 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 303d27d35..e058519e9 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.mli b/kernel/environ.mli
index 714c26066..2eab32e72 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -250,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/mod_typing.ml b/kernel/mod_typing.ml
index d4b381264..3c58e788c 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -126,11 +126,17 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
 	      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 univs =
+        if cb.const_polymorphic then Some cb.const_universes
+        else None
+      in
       let cb' =
 	{ cb with
 	  const_body = def;
-	  const_universes = univs;
-	  const_body_code = Option.map Cemitcodes.from_val (compile_constant_body env' def) }
+          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
diff --git a/kernel/modops.ml b/kernel/modops.ml
index f0cb65c96..cbb796331 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -335,7 +335,7 @@ let strengthen_const mp_from l cb resolver =
     in
       { cb with
 	const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
-	const_body_code = 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/nativeconv.ml b/kernel/nativeconv.ml
index 7ae66c485..0242fd461 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -63,10 +63,12 @@ and conv_atom env pb lvl a1 a2 cu =
     | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false
     | Arel i1, Arel i2 -> 
 	if Int.equal i1 i2 then cu else raise NotConvertible
-    | Aind ind1, Aind ind2 ->
-	if eq_puniverses eq_ind ind1 ind2 then cu else raise NotConvertible
-    | Aconstant c1, Aconstant c2 ->
-	if eq_puniverses eq_constant c1 c2 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 -> 
         sort_cmp_universes env pb s1 s2 cu
     | Avar id1, Avar id2 ->
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 263befd21..4d033bc99 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -379,7 +379,7 @@ let rec get_alias env (kn, u as p) =
     | None -> p
     | Some tps ->
        match Cemitcodes.force tps with
-       | Cemitcodes.BCalias kn' -> get_alias env kn'
+       | Cemitcodes.BCalias kn' -> get_alias env (kn', u)
        | _ -> p
 
 (*i Global environment *)
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index e4a779993..40bef4bc6 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 9f4361f40..badb15b56 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/reduction.ml b/kernel/reduction.ml
index e081870ba..c5595bbc3 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -171,7 +171,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
@@ -183,8 +183,10 @@ type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constrai
 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
@@ -194,7 +196,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
@@ -585,7 +587,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 UGraph.check_eq_instances univs u u' then univs
   else raise NotConvertible
 
@@ -625,7 +627,7 @@ 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 inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 0bb855c67..ef764f34f 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -37,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;
   } 
 
@@ -50,6 +50,11 @@ type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constrai
 val sort_cmp_universes : env -> conv_pb -> sorts -> sorts ->
   'a * 'a universe_compare -> 'a * 'a universe_compare
 
+(* [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 checked_universes : UGraph.t universe_compare
 val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ec245b064..b71cd31b5 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -207,15 +207,55 @@ 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.handle_side_effects
+let inline_private_constants_in_definition_entry = Term_typing.handle_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 _ -> acc)
+   [] eff
 
 let env_of_safe_env senv = senv.env
 let env_of_senv = env_of_safe_env
@@ -337,7 +377,7 @@ 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 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
@@ -442,19 +482,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 =
@@ -471,7 +508,33 @@ 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.validate_side_effects_for_export
+            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 *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index eac08eb83..2214cf8bb 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
 
@@ -63,16 +83,23 @@ val push_named_assum :
 (** Returns the full universe context necessary to typecheck the definition
   (futures are forced) *)
 val push_named_def :
-  Id.t * Entries.definition_entry -> Univ.universe_context_set safe_transformer
+  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 *)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index b6df8f454..d75bd73fb 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 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 "tological" order between effects we have to uniqize from the
+ * tail *)
+let uniq_seff l = List.rev (uniq_seff (List.rev l))
 
 let handle_side_effects env body ctx side_eff =
-  let handle_sideff (t,ctx) se =
+  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,7 +84,7 @@ let handle_side_effects env body ctx 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
+      | _ -> 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, _ ->
@@ -87,17 +106,60 @@ let handle_side_effects env body ctx side_eff =
               let t = sub c 1 (Vars.lift 1 t) in
 	        mkApp (mkLambda (cname c, b_ty, t), [|b|]),
 		Univ.ContextSet.union ctx
-		  (Univ.ContextSet.of_context cb.const_universes)		
+		  (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), ctx
       | _ -> assert false
     in
-      List.fold_right fix_body cbl (t,ctx)
+    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,ctx)
-    (Declareops.uniquize_side_effects side_eff)
+  List.fold_left handle_sideff (body,ctx,[]) (uniq_seff side_eff)
+
+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 trust_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} 
@@ -105,7 +167,7 @@ let hcons_j j =
 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 ~strict:(not poly) uctx env in
@@ -124,9 +186,14 @@ let infer_declaration env kn dcl =
       let tyj = infer_type env typ in
       let proofterm =
         Future.chain ~greedy:true ~pure:true body (fun ((body, ctx),side_eff) ->
-          let body,ctx = handle_side_effects env body ctx side_eff in
+          let body, ctx, signatures =
+            handle_side_effects env body ctx side_eff in
+          let trusted_signatures = check_signatures trust signatures in
 	  let env' = push_context_set ctx env in
-          let j = infer env' body in
+          let j =
+            let body, env', zip_ctx = trust_seff trusted_signatures body env' in
+            let j = infer env' body in
+            unzip zip_ctx 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
@@ -143,7 +210,7 @@ let infer_declaration env kn dcl =
       let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
       let (body, ctx), side_eff = Future.join body in
       let univsctx = Univ.ContextSet.of_context c.const_entry_universes in
-      let body, ctx = handle_side_effects env body
+      let body, ctx, _ = handle_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
@@ -258,33 +325,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 ->
+    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 def
-      in Option.map Cemitcodes.from_val res
+	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;
@@ -297,8 +361,93 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
 
 (*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 Entries.constant_entry * side_effect_role
+
+let validate_side_effects_for_export 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
@@ -308,9 +457,9 @@ 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
@@ -335,9 +484,9 @@ let translate_mind env kn mie = Indtypes.check_inductive env kn mie
 let handle_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) ->
-			 let body, ctx' = handle_side_effects env body ctx side_eff in
-			 (body, ctx'), Declareops.no_seff);
+      let body, ctx',_ = handle_side_effects env body ctx side_eff in
+      (body, ctx'), []);
 }
 
 let handle_side_effects env body side_eff =
-  fst (handle_side_effects env body Univ.ContextSet.empty side_eff)
+  pi1 (handle_side_effects env body Univ.ContextSet.empty side_eff)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 8d92bcc68..509160ccc 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -12,23 +12,42 @@ 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 handle_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
+val handle_entry_side_effects : env -> side_effects definition_entry -> side_effects definition_entry
 (** Same as {!handle_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
+
+(* Checks weather the side effects in constant_entry can be trusted.
+ * Returns the list of effects to be exported.
+ * Note: It forces the Future.computation.                           *)
+type side_effect_role =
+  | Subproof
+  | Schema of inductive * string
+
+type exported_side_effect = 
+  constant * constant_body * side_effects Entries.constant_entry * side_effect_role
+  
+val validate_side_effects_for_export :
+  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,8 +56,8 @@ 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
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8201980e3..b303a1a5a 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -977,7 +977,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
@@ -1001,8 +1001,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
diff --git a/kernel/univ.mli b/kernel/univ.mli
index ae7400337..5682940a0 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -308,6 +308,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
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 88c1e1038..a800e2531 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 fdd4603b5..c0fbeeb6e 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 2f6be0601..4610dbcb0 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -45,8 +45,15 @@ let rec conv_val env pb k v1 v2 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 -> 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
@@ -81,26 +88,46 @@ and conv_whd env pb k whd1 whd2 cu =
 
 
 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
+  | 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
@@ -144,25 +171,18 @@ 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 vm_conv_gen cv_pb env univs t1 t2 =
   try 
     let v1 = val_of_constr env t1 in
diff --git a/kernel/vm.ml b/kernel/vm.ml
index eacd803fd..64ddc4376 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -121,12 +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|proj name] : a projection blocked by an accu            *)
-(*     -- 4_[accu|fix_app] : a fixpoint blocked by an accu                *)
-(*     -- 5_[accu|vswitch] : a match blocked by an accu                   *)
-(*     -- 6_[fcofix]       : a cofix function                             *)
-(*     -- 7_[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]                                      *)
@@ -136,7 +136,8 @@ type vswitch = {
 
 type atom =
   | Aid of Vars.id_key
-  | Aind of pinductive
+  | Aind of inductive
+  | Atype of Univ.universe
 
 (* Zippers *)
 
@@ -159,17 +160,98 @@ 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 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)
   | i when Int.equal i proj_tag ->
@@ -199,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"
 
@@ -212,67 +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))
-
-(* 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
+	else
+           Vconstr_block(Obj.obj o)
 
 (**********************************************)
 (* Constructors *******************************)
@@ -299,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)
 
@@ -317,11 +355,11 @@ let val_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
@@ -606,3 +644,34 @@ let apply_whd k whd =
       interprete (fun_code to_up) (Obj.magic to_up) (Obj.magic to_up) 0
   | Vatom_stk(a,stk) ->
       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 045d02333..43a42eb9c 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -22,7 +22,8 @@ type arguments
 
 type atom =
   | Aid of Vars.id_key
-  | Aind of pinductive
+  | Aind of inductive
+  | Atype of Univ.universe
 
 (** Zippers *)
 
@@ -45,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 *)