1 files changed, 16 insertions, 18 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fd024b2157..5150ad4113 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -114,7 +114,7 @@ module DPMap = Map.Make(DirPath)
 
 type safe_environment =
   { env : Environ.env;
-    modpath : module_path;
+    modpath : ModPath.t;
     modvariant : modvariant;
     modresolver : Mod_subst.delta_resolver;
     paramresolver : Mod_subst.delta_resolver;
@@ -125,7 +125,7 @@ type safe_environment =
     future_cst : Univ.ContextSet.t Future.computation list;
     engagement : engagement option;
     required : vodigest DPMap.t;
-    loads : (module_path * module_body) list;
+    loads : (ModPath.t * module_body) list;
     local_retroknowledge : Retroknowledge.action list;
     native_symbols : Nativecode.symbols DPMap.t }
 
@@ -143,7 +143,7 @@ let rec library_dp_of_senv senv =
 
 let empty_environment =
   { env = Environ.empty_env;
-    modpath = initial_path;
+    modpath = ModPath.initial;
     modvariant = NONE;
     modresolver = Mod_subst.empty_delta_resolver;
     paramresolver = Mod_subst.empty_delta_resolver;
@@ -160,7 +160,7 @@ let empty_environment =
 
 let is_initial senv =
   match senv.revstruct, senv.modvariant with
-  | [], NONE -> ModPath.equal senv.modpath initial_path
+  | [], NONE -> ModPath.equal senv.modpath ModPath.initial
   | _ -> false
 
 let delta_of_senv senv = senv.modresolver,senv.paramresolver
@@ -249,14 +249,14 @@ let universes_of_private eff =
               in
               match cb.const_universes with
               | Monomorphic_const ctx ->
-                (Univ.ContextSet.of_context ctx) :: acc
+                ctx :: acc
               | Polymorphic_const _ -> acc
            )
            acc l
        | Entries.SEsubproof (c, cb, e) ->
          match cb.const_universes with
               | Monomorphic_const ctx ->
-                (Univ.ContextSet.of_context ctx) :: acc
+                ctx :: acc
               | Polymorphic_const _ -> acc
     )
     [] (Term_typing.uniq_seff eff)
@@ -389,7 +389,6 @@ let push_named_def (id,de) senv =
   | Monomorphic_const_entry _ -> false
   | Polymorphic_const_entry _ -> true
   in
-  let univs = Univ.ContextSet.of_context univs in
   let c, univs = match c with
     | Def c -> Mod_subst.force_constr c, univs
     | OpaqueDef o ->
@@ -425,9 +424,8 @@ let labels_of_mib mib =
 
 let globalize_constant_universes env cb =
   match cb.const_universes with
-  | Monomorphic_const ctx ->
-    let cstrs = Univ.ContextSet.of_context ctx in
-    Now (false, cstrs) ::  
+  | Monomorphic_const cstrs ->
+    Now (false, cstrs) ::
     (match cb.const_body with
      | (Undef _ | Def _) -> []
      | OpaqueDef lc ->
@@ -443,7 +441,7 @@ let globalize_constant_universes env cb =
 let globalize_mind_universes mb =
   match mb.mind_universes with
   | Monomorphic_ind ctx ->
-    [Now (false, Univ.ContextSet.of_context ctx)]
+    [Now (false, ctx)]
   | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)]
   | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)]
 
@@ -458,8 +456,8 @@ let constraints_of_sfb env sfb =
     It also performs the corresponding [add_constraints]. *)
 
 type generic_name =
-  | C of constant
-  | I of mutual_inductive
+  | C of Constant.t
+  | I of MutInd.t
   | M (** name already known, cf the mod_mp field *)
   | MT (** name already known, cf the mod_mp field *)
 
@@ -502,7 +500,7 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 type exported_private_constant = 
-  constant * private_constant_role
+  Constant.t * private_constant_role
 
 let add_constant_aux no_section senv (kn, cb) =
   let l = pi3 (Constant.repr3 kn) in
@@ -521,7 +519,7 @@ let add_constant_aux no_section senv (kn, cb) =
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
       update_resolver
-        (Mod_subst.add_inline_delta_resolver (user_con kn) (lev,None)) senv'
+        (Mod_subst.add_inline_delta_resolver (Constant.user kn) (lev,None)) senv'
     | _ -> senv'
   in
   senv''
@@ -535,7 +533,7 @@ let export_private_constants ~in_section ce senv =
   (ce, exported), senv
 
 let add_constant dir l decl senv =
-  let kn = make_con senv.modpath dir l in
+  let kn = Constant.make3 senv.modpath dir l in
   let no_section = DirPath.is_empty dir in
   let senv =
     let cb = 
@@ -562,7 +560,7 @@ let check_mind mie lab =
 
 let add_mind dir l mie senv =
   let () = check_mind mie l in
-  let kn = make_mind senv.modpath dir l in
+  let kn = MutInd.make3 senv.modpath dir l in
   let mib = Term_typing.translate_mind senv.env kn mie in
   let mib =
     match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
@@ -860,7 +858,7 @@ let export ?except senv dir =
     }
   in
   let ast, symbols =
-    if !Flags.native_compiler then
+    if !Flags.output_native_objects then
       Nativelibrary.dump_library mp dir senv.env str
     else [], Nativecode.empty_symbols
   in