Remove (useless) aliases from the API.

16 files changed, 129 insertions, 128 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9c3f97696..e66bf7e1b 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -10,6 +10,7 @@ open API
 open Pp
 open Util
 open Names
+open ModPath
 open Namegen
 open Nameops
 open Libnames
@@ -45,7 +46,7 @@ let pp_apply2 st par args =
 
 let pr_binding = function
   | [] -> mt ()
-  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
+  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") Id.print l
 
 let pp_tuple_light f = function
   | [] -> mt ()
@@ -274,8 +275,8 @@ let params_ren_add, params_ren_mem =
   seen at this level.
 *)
 
-type visible_layer = { mp : module_path;
-		       params : module_path list;
+type visible_layer = { mp : ModPath.t;
+		       params : ModPath.t list;
 		       mutable content : Label.t KMap.t; }
 
 let pop_visible, push_visible, get_visible =
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 4c9b1e1a5..004019e16 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -50,20 +50,20 @@ type phase = Pre | Impl | Intf
 val set_phase : phase -> unit
 val get_phase : unit -> phase
 
-val opened_libraries : unit -> module_path list
+val opened_libraries : unit -> ModPath.t list
 
 type kind = Term | Type | Cons | Mod
 
 val pp_global : kind -> global_reference -> string
-val pp_module : module_path -> string
+val pp_module : ModPath.t -> string
 
-val top_visible_mp : unit -> module_path
+val top_visible_mp : unit -> ModPath.t
 (* In [push_visible], the [module_path list] corresponds to
    module parameters, the innermost one coming first in the list *)
-val push_visible : module_path -> module_path list -> unit
+val push_visible : ModPath.t -> ModPath.t list -> unit
 val pop_visible : unit -> unit
 
-val get_duplicate : module_path -> Label.t -> string option
+val get_duplicate : ModPath.t -> Label.t -> string option
 
 type reset_kind = AllButExternal | Everything
 
@@ -73,7 +73,7 @@ val set_keywords : Id.Set.t -> unit
 
 (** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *)
 
-val mk_ind : string -> string -> mutual_inductive
+val mk_ind : string -> string -> MutInd.t
 
 (** Special hack for constants of type Ascii.ascii : if an
     [Extract Inductive ascii => char] has been declared, then
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 688bcd025..40ef6601d 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -11,6 +11,7 @@ open Miniml
 open Term
 open Declarations
 open Names
+open ModPath
 open Libnames
 open Globnames
 open Pp
@@ -28,13 +29,13 @@ open Common
 let toplevel_env () =
   let get_reference = function
     | (_,kn), Lib.Leaf o ->
-	let mp,_,l = repr_kn kn in
+	let mp,_,l = KerName.repr kn in
 	begin match Libobject.object_tag o with
 	  | "CONSTANT" ->
-            let constant = Global.lookup_constant (constant_of_kn kn) in
+            let constant = Global.lookup_constant (Constant.make1 kn) in
             Some (l, SFBconst constant)
 	  | "INDUCTIVE" ->
-            let inductive = Global.lookup_mind (mind_of_kn kn) in
+            let inductive = Global.lookup_mind (MutInd.make1 kn) in
             Some (l, SFBmind inductive)
 	  | "MODULE" ->
             let modl = Global.lookup_module (MPdot (mp, l)) in
@@ -73,21 +74,21 @@ module type VISIT = sig
 
   (* Add the module_path and all its prefixes to the mp visit list.
      We'll keep all fields of these modules. *)
-  val add_mp_all : module_path -> unit
+  val add_mp_all : ModPath.t -> unit
 
   (* Add reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
   val add_ref : global_reference -> unit
-  val add_kn : kernel_name -> unit
+  val add_kn : KerName.t -> unit
   val add_decl_deps : ml_decl -> unit
   val add_spec_deps : ml_spec -> unit
 
   (* Test functions:
      is a particular object a needed dependency for the current extraction ? *)
-  val needed_ind : mutual_inductive -> bool
-  val needed_cst : constant -> bool
-  val needed_mp : module_path -> bool
-  val needed_mp_all : module_path -> bool
+  val needed_ind : MutInd.t -> bool
+  val needed_cst : Constant.t -> bool
+  val needed_mp : ModPath.t -> bool
+  val needed_mp_all : ModPath.t -> bool
 end
 
 module Visit : VISIT = struct
@@ -102,8 +103,8 @@ module Visit : VISIT = struct
     v.kn <- KNset.empty;
     v.mp <- MPset.empty;
     v.mp_all <- MPset.empty
-  let needed_ind i = KNset.mem (user_mind i) v.kn
-  let needed_cst c = KNset.mem (user_con c) v.kn
+  let needed_ind i = KNset.mem (MutInd.user i) v.kn
+  let needed_cst c = KNset.mem (Constant.user c) v.kn
   let needed_mp mp = MPset.mem mp v.mp || MPset.mem mp v.mp_all
   let needed_mp_all mp = MPset.mem mp v.mp_all
   let add_mp mp =
@@ -112,10 +113,10 @@ module Visit : VISIT = struct
     check_loaded_modfile mp;
     v.mp <- MPset.union (prefixes_mp mp) v.mp;
     v.mp_all <- MPset.add mp v.mp_all
-  let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn)
+  let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (KerName.modpath kn)
   let add_ref = function
-    | ConstRef c -> add_kn (user_con c)
-    | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (user_mind ind)
+    | ConstRef c -> add_kn (Constant.user c)
+    | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (MutInd.user ind)
     | VarRef _ -> assert false
   let add_decl_deps = decl_iter_references add_ref add_ref add_ref
   let add_spec_deps = spec_iter_references add_ref add_ref add_ref
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 1e7a6ba5b..4f0ed953c 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -21,12 +21,12 @@ val extraction_library : bool -> Id.t -> unit
 (* For debug / external output via coqtop.byte + Drop : *)
 
 val mono_environment :
- global_reference list -> module_path list -> Miniml.ml_structure
+ global_reference list -> ModPath.t list -> Miniml.ml_structure
 
 (* Used by the Relation Extraction plugin *)
 
 val print_one_decl :
-  Miniml.ml_structure -> module_path -> Miniml.ml_decl -> Pp.std_ppcmds
+  Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.std_ppcmds
 
 (* Used by Extraction Compute *)
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index f1a50e7eb..2b7199a76 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -32,7 +32,7 @@ open Context.Rel.Declaration
 exception I of inductive_kind
 
 (* A set of all fixpoint functions currently being extracted *)
-let current_fixpoints = ref ([] : constant list)
+let current_fixpoints = ref ([] : Constant.t list)
 
 let none = Evd.empty
 
@@ -256,7 +256,7 @@ let rec extract_type env db j c args =
 		      let reason = if lvl == TypeScheme then Ktype else Kprop in
 		      Tarr (Tdummy reason, mld)))
     | Sort _ -> Tdummy Ktype (* The two logical cases. *)
-    | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop
+    | _ when sort_of env (applistc c args) == InProp -> Tdummy Kprop
     | Rel n ->
 	(match lookup_rel n env with
            | LocalDef (_,t,_) -> extract_type env db j (lift n t) args
@@ -277,7 +277,7 @@ let rec extract_type env db j c args =
 		  | Undef _ | OpaqueDef _ -> mlt
 		  | Def _ when is_custom r -> mlt
 		  | Def lbody ->
-		      let newc = applist (Mod_subst.force_constr lbody, args) in
+		      let newc = applistc (Mod_subst.force_constr lbody) args in
 		      let mlt' = extract_type env db j newc [] in
 		      (* ML type abbreviations interact badly with Coq *)
 		      (* reduction, so [mlt] and [mlt'] might be different: *)
@@ -291,7 +291,7 @@ let rec extract_type env db j c args =
 		  | Undef _  | OpaqueDef _ -> Tunknown (* Brutal approx ... *)
 		  | Def lbody ->
 		      (* We try to reduce. *)
-		      let newc = applist (Mod_subst.force_constr lbody, args) in
+		      let newc = applistc (Mod_subst.force_constr lbody) args in
 		      extract_type env db j newc []))
     | Ind ((kn,i),u) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
@@ -362,14 +362,14 @@ and extract_really_ind env kn mib =
        (cf Vector and bug #2570) *)
     let equiv =
       if lang () != Ocaml ||
-	 (not (modular ()) && at_toplevel (mind_modpath kn)) ||
-	 KerName.equal (canonical_mind kn) (user_mind kn)
+	 (not (modular ()) && at_toplevel (MutInd.modpath kn)) ||
+	 KerName.equal (MutInd.canonical kn) (MutInd.user kn)
       then
 	NoEquiv
       else
 	begin
-	  ignore (extract_ind env (mind_of_kn (canonical_mind kn)));
-	  Equiv (canonical_mind kn)
+	  ignore (extract_ind env (MutInd.make1 (MutInd.canonical kn)));
+	  Equiv (MutInd.canonical kn)
 	end
     in
     (* Everything concerning parameters. *)
@@ -865,7 +865,7 @@ let decomp_lams_eta_n n m env c t =
   (* we'd better keep rels' as long as possible. *)
   let rels = (List.firstn d rels) @ rels' in
   let eta_args = List.rev_map mkRel (List.interval 1 d) in
-  rels, applist (lift d c,eta_args)
+  rels, applistc (lift d c) eta_args
 
 (* Let's try to identify some situation where extracted code
    will allow generalisation of type variables *)
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 2b4b05a95..26268fb17 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -15,18 +15,18 @@ open Declarations
 open Environ
 open Miniml
 
-val extract_constant : env -> constant -> constant_body -> ml_decl
+val extract_constant : env -> Constant.t -> constant_body -> ml_decl
 
-val extract_constant_spec : env -> constant -> constant_body -> ml_spec
+val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec
 
 (** For extracting "module ... with ..." declaration *)
 
 val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option
 
 val extract_fixpoint :
-  env -> constant array -> (constr, types) prec_declaration -> ml_decl
+  env -> Constant.t array -> (constr, types) prec_declaration -> ml_decl
 
-val extract_inductive : env -> mutual_inductive -> ml_ind
+val extract_inductive : env -> MutInd.t -> ml_ind
 
 (** For extraction compute *)
 
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 6cba83ef9..76b435410 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -20,7 +20,6 @@ open Genarg
 open Stdarg
 open Pp
 open Names
-open Nameops
 open Table
 open Extract_env
 
@@ -35,7 +34,7 @@ END
 
 let pr_int_or_id _ _ _ = function
   | ArgInt i -> int i
-  | ArgId id -> pr_id id
+  | ArgId id -> Id.print id
 
 ARGUMENT EXTEND int_or_id
   PRINTED BY pr_int_or_id
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 8cdfb3499..4bd207a98 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -13,7 +13,6 @@ open Pp
 open CErrors
 open Util
 open Names
-open Nameops
 open Globnames
 open Table
 open Miniml
@@ -94,7 +93,7 @@ let preamble mod_name comment used_modules usf =
 let pp_abst = function
   | [] -> (mt ())
   | l  -> (str "\\" ++
-             prlist_with_sep (fun () -> (str " ")) pr_id l ++
+             prlist_with_sep (fun () -> (str " ")) Id.print l ++
              str " ->" ++ spc ())
 
 (*s The pretty-printer for haskell syntax *)
@@ -110,7 +109,7 @@ let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ -> assert false
     | Tvar i ->
-      (try pr_id (List.nth vl (pred i))
+      (try Id.print (List.nth vl (pred i))
        with Failure _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global Type r
     | Tglob (IndRef(kn,0),l)
@@ -149,7 +148,7 @@ let rec pp_expr par env args =
         (* Try to survive to the occurrence of a Dummy rel.
            TODO: we should get rid of this hack (cf. #592) *)
         let id = if Id.equal id dummy_name then Id.of_string "__" else id in
-        apply (pr_id id)
+        apply (Id.print id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
@@ -160,7 +159,7 @@ let rec pp_expr par env args =
 	apply2 st
     | MLletin (id,a1,a2) ->
 	let i,env' = push_vars [id_of_mlid id] env in
-	let pp_id = pr_id (List.hd i)
+	let pp_id = Id.print (List.hd i)
 	and pp_a1 = pp_expr false env [] a1
 	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
 	let pp_def =
@@ -224,10 +223,10 @@ and pp_cons_pat par r ppl =
 
 and pp_gen_pat par ids env = function
   | Pcons (r,l) -> pp_cons_pat par r (List.map (pp_gen_pat true ids env) l)
-  | Pusual r -> pp_cons_pat par r (List.map pr_id ids)
+  | Pusual r -> pp_cons_pat par r (List.map Id.print ids)
   | Ptuple l -> pp_boxed_tuple (pp_gen_pat false ids env) l
   | Pwild -> str "_"
-  | Prel n -> pr_id (get_db_name n env)
+  | Prel n -> Id.print (get_db_name n env)
 
 and pp_one_pat env (ids,p,t) =
   let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in
@@ -252,10 +251,10 @@ and pp_fix par env i (ids,bl) args =
     (v 0
        (v 1 (str "let {" ++ fnl () ++
 	     prvect_with_sep (fun () -> str ";" ++ fnl ())
-	       (fun (fi,ti) -> pp_function env (pr_id fi) ti)
+	       (fun (fi,ti) -> pp_function env (Id.print fi) ti)
 	       (Array.map2 (fun a b -> a,b) ids bl) ++
 	     str "}") ++
-        fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args))
+        fnl () ++ str "in " ++ pp_apply (Id.print ids.(i)) false args))
 
 and pp_function env f t =
   let bl,t' = collect_lams t in
@@ -267,19 +266,19 @@ and pp_function env f t =
 (*s Pretty-printing of inductive types declaration. *)
 
 let pp_logical_ind packet =
-  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
+  pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++
   pp_comment (str "with constructors : " ++
-	      prvect_with_sep spc pr_id packet.ip_consnames)
+	      prvect_with_sep spc Id.print packet.ip_consnames)
 
 let pp_singleton kn packet =
   let name = pp_global Type (IndRef (kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
   hov 2 (str "type " ++ name ++ spc () ++
-	 prlist_with_sep spc pr_id l ++
+	 prlist_with_sep spc Id.print l ++
 	 (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
 	 pp_comment (str "singleton inductive, whose constructor was " ++
-		     pr_id packet.ip_consnames.(0)))
+		     Id.print packet.ip_consnames.(0)))
 
 let pp_one_ind ip pl cv =
   let pl = rename_tvars keywords pl in
@@ -331,7 +330,7 @@ let pp_decl = function
 	    let ids,s = find_type_custom r in
 	    prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
 	  with Not_found ->
-	    prlist (fun id -> pr_id id ++ str " ") l ++
+	    prlist (fun id -> Id.print id ++ str " ") l ++
 	    if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl ()
 	    else str "=" ++ spc () ++ pp_type false l t
 	in
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 28226f225..ec28f4996 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -83,7 +83,7 @@ type ml_ind_packet = {
 
 type equiv =
   | NoEquiv
-  | Equiv of kernel_name
+  | Equiv of KerName.t
   | RenEquiv of string
 
 type ml_ind = {
@@ -138,13 +138,13 @@ and ml_pattern =
 (*s ML declarations. *)
 
 type ml_decl =
-  | Dind  of mutual_inductive * ml_ind
+  | Dind  of MutInd.t * ml_ind
   | Dtype of global_reference * Id.t list * ml_type
   | Dterm of global_reference * ml_ast * ml_type
   | Dfix  of global_reference array * ml_ast array * ml_type array
 
 type ml_spec =
-  | Sind  of mutual_inductive * ml_ind
+  | Sind  of MutInd.t * ml_ind
   | Stype of global_reference * Id.t list * ml_type option
   | Sval  of global_reference * ml_type
 
@@ -154,14 +154,14 @@ type ml_specif =
   | Smodtype of ml_module_type
 
 and ml_module_type =
-  | MTident of module_path
+  | MTident of ModPath.t
   | MTfunsig of MBId.t * ml_module_type * ml_module_type
-  | MTsig of module_path * ml_module_sig
+  | MTsig of ModPath.t * ml_module_sig
   | MTwith of ml_module_type * ml_with_declaration
 
 and ml_with_declaration =
   | ML_With_type of Id.t list * Id.t list * ml_type
-  | ML_With_module of Id.t list * module_path
+  | ML_With_module of Id.t list * ModPath.t
 
 and ml_module_sig = (Label.t * ml_specif) list
 
@@ -171,9 +171,9 @@ type ml_structure_elem =
   | SEmodtype of ml_module_type
 
 and ml_module_expr =
-  | MEident of module_path
+  | MEident of ModPath.t
   | MEfunctor of MBId.t * ml_module_type * ml_module_expr
-  | MEstruct of module_path * ml_module_structure
+  | MEstruct of ModPath.t * ml_module_structure
   | MEapply of ml_module_expr * ml_module_expr
 
 and ml_module_structure = (Label.t * ml_structure_elem) list
@@ -185,9 +185,9 @@ and ml_module =
 (* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp]
    implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *)
 
-type ml_structure = (module_path * ml_module_structure) list
+type ml_structure = (ModPath.t * ml_module_structure) list
 
-type ml_signature = (module_path * ml_module_sig) list
+type ml_signature = (ModPath.t * ml_module_sig) list
 
 type ml_flat_structure = ml_structure_elem list
 
@@ -203,10 +203,10 @@ type language_descr = {
 
   (* Concerning the source file *)
   file_suffix : string;
-  file_naming : module_path -> string;
+  file_naming : ModPath.t -> string;
   (* the second argument is a comment to add to the preamble *)
   preamble :
-    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs ->
     std_ppcmds;
   pp_struct : ml_structure -> std_ppcmds;
 
@@ -214,7 +214,7 @@ type language_descr = {
   sig_suffix : string option;
   (* the second argument is a comment to add to the preamble *)
   sig_preamble :
-    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs ->
     std_ppcmds;
   pp_sig : ml_signature -> std_ppcmds;
 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 5a50899c6..3a70a5020 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -29,9 +29,9 @@ let dummy_name = Id.of_string "_"
 let anonymous = Id anonymous_name
 
 let id_of_name = function
-  | Anonymous -> anonymous_name
-  | Name id when Id.equal id dummy_name -> anonymous_name
-  | Name id -> id
+  | Name.Anonymous -> anonymous_name
+  | Name.Name id when Id.equal id dummy_name -> anonymous_name
+  | Name.Name id -> id
 
 let id_of_mlid = function
   | Dummy -> dummy_name
@@ -1488,7 +1488,7 @@ let inline_test r t =
 
 let con_of_string s =
   let d, id = Libnames.split_dirpath (dirpath_of_string s) in
-  Constant.make2 (MPfile d) (Label.of_id id)
+  Constant.make2 (ModPath.MPfile d) (Label.of_id id)
 
 let manual_inline_set =
   List.fold_right (fun x -> Cset_env.add (con_of_string x))
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 2655dfc89..6924dc9ff 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -49,7 +49,7 @@ end
 
 (*s Utility functions over ML types without meta *)
 
-val type_mem_kn : mutual_inductive -> ml_type -> bool
+val type_mem_kn : MutInd.t -> ml_type -> bool
 
 val type_maxvar : ml_type -> int
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 2b1e81060..6c38813e4 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -8,6 +8,7 @@
 
 open API
 open Names
+open ModPath
 open Globnames
 open CErrors
 open Util
@@ -111,7 +112,7 @@ let ind_iter_references do_term do_cons do_type kn ind =
     do_type (IndRef ip);
     if lang () == Ocaml then
       (match ind.ind_equiv with
-	 | Miniml.Equiv kne -> do_type (IndRef (mind_of_kn kne, snd ip));
+	 | Miniml.Equiv kne -> do_type (IndRef (MutInd.make1 kne, snd ip));
 	 | _ -> ());
     Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
   in
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 45e890be0..9a67baa96 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -26,7 +26,7 @@ val signature_of_structure : ml_structure -> ml_signature
 
 val mtyp_of_mexpr : ml_module_expr -> ml_module_type
 
-val msid_of_mt : ml_module_type -> module_path
+val msid_of_mt : ml_module_type -> ModPath.t
 
 val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
 
@@ -37,5 +37,5 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
    optimizations. The first argument is the list of objects we want to appear.
 *)
 
-val optimize_struct : global_reference list * module_path list ->
+val optimize_struct : global_reference list * ModPath.t list ->
   ml_structure -> ml_structure
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 83abaf508..16feaf4d6 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -13,7 +13,7 @@ open Pp
 open CErrors
 open Util
 open Names
-open Nameops
+open ModPath
 open Globnames
 open Table
 open Miniml
@@ -29,7 +29,7 @@ let pp_tvar id = str ("'" ^ Id.to_string id)
 let pp_abst = function
   | [] -> mt ()
   | l  ->
-      str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++
+      str "fun " ++ prlist_with_sep (fun () -> str " ") Id.print l ++
       str " ->" ++ spc ()
 
 let pp_parameters l =
@@ -183,7 +183,7 @@ let rec pp_expr par env args =
         (* Try to survive to the occurrence of a Dummy rel.
            TODO: we should get rid of this hack (cf. #592) *)
         let id = if Id.equal id dummy_name then Id.of_string "__" else id in
-        apply (pr_id id)
+        apply (Id.print id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
@@ -195,7 +195,7 @@ let rec pp_expr par env args =
 	apply2 st
     | MLletin (id,a1,a2) ->
 	let i,env' = push_vars [id_of_mlid id] env in
-	let pp_id = pr_id (List.hd i)
+	let pp_id = Id.print (List.hd i)
 	and pp_a1 = pp_expr false env [] a1
 	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
 	hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
@@ -331,10 +331,10 @@ and pp_cons_pat r ppl =
 
 and pp_gen_pat ids env = function
   | Pcons (r, l) -> pp_cons_pat r (List.map (pp_gen_pat ids env) l)
-  | Pusual r -> pp_cons_pat r (List.map pr_id ids)
+  | Pusual r -> pp_cons_pat r (List.map Id.print ids)
   | Ptuple l -> pp_boxed_tuple (pp_gen_pat ids env) l
   | Pwild -> str "_"
-  | Prel n -> pr_id (get_db_name n env)
+  | Prel n -> Id.print (get_db_name n env)
 
 and pp_ifthenelse env expr pv = match pv with
   | [|([],tru,the);([],fal,els)|] when
@@ -373,7 +373,7 @@ and pp_function env t =
 	  v 0 (pp_pat env' pv)
 	else
           pr_binding (List.rev bl) ++
-          str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
+          str " = match " ++ Id.print (List.hd bl) ++ str " with" ++ fnl () ++
 	  v 0 (pp_pat env' pv)
     | _ ->
           pr_binding (List.rev bl) ++
@@ -388,10 +388,10 @@ and pp_fix par env i (ids,bl) args =
     (v 0 (str "let rec " ++
 	  prvect_with_sep
       	    (fun () -> fnl () ++ str "and ")
-	    (fun (fi,ti) -> pr_id fi ++ pp_function env ti)
+	    (fun (fi,ti) -> Id.print fi ++ pp_function env ti)
 	    (Array.map2 (fun id b -> (id,b)) ids bl) ++
 	  fnl () ++
-	  hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
+	  hov 2 (str "in " ++ pp_apply (Id.print ids.(i)) false args)))
 
 (* Ad-hoc double-newline in v boxes, with enough negative whitespace
    to avoid indenting the intermediate blank line *)
@@ -432,7 +432,7 @@ let pp_Dfix (rv,c,t) =
 let pp_equiv param_list name = function
   | NoEquiv, _ -> mt ()
   | Equiv kn, i ->
-      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (mind_of_kn kn,i))
+      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (MutInd.make1 kn,i))
   | RenEquiv ren, _  ->
       str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
 
@@ -452,10 +452,10 @@ let pp_one_ind prefix ip_equiv pl name cnames ctyps =
   else fnl () ++ v 0 (prvecti pp_constructor ctyps)
 
 let pp_logical_ind packet =
-  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
+  pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++
   fnl () ++
   pp_comment (str "with constructors : " ++
-	      prvect_with_sep spc pr_id packet.ip_consnames) ++
+	      prvect_with_sep spc Id.print packet.ip_consnames) ++
   fnl ()
 
 let pp_singleton kn packet =
@@ -464,7 +464,7 @@ let pp_singleton kn packet =
   hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
 	 pp_comment (str "singleton inductive, whose constructor was " ++
-		     pr_id packet.ip_consnames.(0)))
+		     Id.print packet.ip_consnames.(0)))
 
 let pp_record kn fields ip_equiv packet =
   let ind = IndRef (kn,0) in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 607ca1b3a..b82c5257e 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -8,9 +8,9 @@
 
 open API
 open Names
+open ModPath
 open Term
 open Declarations
-open Nameops
 open Namegen
 open Libobject
 open Goptions
@@ -36,14 +36,14 @@ module Refset' = Refset_env
 
 let occur_kn_in_ref kn = function
   | IndRef (kn',_)
-  | ConstructRef ((kn',_),_) -> Names.eq_mind kn kn'
+  | ConstructRef ((kn',_),_) -> MutInd.equal kn kn'
   | ConstRef _ -> false
   | VarRef _ -> assert false
 
 let repr_of_r = function
-  | ConstRef kn -> repr_con kn
+  | ConstRef kn -> Constant.repr3 kn
   | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) -> repr_mind kn
+  | ConstructRef ((kn,_),_) -> MutInd.repr3 kn
   | VarRef _ -> assert false
 
 let modpath_of_r r =
@@ -65,7 +65,7 @@ let raw_string_of_modfile = function
   | _ -> assert false
 
 let is_toplevel mp =
-  ModPath.equal mp initial_path || ModPath.equal mp (Lib.current_mp ())
+  ModPath.equal mp ModPath.initial || ModPath.equal mp (Lib.current_mp ())
 
 let at_toplevel mp =
   is_modfile mp || is_toplevel mp
@@ -265,8 +265,8 @@ let safe_basename_of_global r =
       anomaly (Pp.str "Inductive object unknown to extraction and not globally visible.")
   in
   match r with
-    | ConstRef kn -> Label.to_id (con_label kn)
-    | IndRef (kn,0) -> Label.to_id (mind_label kn)
+    | ConstRef kn -> Label.to_id (Constant.label kn)
+    | IndRef (kn,0) -> Label.to_id (MutInd.label kn)
     | IndRef (kn,i) ->
       (try (unsafe_lookup_ind kn).ind_packets.(i).ip_typename
        with Not_found -> last_chance r)
@@ -287,8 +287,8 @@ let safe_pr_long_global r =
   try Printer.pr_global r
   with Not_found -> match r with
     | ConstRef kn ->
-	let mp,_,l = repr_con kn in
-	str ((string_of_mp mp)^"."^(Label.to_string l))
+	let mp,_,l = Constant.repr3 kn in
+	str ((ModPath.to_string mp)^"."^(Label.to_string l))
     | _ -> assert false
 
 let pr_long_mp mp =
@@ -417,7 +417,7 @@ let error_singleton_become_prop id og =
                 str " (or in its mutual block)"
     | None -> mt ()
   in
-  err (str "The informative inductive type " ++ pr_id id ++
+  err (str "The informative inductive type " ++ Id.print id ++
        str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++
        str "This happens when a sort-polymorphic singleton inductive type\n" ++
        str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++
@@ -722,7 +722,7 @@ let add_implicits r l =
          let i = List.index Name.equal (Name id) names in
          Int.Set.add i s
        with Not_found ->
-	 err (str "No argument " ++ pr_id id ++ str " for " ++
+	 err (str "No argument " ++ Id.print id ++ str " for " ++
 	      safe_pr_global r)
   in
   let ints = List.fold_left add_arg Int.Set.empty l in
@@ -800,7 +800,7 @@ let extraction_blacklist l =
 (* Printing part *)
 
 let print_extraction_blacklist () =
-  prlist_with_sep fnl pr_id (Id.Set.elements !blacklist_table)
+  prlist_with_sep fnl Id.print (Id.Set.elements !blacklist_table)
 
 (* Reset part *)
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index cd1667bdb..cfe75bf4e 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -22,22 +22,22 @@ val safe_basename_of_global : global_reference -> Id.t
 
 val warning_axioms : unit -> unit
 val warning_opaques : bool -> unit
-val warning_ambiguous_name : ?loc:Loc.t -> qualid * module_path * global_reference -> unit
+val warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * global_reference -> unit
 val warning_id : string -> unit
 val error_axiom_scheme : global_reference -> int -> 'a
 val error_constant : global_reference -> 'a
 val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
-val error_module_clash : module_path -> module_path -> 'a
-val error_no_module_expr : module_path -> 'a
+val error_module_clash : ModPath.t -> ModPath.t -> 'a
+val error_no_module_expr : ModPath.t -> 'a
 val error_singleton_become_prop : Id.t -> global_reference option -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
-val error_MPfile_as_mod : module_path -> bool -> 'a
+val error_MPfile_as_mod : ModPath.t -> bool -> 'a
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
-val check_loaded_modfile : module_path -> unit
+val check_loaded_modfile : ModPath.t -> unit
 val msg_of_implicit : kill_reason -> string
 val err_or_warn_remaining_implicit : kill_reason -> unit
 
@@ -45,22 +45,22 @@ val info_file : string -> unit
 
 (*s utilities about [module_path] and [kernel_names] and [global_reference] *)
 
-val occur_kn_in_ref : mutual_inductive -> global_reference -> bool
-val repr_of_r : global_reference -> module_path * DirPath.t * Label.t
-val modpath_of_r : global_reference -> module_path
+val occur_kn_in_ref : MutInd.t -> global_reference -> bool
+val repr_of_r : global_reference -> ModPath.t * DirPath.t * Label.t
+val modpath_of_r : global_reference -> ModPath.t
 val label_of_r : global_reference -> Label.t
-val base_mp : module_path -> module_path
-val is_modfile : module_path -> bool
-val string_of_modfile : module_path -> string
-val file_of_modfile : module_path -> string
-val is_toplevel : module_path -> bool
-val at_toplevel : module_path -> bool
-val mp_length : module_path -> int
-val prefixes_mp : module_path -> MPset.t
+val base_mp : ModPath.t -> ModPath.t
+val is_modfile : ModPath.t -> bool
+val string_of_modfile : ModPath.t -> string
+val file_of_modfile : ModPath.t -> string
+val is_toplevel : ModPath.t -> bool
+val at_toplevel : ModPath.t -> bool
+val mp_length : ModPath.t -> int
+val prefixes_mp : ModPath.t -> MPset.t
 val common_prefix_from_list :
-  module_path -> module_path list -> module_path option
-val get_nth_label_mp : int -> module_path -> Label.t
-val labels_of_ref : global_reference -> module_path * Label.t list
+  ModPath.t -> ModPath.t list -> ModPath.t option
+val get_nth_label_mp : int -> ModPath.t -> Label.t
+val labels_of_ref : global_reference -> ModPath.t * Label.t list
 
 (*s Some table-related operations *)
 
@@ -72,16 +72,16 @@ val labels_of_ref : global_reference -> module_path * Label.t list
    [mutual_inductive_body] as checksum. In both case, we should ideally
    also check the env *)
 
-val add_typedef : constant -> constant_body -> ml_type -> unit
-val lookup_typedef : constant -> constant_body -> ml_type option
+val add_typedef : Constant.t -> constant_body -> ml_type -> unit
+val lookup_typedef : Constant.t -> constant_body -> ml_type option
 
-val add_cst_type : constant -> constant_body -> ml_schema -> unit
-val lookup_cst_type : constant -> constant_body -> ml_schema option
+val add_cst_type : Constant.t -> constant_body -> ml_schema -> unit
+val lookup_cst_type : Constant.t -> constant_body -> ml_schema option
 
-val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit
-val lookup_ind : mutual_inductive -> mutual_inductive_body -> ml_ind option
+val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit
+val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option
 
-val add_inductive_kind : mutual_inductive -> inductive_kind -> unit
+val add_inductive_kind : MutInd.t -> inductive_kind -> unit
 val is_coinductive : global_reference -> bool
 val is_coinductive_type : ml_type -> bool
 (* What are the fields of a record (empty for a non-record) *)
@@ -89,10 +89,10 @@ val get_record_fields :
   global_reference -> global_reference option list
 val record_fields_of_type : ml_type -> global_reference option list
 
-val add_recursors : Environ.env -> mutual_inductive -> unit
+val add_recursors : Environ.env -> MutInd.t -> unit
 val is_recursor : global_reference -> bool
 
-val add_projection : int -> constant -> inductive -> unit
+val add_projection : int -> Constant.t -> inductive -> unit
 val is_projection : global_reference -> bool
 val projection_arity : global_reference -> int
 val projection_info : global_reference -> inductive * int (* arity *)