31 files changed, 165 insertions, 224 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index 704eb1ef98..27287205f4 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -230,6 +230,12 @@ if (sp - num_args < coq_stack_threshold) {                                     \
     *sp = swap_accu_sp_tmp__;                   \
   }while(0)
 
+/* Turn a code pointer into a stack value usable as a return address, and conversely.
+   The least significant bit is set to 1 so that the GC does not mistake return
+   addresses for heap pointers. */
+#define StoreRA(p) ((value)(p) + 1)
+#define LoadRA(p) ((code_t)((value)(p) - 1))
+
 #if OCAML_VERSION < 41000
 /* For signal handling, we hijack some code from the caml runtime */
 
@@ -445,7 +451,7 @@ value coq_interprete
       Instruct(PUSH_RETADDR) {
         print_instr("PUSH_RETADDR");
         sp -= 3;
-        sp[0] = (value) (pc + *pc);
+        sp[0] = StoreRA(pc + *pc);
         sp[1] = coq_env;
         sp[2] = Val_long(coq_extra_args);
         coq_extra_args = 0;
@@ -466,7 +472,7 @@ value coq_interprete
         arg1 = sp[0];
         sp -= 3;
         sp[0] = arg1;
-        sp[1] = (value)pc;
+        sp[1] = StoreRA(pc);
         sp[2] = coq_env;
         sp[3] = Val_long(coq_extra_args);
         print_instr("call stack=");
@@ -489,7 +495,7 @@ value coq_interprete
         sp -= 3;
         sp[0] = arg1;
         sp[1] = arg2;
-        sp[2] = (value)pc;
+        sp[2] = StoreRA(pc);
         sp[3] = coq_env;
         sp[4] = Val_long(coq_extra_args);
         pc = Code_val(accu);
@@ -511,7 +517,7 @@ value coq_interprete
         sp[0] = arg1;
         sp[1] = arg2;
         sp[2] = arg3;
-        sp[3] = (value)pc;
+        sp[3] = StoreRA(pc);
         sp[4] = coq_env;
         sp[5] = Val_long(coq_extra_args);
         pc = Code_val(accu);
@@ -531,7 +537,7 @@ value coq_interprete
         sp[1] = arg2;
         sp[2] = arg3;
         sp[3] = arg4;
-        sp[4] = (value)pc;
+        sp[4] = StoreRA(pc);
         sp[5] = coq_env;
         sp[6] = Val_long(coq_extra_args);
         pc = Code_val(accu);
@@ -647,7 +653,7 @@ value coq_interprete
           coq_env = accu;
         } else {
           print_instr("extra args = 0");
-          pc = (code_t)(sp[0]);
+          pc = LoadRA(sp[0]);
           coq_env = sp[1];
           coq_extra_args = Long_val(sp[2]);
           sp += 3;
@@ -682,7 +688,7 @@ value coq_interprete
           for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i];
           Code_val(accu) = pc - 3; /* Point to the preceding RESTART instr. */
           sp += num_args;
-          pc = (code_t)(sp[0]);
+          pc = LoadRA(sp[0]);
           coq_env = sp[1];
           coq_extra_args = Long_val(sp[2]);
           sp += 3;
@@ -707,7 +713,7 @@ value coq_interprete
             Field(accu, 2) = coq_env;
             for (i = 0; i < num_args; i++) Field(accu, i + 3) = sp[i];
             sp += num_args;
-            pc = (code_t)(sp[0]);
+            pc = LoadRA(sp[0]);
             coq_env = sp[1];
             coq_extra_args = Long_val(sp[2]);
             sp += 3;
@@ -745,7 +751,7 @@ value coq_interprete
             Code_val(block) = accumulate;
             Field(block, 1) = Val_int(2);
             accu = block;
-            pc = (code_t)(sp[0]);
+            pc = LoadRA(sp[0]);
             coq_env = sp[1];
             coq_extra_args = Long_val(sp[2]);
             sp += 3;
@@ -1031,7 +1037,7 @@ value coq_interprete
               mlsize_t i, nargs;
               sp -= 2;
               // Push the current instruction as the return address
-              sp[0] = (value)(pc - 1);
+              sp[0] = StoreRA(pc - 1);
               sp[1] = coq_env;
               coq_env = Field(accu, 0); // Pointer to suspension
               accu = sp[2]; // Save accumulator to accu register
@@ -1142,7 +1148,7 @@ value coq_interprete
           for (i = size; i < sz; ++i)
             caml_initialize(&Field(accu, i), *sp++);
         }
-        pc = (code_t)(sp[0]);
+        pc = LoadRA(sp[0]);
         coq_env = sp[1];
         coq_extra_args = Long_val(sp[2]);
         sp += 3;
@@ -1160,7 +1166,7 @@ value coq_interprete
             sp-=2;
             pc++;
             // Push the return address
-            sp[0] = (value) (pc + *pc);
+            sp[0] = StoreRA(pc + *pc);
             sp[1] = coq_env;
             coq_env = Field(accu,0); // Pointer to suspension
             accu = sp[2]; // Save accumulator to accu register
@@ -1263,7 +1269,7 @@ value coq_interprete
         }
         Code_val(accu) = accumulate;
         Field(accu, 1) = Val_int(2);
-        pc = (code_t)(sp[0]);
+        pc = LoadRA(sp[0]);
         coq_env = sp[1];
         coq_extra_args = Long_val(sp[2]);
         sp += 3;
@@ -1916,7 +1922,7 @@ value coq_push_ra(value code) {
   code_t tcode = Code_val(code);
   print_instr("push_ra");
   coq_sp -= 3;
-  coq_sp[0] = (value) tcode;
+  coq_sp[0] = StoreRA(tcode);
   coq_sp[1] = Val_unit;
   coq_sp[2] = Val_long(0);
   return Val_unit;
diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c
index a55ff57c8d..f404cb2b1c 100644
--- a/kernel/byterun/coq_memory.c
+++ b/kernel/byterun/coq_memory.c
@@ -66,10 +66,6 @@ static void coq_scan_roots(scanning_action action)
   /* Scan the stack */
   for (i = coq_sp; i < coq_stack_high; i++) {
     if (!Is_block(*i)) continue;
-#ifdef NO_NAKED_POINTERS
-    /* The VM stack may contain C-allocated bytecode */
-    if (!Is_in_heap_or_young(*i)) continue;
-#endif
     (*action) (*i, i);
   };
   /* Hook */
diff --git a/kernel/byterun/dune b/kernel/byterun/dune
index b14ad5c558..4d2000bb52 100644
--- a/kernel/byterun/dune
+++ b/kernel/byterun/dune
@@ -1,5 +1,5 @@
 (library
- (name byterun)
+ (name coqrun)
  (synopsis "Coq's Kernel Abstract Reduction Machine [C implementation]")
  (public_name coq-core.vm)
  (foreign_stubs
diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml
index 6ef0e9fa15..9e0f574fa3 100644
--- a/kernel/cPrimitives.ml
+++ b/kernel/cPrimitives.ml
@@ -295,38 +295,57 @@ let types =
         PITT_param 1))
   in
   function
-  | Int63head0 | Int63tail0 -> [int_ty; int_ty]
+  | Int63head0 | Int63tail0 ->
+      [int_ty], int_ty
   | Int63add | Int63sub | Int63mul
   | Int63div | Int63mod
   | Int63divs | Int63mods
   | Int63lsr | Int63lsl | Int63asr
-  | Int63land | Int63lor | Int63lxor -> [int_ty; int_ty; int_ty]
+  | Int63land | Int63lor | Int63lxor ->
+      [int_ty; int_ty], int_ty
   | Int63addc | Int63subc | Int63addCarryC | Int63subCarryC ->
-     [int_ty; int_ty; PITT_ind (PIT_carry, int_ty)]
+      [int_ty; int_ty], PITT_ind (PIT_carry, int_ty)
   | Int63mulc | Int63diveucl ->
-     [int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
-  | Int63eq | Int63lt | Int63le | Int63lts | Int63les -> [int_ty; int_ty; PITT_ind (PIT_bool, ())]
-  | Int63compare | Int63compares -> [int_ty; int_ty; PITT_ind (PIT_cmp, ())]
+      [int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty))
+  | Int63eq | Int63lt | Int63le | Int63lts | Int63les ->
+      [int_ty; int_ty], PITT_ind (PIT_bool, ())
+  | Int63compare | Int63compares ->
+      [int_ty; int_ty], PITT_ind (PIT_cmp, ())
   | Int63div21 ->
-     [int_ty; int_ty; int_ty; PITT_ind (PIT_pair, (int_ty, int_ty))]
-  | Int63addMulDiv -> [int_ty; int_ty; int_ty; int_ty]
+      [int_ty; int_ty; int_ty], PITT_ind (PIT_pair, (int_ty, int_ty))
+  | Int63addMulDiv ->
+      [int_ty; int_ty; int_ty], int_ty
   | Float64opp | Float64abs | Float64sqrt
-  | Float64next_up | Float64next_down -> [float_ty; float_ty]
-  | Float64ofInt63 -> [int_ty; float_ty]
-  | Float64normfr_mantissa -> [float_ty; int_ty]
-  | Float64frshiftexp -> [float_ty; PITT_ind (PIT_pair, (float_ty, int_ty))]
-  | Float64eq | Float64lt | Float64le -> [float_ty; float_ty; PITT_ind (PIT_bool, ())]
-  | Float64compare -> [float_ty; float_ty; PITT_ind (PIT_f_cmp, ())]
-  | Float64classify -> [float_ty; PITT_ind (PIT_f_class, ())]
-  | Float64add | Float64sub | Float64mul
-  | Float64div -> [float_ty; float_ty; float_ty]
-  | Float64ldshiftexp -> [float_ty; int_ty; float_ty]
-  | Arraymake -> [int_ty; PITT_param 1; array_ty]
-  | Arrayget -> [array_ty; int_ty; PITT_param 1]
-  | Arraydefault -> [array_ty; PITT_param 1]
-  | Arrayset -> [array_ty; int_ty; PITT_param 1; array_ty]
-  | Arraycopy -> [array_ty; array_ty]
-  | Arraylength -> [array_ty; int_ty]
+  | Float64next_up | Float64next_down ->
+      [float_ty], float_ty
+  | Float64ofInt63 ->
+      [int_ty], float_ty
+  | Float64normfr_mantissa ->
+      [float_ty], int_ty
+  | Float64frshiftexp ->
+      [float_ty], PITT_ind (PIT_pair, (float_ty, int_ty))
+  | Float64eq | Float64lt | Float64le ->
+      [float_ty; float_ty], PITT_ind (PIT_bool, ())
+  | Float64compare ->
+      [float_ty; float_ty], PITT_ind (PIT_f_cmp, ())
+  | Float64classify ->
+      [float_ty], PITT_ind (PIT_f_class, ())
+  | Float64add | Float64sub | Float64mul | Float64div ->
+      [float_ty; float_ty], float_ty
+  | Float64ldshiftexp ->
+      [float_ty; int_ty], float_ty
+  | Arraymake ->
+      [int_ty; PITT_param 1], array_ty
+  | Arrayget ->
+      [array_ty; int_ty], PITT_param 1
+  | Arraydefault ->
+      [array_ty], PITT_param 1
+  | Arrayset ->
+      [array_ty; int_ty; PITT_param 1], array_ty
+  | Arraycopy ->
+      [array_ty], array_ty
+  | Arraylength ->
+      [array_ty], int_ty
 
 let one_param =
   (* currently if there's a parameter it's always this *)
@@ -460,14 +479,17 @@ type args_red = arg_kind list
 (* Invariant only argument of type int63, float or an inductive can
    have kind Kwhnf *)
 
-let arity t = let sign = types t in nparams t + List.length sign - 1
+let arity t =
+  nparams t + List.length (fst (types t))
 
 let kind t =
   let rec params n = if n <= 0 then [] else Kparam :: params (n - 1) in
   let args = function PITT_type _ | PITT_ind _ -> Kwhnf | PITT_param _ -> Karg in
-  params (nparams t) @ List.map args (CList.drop_last (types t))
+  params (nparams t) @ List.map args (fst (types t))
 
-let types t = params t, types t
+let types t =
+  let args_ty, ret_ty = types t in
+  params t, args_ty, ret_ty
 
 (** Special Entries for Register **)
 
diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli
index de90179726..6661851d53 100644
--- a/kernel/cPrimitives.mli
+++ b/kernel/cPrimitives.mli
@@ -140,8 +140,8 @@ val parse_op_or_type : ?loc:Loc.t -> string -> op_or_type
 
 val univs : t -> Univ.AUContext.t
 
-val types : t -> Constr.rel_context * ind_or_type list
-(** Parameters * Reduction relevant arguments and output type
+val types : t -> Constr.rel_context * ind_or_type list * ind_or_type
+(** Parameters * Reduction relevant arguments * output type
 
   XXX we could reify universes in ind_or_type (currently polymorphic types
   like array are assumed to use universe 0). *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f82b754c59..87b1a71c9d 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -252,9 +252,6 @@ let cook_constant { from = cb; info } =
     cook_context = Some const_hyps;
   }
 
-(* let cook_constant_key = CProfile.declare_profile "cook_constant" *)
-(* let cook_constant = CProfile.profile2 cook_constant_key cook_constant *)
-
 (********************************)
 (* Discharging mutual inductive *)
 
diff --git a/kernel/dune b/kernel/dune
index 0bf51f80ec..af88e9864f 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -4,7 +4,7 @@
  (public_name coq-core.kernel)
  (wrapped false)
  (modules (:standard \ genOpcodeFiles uint63_31 uint63_63 float64_31 float64_63))
- (libraries lib byterun dynlink))
+ (libraries lib coqrun dynlink))
 
 (executable
   (name genOpcodeFiles)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index eb18d4b90e..ddbd5fa0a7 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -717,7 +717,7 @@ let rec ienv_decompose_prod (env,_ as ienv) n c =
      ienv_decompose_prod ienv' (n-1) b
      | _ -> assert false
 
-let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0))
+let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) "" 0))
 let dummy_implicit_sort = mkType (Universe.make dummy_univ)
 let lambda_implicit_lift n a =
   let anon = Context.make_annot Anonymous Sorts.Relevant in
@@ -1334,11 +1334,6 @@ let check_fix env ((nvect,_),(names,_,bodies as recdef) as fix) =
   else
     ()
 
-(*
-let cfkey = CProfile.declare_profile "check_fix";;
-let check_fix env fix = CProfile.profile3 cfkey check_fix env fix;;
-*)
-
 (************************************************************************)
 (* Co-fixpoints. *)
 
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index c5ac57a2cd..d2fb773dc4 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -291,6 +291,11 @@ let subst_ind sub (ind,i as indi) =
   let ind' = subst_mind sub ind in
     if ind' == ind then indi else ind',i
 
+let subst_constructor subst (ind,j as ref) =
+  let ind' = subst_ind subst ind in
+  if ind==ind' then ref
+  else (ind',j)
+
 let subst_pind sub (ind,u) =
   (subst_ind sub ind, u)
 
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 9cf270cff7..e7bfceb4de 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -127,6 +127,9 @@ val subst_mind :
 val subst_ind :
   substitution -> inductive -> inductive
 
+val subst_constructor :
+  substitution -> constructor -> constructor
+
 val subst_pind : substitution -> pinductive -> pinductive
 
 val subst_kn :
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index d517d215ed..22bbcb8a65 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -994,9 +994,8 @@ let extract_prim ml_of l =
   let decl = ref [] in
   let cond = ref [] in
   let type_args p =
-    let rec aux = function [] | [_] -> [] | h :: t -> h :: aux t in
-    let params, sign = CPrimitives.types p in
-    List.length params, Array.of_list (aux sign) in
+    let params, args_ty, _ = CPrimitives.types p in
+    List.length params, Array.of_list args_ty in
   let rec aux l =
     match l with
     | Lprim(prefix,kn,p,args) ->
@@ -2130,7 +2129,7 @@ let compile_deps env sigma prefix init t =
   in
   aux env 0 init t
 
-let compile_constant_field env _prefix con acc cb =
+let compile_constant_field env con acc cb =
     let gl = compile_constant env empty_evars con cb in
     gl@acc
 
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index 90525a19b2..17312ec8ea 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -65,7 +65,7 @@ val register_native_file : string -> unit
 
 val is_loaded_native_file : string -> bool
 
-val compile_constant_field : env -> string -> Constant.t ->
+val compile_constant_field : env -> Constant.t ->
   global list -> 'a constant_body -> global list
 
 val compile_mind_field : ModPath.t -> Label.t ->
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index f3b483467d..aa30a01134 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -381,10 +381,7 @@ let makeblock env ind tag nparams arity args =
     Lmakeblock(prefix, ind, tag, args)
 
 let makearray args def =
-  try
-    let p = Array.map get_value args in
-    Lval (Nativevalues.parray_of_array p (get_value def))
-  with Not_found -> Lparray (args, def)
+  Lparray (args, def)
 
 (* Translation of constants *)
 
diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml
index 2e27fe071e..6dd7f315e0 100644
--- a/kernel/nativelibrary.ml
+++ b/kernel/nativelibrary.ml
@@ -17,21 +17,21 @@ open Nativecode
 (** This file implements separate compilation for libraries in the native
 compiler *)
 
-let rec translate_mod prefix mp env mod_expr acc =
+let rec translate_mod mp env mod_expr acc =
   match mod_expr with
   | NoFunctor struc ->
       let env' = add_structure mp struc empty_delta_resolver env in
-      List.fold_left (translate_field prefix mp env') acc struc
+      List.fold_left (translate_field mp env') acc struc
   | MoreFunctor _ -> acc
 
-and translate_field prefix mp env acc (l,x) =
+and translate_field mp env acc (l,x) =
   match x with
   | SFBconst cb ->
      let con = Constant.make2 mp l in
      (debug_native_compiler (fun () ->
         let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in
         Pp.str msg));
-     compile_constant_field env prefix con acc cb
+     compile_constant_field env con acc cb
   | SFBmind mb ->
      (debug_native_compiler (fun () ->
         let id = mb.mind_packets.(0).mind_typename in
@@ -45,7 +45,7 @@ and translate_field prefix mp env acc (l,x) =
           Printf.sprintf "Compiling module %s..." (ModPath.to_string mp)
         in
         Pp.str msg));
-     translate_mod prefix mp env md.mod_type acc
+     translate_mod mp env md.mod_type acc
   | SFBmodtype mdtyp ->
      let mp = mdtyp.mod_mp in
      (debug_native_compiler (fun () ->
@@ -53,19 +53,18 @@ and translate_field prefix mp env acc (l,x) =
           Printf.sprintf "Compiling module type %s..." (ModPath.to_string mp)
         in
         Pp.str msg));
-     translate_mod prefix mp env mdtyp.mod_type acc
+     translate_mod mp env mdtyp.mod_type acc
 
-let dump_library mp dp env mod_expr =
+let dump_library mp env mod_expr =
   debug_native_compiler (fun () -> Pp.str "Compiling library...");
   match mod_expr with
   | NoFunctor struc ->
       let env = add_structure mp struc empty_delta_resolver env in
-      let prefix = mod_uid_of_dirpath dp ^ "." in
       let t0 = Sys.time () in
       clear_global_tbl ();
       clear_symbols ();
       let mlcode =
-        List.fold_left (translate_field prefix mp env) [] struc
+        List.fold_left (translate_field mp env) [] struc
       in
       let t1 = Sys.time () in
       let time_info = Format.sprintf "Time spent generating this code: %.5fs" (t1-.t0) in
diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli
index 8f58dfa8d3..1d0d56703d 100644
--- a/kernel/nativelibrary.mli
+++ b/kernel/nativelibrary.mli
@@ -15,5 +15,5 @@ open Nativecode
 (** This file implements separate compilation for libraries in the native
 compiler *)
 
-val dump_library : ModPath.t -> DirPath.t -> env -> module_signature ->
+val dump_library : ModPath.t -> env -> module_signature ->
   global list * Nativevalues.symbols
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 1e39756d47..18c3a3ec9c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -964,7 +964,8 @@ let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
     compare_instances = infer_convert_instances;
     compare_cumul_instances = infer_inductive_instances; }
 
-let gen_conv cv_pb l2r reds env evars univs t1 t2 =
+let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _ -> None)) t1 t2 =
+  let univs = Environ.universes env in
   let b =
     if cv_pb = CUMUL then leq_constr_univs univs t1 t2
     else eq_constr_univs univs t1 t2
@@ -974,16 +975,7 @@ let gen_conv cv_pb l2r reds env evars univs t1 t2 =
       let _ = clos_gen_conv reds cv_pb l2r evars env univs (univs, checked_universes) t1 t2 in
         ()
 
-(* Profiling *)
-let gen_conv cv_pb ?(l2r=false) ?(reds=TransparentState.full) env ?(evars=(fun _->None)) =
-  let univs = Environ.universes env in
-  if Flags.profile then
-    let fconv_universes_key = CProfile.declare_profile "trans_fconv_universes" in
-      CProfile.profile8 fconv_universes_key gen_conv cv_pb l2r reds env evars univs
-  else gen_conv cv_pb l2r reds env evars univs
-
 let conv = gen_conv CONV
-
 let conv_leq = gen_conv CUMUL
 
 let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
@@ -992,7 +984,7 @@ let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
     clos_gen_conv reds cv_pb l2r evars env graph univs t1 t2
   in s
 
-let infer_conv_universes cv_pb l2r evars reds env t1 t2 =
+let infer_conv_universes cv_pb ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full) env t1 t2 =
   let univs = Environ.universes env in
   let b, cstrs =
     if cv_pb == CUMUL then Constr.leq_constr_univs_infer univs t1 t2
@@ -1001,37 +993,16 @@ let infer_conv_universes cv_pb l2r evars reds env t1 t2 =
     if b then cstrs
     else
       let state = ((univs, Univ.Constraint.empty), inferred_universes) in
-      let ((_,cstrs), _) = clos_gen_conv reds cv_pb l2r evars env univs state t1 t2 in
+      let ((_,cstrs), _) = clos_gen_conv ts cv_pb l2r evars env univs state t1 t2 in
         cstrs
 
-(* Profiling *)
-let infer_conv_universes =
-  if Flags.profile then
-    let infer_conv_universes_key = CProfile.declare_profile "infer_conv_universes" in
-      CProfile.profile7 infer_conv_universes_key infer_conv_universes
-  else infer_conv_universes
-
-let infer_conv ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
-    env t1 t2 =
-  infer_conv_universes CONV l2r evars ts env t1 t2
-
-let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=TransparentState.full)
-    env t1 t2 =
-  infer_conv_universes CUMUL l2r evars ts env t1 t2
+let infer_conv = infer_conv_universes CONV
+let infer_conv_leq = infer_conv_universes CUMUL
 
 let default_conv cv_pb ?l2r:_ env t1 t2 =
     gen_conv cv_pb env t1 t2
 
 let default_conv_leq = default_conv CUMUL
-(*
-let convleqkey = CProfile.declare_profile "Kernel_reduction.conv_leq";;
-let conv_leq env t1 t2 =
-  CProfile.profile4 convleqkey conv_leq env t1 t2;;
-
-let convkey = CProfile.declare_profile "Kernel_reduction.conv";;
-let conv env t1 t2 =
-  CProfile.profile4 convleqkey conv env t1 t2;;
-*)
 
 (* Application with on-the-fly reduction *)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index a35f94e3ce..5f83e78eb0 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1273,7 +1273,7 @@ let export ?except ~output_native_objects senv dir =
   in
   let ast, symbols =
     if output_native_objects then
-      Nativelibrary.dump_library mp dir senv.env str
+      Nativelibrary.dump_library mp senv.env str
     else [], Nativevalues.empty_symbols
   in
   let lib = {
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 1a4c786e43..627bf42570 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -226,6 +226,7 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
     check_conv err cst poly (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2
   in
   match info1 with
+    | IndType _ | IndConstr _ -> error DefinitionFieldExpected
     | Constant cb1 ->
       let () = assert (List.is_empty cb1.const_hyps && List.is_empty cb2.const_hyps) in
       let cb1 = Declareops.subst_const_body subst1 cb1 in
@@ -254,18 +255,7 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
               let c1 = Mod_subst.force_constr lc1 in
               let c2 = Mod_subst.force_constr lc2 in
               check_conv NotConvertibleBodyField cst poly (infer_conv ?l2r:None ?evars:None ?ts:None) env c1 c2))
-   | IndType ((_kn,_i),_mind1) ->
-       CErrors.user_err Pp.(str @@
-       "The kernel does not recognize yet that a parameter can be " ^
-       "instantiated by an inductive type. Hint: you can rename the " ^
-       "inductive type and give a definition to map the old name to the new " ^
-       "name.")
-   | IndConstr (((_kn,_i),_j),_mind1) ->
-      CErrors.user_err Pp.(str @@
-       "The kernel does not recognize yet that a parameter can be " ^
-       "instantiated by a constructor. Hint: you can rename the " ^
-       "constructor and give a definition to map the old name to the new " ^
-       "name.")
+
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
   let mty1 = module_type_of_module msb1 in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 24aa4ed771..013892ad74 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -269,16 +269,14 @@ let build_constant_declaration env result =
         in
         Environ.really_needed env (Id.Set.union ids_typ ids_def), def
     | Some declared ->
-      let needed = Environ.really_needed env declared in
-      (* Transitive closure ensured by the upper layers *)
-      let () = assert (Id.Set.equal needed declared) in
-        (* We use the declared set and chain a check of correctness *)
-        declared,
-        match def with
-        | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *)
-        | Def cs as x ->
-          let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in
-          x
+      let declared = Environ.really_needed env declared in
+      (* We use the declared set and chain a check of correctness *)
+      declared,
+      match def with
+      | Undef _ | Primitive _ | OpaqueDef _ as x -> x (* nothing to check *)
+      | Def cs as x ->
+        let () = check_section_variables env declared typ (Mod_subst.force_constr cs) in
+        x
   in
   let univs = result.cook_universes in
   let hyps = List.filter (fun d -> Id.Set.mem (NamedDecl.get_id d) hyps) (Environ.named_context env) in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 741491c917..3a946fc03a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -644,12 +644,6 @@ let infer env constr =
   let constr, t = execute env constr in
   make_judge constr t
 
-let infer =
-  if Flags.profile then
-    let infer_key = CProfile.declare_profile "Fast_infer" in
-      CProfile.profile2 infer_key (fun b c -> infer b c)
-  else (fun b c -> infer b c)
-
 let assumption_of_judgment env {uj_val=c; uj_type=t} =
   infer_assumption env c t
 
@@ -785,15 +779,16 @@ let type_of_prim env u t =
     | PITT_type (ty,t) -> tr_prim_type (tr_type n) ty t
     | PITT_param i -> Constr.mkRel (n+i)
   in
-  let rec nary_op n = function
-    | [] -> assert false
-    | [ret_ty] -> tr_type n ret_ty
+  let rec nary_op n ret_ty = function
+    | [] -> tr_type n ret_ty
     | arg_ty :: r ->
-      Constr.mkProd(Context.nameR (Id.of_string "x"), tr_type n arg_ty, nary_op (n+1) r)
+        Constr.mkProd (Context.nameR (Id.of_string "x"),
+                       tr_type n arg_ty, nary_op (n + 1) ret_ty r)
   in
-  let params, sign = types t in
+  let params, args_ty, ret_ty = types t in
   assert (AUContext.size (univs t) = Instance.length u);
-  Vars.subst_instance_constr u (Term.it_mkProd_or_LetIn (nary_op 0 sign) params)
+  Vars.subst_instance_constr u
+    (Term.it_mkProd_or_LetIn (nary_op 0 ret_ty args_ty) params)
 
 let type_of_prim_or_type env u = let open CPrimitives in
   function
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index b988ec40a7..6db54a3bb6 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -251,28 +251,3 @@ type node = G.node =
 let repr g = G.repr g.graph
 
 let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) g
-
-(** Profiling *)
-
-let merge_constraints =
-  if Flags.profile then
-    let key = CProfile.declare_profile "merge_constraints" in
-      CProfile.profile2 key merge_constraints
-  else merge_constraints
-let check_constraints =
-  if Flags.profile then
-    let key = CProfile.declare_profile "check_constraints" in
-      CProfile.profile2 key check_constraints
-  else check_constraints
-
-let check_eq =
-  if Flags.profile then
-    let check_eq_key = CProfile.declare_profile "check_eq" in
-      CProfile.profile3 check_eq_key check_eq
-  else check_eq
-
-let check_leq =
-  if Flags.profile then
-    let check_leq_key = CProfile.declare_profile "check_leq" in
-      CProfile.profile3 check_leq_key check_leq
-  else check_leq
diff --git a/kernel/univ.ml b/kernel/univ.ml
index a2fd14025e..c2496f10b0 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -38,20 +38,22 @@ struct
   open Names
 
   module UGlobal = struct
-    type t = DirPath.t * int
+    type t = DirPath.t * string * int
 
-    let make dp i = (DirPath.hcons dp,i)
+    let make dp s i = (DirPath.hcons dp,s,i)
 
     let repr x : t = x
 
-    let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+    let equal (d, s, i) (d', s', i') = Int.equal i i' && DirPath.equal d d' && String.equal s s'
 
-    let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d)
+    let hash (d,s,i) = Hashset.Combine.combine3 i (String.hash s) (DirPath.hash d)
 
-    let compare (d, i) (d', i') =
-      let c = Int.compare i i' in
-      if Int.equal c 0 then DirPath.compare d d'
-      else c
+    let compare (d, s, i) (d', s', i') =
+      if i < i' then -1
+      else if i' < i then 1
+      else let c = DirPath.compare d d' in
+        if not (Int.equal c 0) then c
+        else String.compare s s'
   end
 
   type t =
@@ -84,10 +86,7 @@ struct
     | Set, Set -> 0
     | Set, _ -> -1
     | _, Set -> 1
-    | Level (dp1, i1), Level (dp2, i2) ->
-      if i1 < i2 then -1
-      else if i1 > i2 then 1
-      else DirPath.compare dp1 dp2
+    | Level l1, Level l2 -> UGlobal.compare l1 l2
     | Level _, _ -> -1
     | _, Level _ -> 1
     | Var n, Var m -> Int.compare n m
@@ -98,8 +97,8 @@ struct
       | SProp, SProp -> true
       | Prop, Prop -> true
       | Set, Set -> true
-      | Level (n,d), Level (n',d') ->
-        n == n' && d == d'
+      | Level (d,s,n), Level (d',s',n') ->
+        n == n' && s==s' && d == d'
       | Var n, Var n' -> n == n'
       | _ -> false
 
@@ -107,9 +106,10 @@ struct
     | SProp as x -> x
     | Prop as x -> x
     | Set as x -> x
-    | Level (d,n) as x ->
+    | Level (d,s,n) as x ->
+      let s' = CString.hcons s in
       let d' = Names.DirPath.hcons d in
-        if d' == d then x else Level (d',n)
+        if s' == s && d' == d then x else Level (d',s',n)
     | Var _n as x -> x
 
   open Hashset.Combine
@@ -119,7 +119,7 @@ struct
     | Prop -> combinesmall 1 1
     | Set -> combinesmall 1 2
     | Var n -> combinesmall 2 n
-    | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d))
+    | Level l -> combinesmall 3 (UGlobal.hash l)
 
 end
 
@@ -200,7 +200,10 @@ module Level = struct
     | SProp -> "SProp"
     | Prop -> "Prop"
     | Set -> "Set"
-    | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n
+    | Level (d,s,n) ->
+      Names.DirPath.to_string d ^
+      (if CString.is_empty s then "" else "." ^ s) ^
+      "." ^ string_of_int n
     | Var n -> "Var(" ^ string_of_int n ^ ")"
 
   let pr u = str (to_string u)
@@ -218,7 +221,7 @@ module Level = struct
 
   let name u =
     match data u with
-    | Level (d, n) -> Some (d, n)
+    | Level l -> Some l
     | _ -> None
 end
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 7286fc84cb..eeaa1ad62d 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -15,8 +15,8 @@ sig
   module UGlobal : sig
     type t
 
-    val make : Names.DirPath.t -> int -> t
-    val repr : t -> Names.DirPath.t * int
+    val make : Names.DirPath.t -> string -> int -> t
+    val repr : t -> Names.DirPath.t * string * int
     val equal : t -> t -> bool
     val hash : t -> int
     val compare : t -> t -> int
diff --git a/kernel/vars.ml b/kernel/vars.ml
index b09577d4db..b9991391c2 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -123,11 +123,6 @@ let substn_many lamv n c =
       | _ -> Constr.map_with_binders succ substrec depth c in
     substrec n c
 
-(*
-let substkey = CProfile.declare_profile "substn_many";;
-let substn_many lamv n c = CProfile.profile3 substkey substn_many lamv n c;;
-*)
-
 let make_subst = function
 | [] -> [||]
 | hd :: tl ->
@@ -343,9 +338,6 @@ let univ_instantiate_constr u c =
   assert (Int.equal (Instance.length u) (AUContext.size c.univ_abstracted_binder));
   subst_instance_constr u c.univ_abstracted_value
 
-(* let substkey = CProfile.declare_profile "subst_instance_constr";; *)
-(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *)
-
 let subst_instance_context s ctx =
   if Univ.Instance.is_empty s then ctx
   else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
diff --git a/kernel/vmbytecodes.ml b/kernel/vmbytecodes.ml
index c2b087f061..b5604d0593 100644
--- a/kernel/vmbytecodes.ml
+++ b/kernel/vmbytecodes.ml
@@ -35,6 +35,7 @@ type instruction =
   | Kpush
   | Kpop of int
   | Kpush_retaddr of Label.t
+  | Kshort_apply of int
   | Kapply of int
   | Kappterm of int * int
   | Kreturn of int
@@ -93,6 +94,7 @@ let rec pp_instr i =
   | Kpush -> str "push"
   | Kpop n -> str "pop " ++ int n
   | Kpush_retaddr lbl -> str "push_retaddr " ++ pp_lbl lbl
+  | Kshort_apply n -> str "short_apply " ++ int n
   | Kapply n -> str "apply " ++ int n
   | Kappterm(n, m) ->
       str "appterm " ++ int n ++ str ", " ++ int m
@@ -146,8 +148,8 @@ let rec pp_instr i =
         (Constant.print (fst id))
 
   | Kcamlprim (op, lbl) ->
-    str "camlcall " ++ str (CPrimitives.to_string op) ++ spc () ++
-    pp_lbl lbl
+    str "camlcall " ++ str (CPrimitives.to_string op) ++ str ", branch " ++
+    pp_lbl lbl ++ str " on accu"
 
 and pp_bytecodes c =
   match c with
diff --git a/kernel/vmbytecodes.mli b/kernel/vmbytecodes.mli
index eeca0d2ad1..d9e2d91177 100644
--- a/kernel/vmbytecodes.mli
+++ b/kernel/vmbytecodes.mli
@@ -30,6 +30,7 @@ type instruction =
   | 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 *)
+  | Kshort_apply of int                 (** number of arguments (arguments on top of stack) *)
   | 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 *)
diff --git a/kernel/vmbytegen.ml b/kernel/vmbytegen.ml
index 7d3b3469b0..b4d97228bf 100644
--- a/kernel/vmbytegen.ml
+++ b/kernel/vmbytegen.ml
@@ -461,7 +461,7 @@ let comp_app comp_fun comp_arg cenv f args sz cont =
   | None ->
       if nargs <= 4 then
         comp_args comp_arg cenv args sz
-          (Kpush :: (comp_fun cenv f (sz+nargs) (Kapply nargs :: cont)))
+          (Kpush :: (comp_fun cenv f (sz+nargs) (Kshort_apply nargs :: cont)))
       else
         let lbl,cont1 = label_code cont in
         Kpush_retaddr lbl ::
@@ -757,26 +757,25 @@ let rec compile_lam env cenv lam sz cont =
     let cont = code_makeblock ~stack_size:(sz+arity-1) ~arity ~tag cont in
     comp_args (compile_lam env) cenv args sz cont
 
-  | Lprim ((kn,u), op, args) when is_caml_prim op ->
+  | Lprim (kn, op, args) when is_caml_prim op ->
     let arity = CPrimitives.arity op in
     let nparams = CPrimitives.nparams op in
     let nargs = arity - nparams in
-    assert (arity = Array.length args && arity <= 4);
+    assert (arity = Array.length args && arity <= 4 && nargs >= 1);
     let (jump, cont) = make_branch cont in
     let lbl_default = Label.create () in
     let default =
-      let cont = [Kgetglobal kn; Kapply (arity + Univ.Instance.length u); jump] in
+      let cont = [Kshort_apply arity; jump] in
+      let cont = Kpush :: compile_get_global cenv kn (sz + arity) cont in
       let cont =
-        if Univ.Instance.is_empty u then cont
-        else comp_args compile_universe cenv (Univ.Instance.to_array u) (sz + arity) (Kpush::cont)
-      in
-      Klabel lbl_default ::
-      Kpush ::
-      if Int.equal nparams 0 then cont
-      else comp_args (compile_lam env) cenv (Array.sub args 0 nparams) (sz + nargs) (Kpush::cont)
-    in
+        if Int.equal nparams 0 then cont
+        else
+          let params = Array.sub args 0 nparams in
+          Kpush :: comp_args (compile_lam env) cenv params (sz + nargs) cont in
+      Klabel lbl_default :: cont in
     fun_code := Ksequence default :: !fun_code;
-    comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz (Kcamlprim (op, lbl_default) :: cont)
+    let cont = Kcamlprim (op, lbl_default) :: cont in
+    comp_args (compile_lam env) cenv (Array.sub args nparams nargs) sz cont
 
   | Lprim (kn, op, args) ->
     comp_args (compile_lam env) cenv args sz (Kprim(op, kn)::cont)
diff --git a/kernel/vmemitcodes.ml b/kernel/vmemitcodes.ml
index caa263432e..44e933ef26 100644
--- a/kernel/vmemitcodes.ml
+++ b/kernel/vmemitcodes.ml
@@ -300,8 +300,11 @@ let emit_instr env = function
       out env opPOP; out_int env n
   | Kpush_retaddr lbl ->
       out env opPUSH_RETADDR; out_label env lbl
+  | Kshort_apply n ->
+      assert (1 <= n && n <= 4);
+      out env(opAPPLY1 + n - 1)
   | Kapply n ->
-      if n <= 4 then out env(opAPPLY1 + n - 1) else (out env opAPPLY; out_int env n)
+      out env opAPPLY; out_int env n
   | Kappterm(n, sz) ->
       if n < 4 then (out env(opAPPTERM1 + n - 1); out_int env sz)
                else (out env opAPPTERM; out_int env n; out_int env sz)
diff --git a/kernel/vmlambda.ml b/kernel/vmlambda.ml
index e353348ac7..ee32384ec9 100644
--- a/kernel/vmlambda.ml
+++ b/kernel/vmlambda.ml
@@ -494,10 +494,6 @@ let makeblock tag nparams arity args =
   else Lmakeblock(tag, args)
 
 let makearray args def =
-  try
-    let p = Array.map get_value args in
-    Lval (val_of_parray @@ Parray.unsafe_of_array p (get_value def))
-  with Not_found ->
     let ar = Lmakeblock(0, args) in (* build the ocaml array *)
     let kind = Lmakeblock(0, [|ar; def|]) in (* Parray.Array *)
     Lmakeblock(0,[|kind|]) (* the reference *)
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 9944458d6b..938d1f28f7 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -459,8 +459,6 @@ let val_of_int i = (Obj.magic i : values)
 
 let val_of_uint i = (Obj.magic i : structured_values)
 
-let val_of_parray p = (Obj.magic p : structured_values)
-
 let atom_of_proj kn v =
   let r = Obj.new_block proj_tag 2 in
   Obj.set_field r 0 (Obj.repr kn);
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index d15595766a..534a85d773 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -148,7 +148,6 @@ val val_of_atom : atom -> values
 val val_of_int : int -> structured_values
 val val_of_block : tag -> structured_values array -> structured_values
 val val_of_uint : Uint63.t -> structured_values
-val val_of_parray : structured_values Parray.t -> structured_values
 
 external val_of_annot_switch : annot_switch -> values = "%identity"
 external val_of_proj_name : Projection.Repr.t -> values = "%identity"