Modulification of Label

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16097 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 168 insertions, 117 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index baeab9142c..e2ebce28a8 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -385,7 +385,7 @@ type structure_field_body =
   | SFBmodule of module_body
   | SFBmodtype of module_type_body
 
-and structure_body = (label * structure_field_body) list
+and structure_body = (Label.t * structure_field_body) list
 
 and struct_expr_body =
   | SEBident of module_path
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index fc142d2532..3b43baa79e 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -198,7 +198,7 @@ type structure_field_body =
     a [structure_body], once for a module ([SFBmodule] or [SFBmodtype])
     and once for an object ([SFBconst] or [SFBmind]) *)
 
-and structure_body = (label * structure_field_body) list
+and structure_body = (Label.t * structure_field_body) list
 
 and struct_expr_body =
   | SEBident of module_path
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b358d805ab..0d29cf10b6 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -41,7 +41,7 @@ let is_modular = function
 
 let rec list_split_assoc ((k,m) as km) rev_before = function
   | [] -> raise Not_found
-  | (k',b)::after when eq_label k k' && (is_modular b) == (m : bool) -> rev_before,b,after
+  | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) -> rev_before,b,after
   | h::tail -> list_split_assoc km (h::rev_before) tail
 
 let discr_resolver env mtb =
@@ -80,7 +80,7 @@ and check_with_def env sign (idl,c) mp equiv =
     | [] -> assert false
     | id::idl -> id,idl
   in
-  let l = label_of_id id in
+  let l = Label.of_id id in
     try
       let not_empty = match idl with [] -> false | _ :: _ -> true in
       let rev_before,spec,after = list_split_assoc (l, not_empty) [] sig_b in
@@ -125,7 +125,7 @@ and check_with_def env sign (idl,c) mp equiv =
 	      (* Definition inside a sub-module *)
 	      let old = match spec with
 		| SFBmodule msb -> msb
-		| _ -> error_not_a_module (string_of_label l)
+		| _ -> error_not_a_module (Label.to_string l)
 	      in
 		begin
 		  match old.mod_expr with
@@ -153,7 +153,7 @@ and check_with_mod env sign (idl,mp1) mp equiv =
     | [] -> assert false
     | id::idl -> id,idl
   in
-  let l = label_of_id id in
+  let l = Label.of_id id in
     try
       let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in
       let before = List.rev rev_before in
@@ -162,7 +162,7 @@ and check_with_mod env sign (idl,mp1) mp equiv =
 	      (* Toplevel module definition *)
 	      let old = match spec with
 		  SFBmodule msb -> msb
-		| _ -> error_not_a_module (string_of_label l)
+		| _ -> error_not_a_module (Label.to_string l)
 	      in
 	      let mb_mp1 = (lookup_module mp1 env) in
 	      let mtb_mp1 = 
@@ -175,7 +175,7 @@ and check_with_mod env sign (idl,mp1) mp equiv =
 			  (check_subtypes env' mtb_mp1 
 			     (module_type_of_module None old))
 			  old.mod_constraints
-			with Failure _ -> error_incorrect_with_constraint (label_of_id id)
+			with Failure _ -> error_incorrect_with_constraint (Label.of_id id)
 		      end
 		  | Some (SEBident(mp')) ->
 		      check_modpath_equiv env' mp1 mp';
@@ -197,7 +197,7 @@ and check_with_mod env sign (idl,mp1) mp equiv =
 	      (* Module definition of a sub-module *)
 	      let old = match spec with
 		  SFBmodule msb -> msb
-		| _ -> error_not_a_module (string_of_label l)
+		| _ -> error_not_a_module (Label.to_string l)
 	      in
 	      begin
 		match old.mod_expr with
@@ -215,7 +215,7 @@ and check_with_mod env sign (idl,mp1) mp equiv =
 			SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
 		      new_equiv,cst
 		  | Some (SEBident(mp')) ->
-		      let mpnew = rebuild_mp mp' (List.map label_of_id idl) in
+		      let mpnew = rebuild_mp mp' (List.map Label.of_id idl) in
 			check_modpath_equiv env' mpnew mp;
 			  SEBstruct(before@(l,spec)::after)
 			    ,equiv,empty_constraint
diff --git a/kernel/modops.ml b/kernel/modops.ml
index b81627f22b..e7afec2a05 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -44,24 +44,24 @@ type signature_mismatch_error =
   | NoTypeConstraintExpected
 
 type module_typing_error =
-  | SignatureMismatch of label * structure_field_body * signature_mismatch_error
-  | LabelAlreadyDeclared of label
+  | SignatureMismatch of Label.t * structure_field_body * signature_mismatch_error
+  | LabelAlreadyDeclared of Label.t
   | ApplicationToNotPath of module_struct_entry
   | NotAFunctor of struct_expr_body
   | IncompatibleModuleTypes of module_type_body * module_type_body
   | NotEqualModulePaths of module_path * module_path
-  | NoSuchLabel of label
-  | IncompatibleLabels of label * label
+  | NoSuchLabel of Label.t
+  | IncompatibleLabels of Label.t * Label.t
   | SignatureExpected of struct_expr_body
   | NoModuleToEnd
   | NoModuleTypeToEnd
   | NotAModule of string
   | NotAModuleType of string
-  | NotAConstant of label
-  | IncorrectWithConstraint of label
-  | GenerativeModuleExpected of label
-  | NonEmptyLocalContect of label option
-  | LabelMissing of label * string
+  | NotAConstant of Label.t
+  | IncorrectWithConstraint of Label.t
+  | GenerativeModuleExpected of Label.t
+  | NonEmptyLocalContect of Label.t option
+  | LabelMissing of Label.t * string
 
 exception ModuleTypingError of module_typing_error
 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 0d87ce88b4..13129cdbdf 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -71,28 +71,28 @@ type signature_mismatch_error =
   | NoTypeConstraintExpected
 
 type module_typing_error =
-  | SignatureMismatch of label * structure_field_body * signature_mismatch_error
-  | LabelAlreadyDeclared of label
+  | SignatureMismatch of Label.t * structure_field_body * signature_mismatch_error
+  | LabelAlreadyDeclared of Label.t
   | ApplicationToNotPath of module_struct_entry
   | NotAFunctor of struct_expr_body
   | IncompatibleModuleTypes of module_type_body * module_type_body
   | NotEqualModulePaths of module_path * module_path
-  | NoSuchLabel of label
-  | IncompatibleLabels of label * label
+  | NoSuchLabel of Label.t
+  | IncompatibleLabels of Label.t * Label.t
   | SignatureExpected of struct_expr_body
   | NoModuleToEnd
   | NoModuleTypeToEnd
   | NotAModule of string
   | NotAModuleType of string
-  | NotAConstant of label
-  | IncorrectWithConstraint of label
-  | GenerativeModuleExpected of label
-  | NonEmptyLocalContect of label option
-  | LabelMissing of label * string
+  | NotAConstant of Label.t
+  | IncorrectWithConstraint of Label.t
+  | GenerativeModuleExpected of Label.t
+  | NonEmptyLocalContect of Label.t option
+  | LabelMissing of Label.t * string
 
 exception ModuleTypingError of module_typing_error
 
-val error_existing_label : label -> 'a
+val error_existing_label : Label.t -> 'a
 
 val error_application_to_not_path : module_struct_entry -> 'a
 
@@ -100,11 +100,11 @@ val error_incompatible_modtypes :
   module_type_body -> module_type_body -> 'a
 
 val error_signature_mismatch :
-  label -> structure_field_body -> signature_mismatch_error -> 'a
+  Label.t -> structure_field_body -> signature_mismatch_error -> 'a
 
-val error_incompatible_labels : label -> label -> 'a
+val error_incompatible_labels : Label.t -> Label.t -> 'a
 
-val error_no_such_label : label -> 'a
+val error_no_such_label : Label.t -> 'a
 
 val error_signature_expected : struct_expr_body -> 'a
 
@@ -114,12 +114,12 @@ val error_no_modtype_to_end : unit -> 'a
 
 val error_not_a_module : string -> 'a
 
-val error_not_a_constant : label -> 'a
+val error_not_a_constant : Label.t -> 'a
 
-val error_incorrect_with_constraint : label -> 'a
+val error_incorrect_with_constraint : Label.t -> 'a
 
-val error_generative_module_expected : label -> 'a
+val error_generative_module_expected : Label.t -> 'a
 
-val error_non_empty_local_context : label option -> 'a
+val error_non_empty_local_context : Label.t option -> 'a
 
-val error_no_such_label_sub : label->string->'a
+val error_no_such_label_sub : Label.t->string->'a
diff --git a/kernel/names.ml b/kernel/names.ml
index e10b34eb2e..9b41fed1f0 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -49,6 +49,8 @@ struct
 
   let to_string id = String.copy id
 
+  let print id = str id
+
   module Self =
   struct
     type t = string
@@ -217,24 +219,33 @@ let id_of_mbid (_,s,_) = s
 
 (** {6 Names of structure elements } *)
 
+module Label =
+struct
+  include Id
+  let make = Id.of_string
+  let of_id id = id
+  let to_id id = id
+end
+
+(** Compatibility layer for [Label] *)
+
 type label = Id.t
 
-let mk_label = id_of_string
-let string_of_label = string_of_id
-let pr_label l = str (string_of_label l)
-let id_of_label l = l
-let label_of_id id = id
-let eq_label = String.equal
+let mk_label = Label.make
+let string_of_label = Label.to_string
+let pr_label = Label.print
+let id_of_label = Label.to_id
+let label_of_id = Label.of_id
+let eq_label = Label.equal
 
-module Labset = Idset
-module Labmap = Idmap
+(** / End of compatibility layer for [Label] *)
 
 (** {6 The module part of the kernel name } *)
 
 type module_path =
   | MPfile of Dir_path.t
   | MPbound of mod_bound_id
-  | MPdot of module_path * label
+  | MPdot of module_path * Label.t
 
 let rec check_bound_mp = function
   | MPbound _ -> true
@@ -244,7 +255,7 @@ let rec check_bound_mp = function
 let rec string_of_mp = function
   | MPfile sl -> string_of_dirpath sl
   | MPbound uid -> string_of_uid uid
-  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ string_of_label l
+  | MPdot (mp,l) -> string_of_mp mp ^ "." ^ Label.to_string l
 
 (** we compare labels first if both are MPdots *)
 let rec mp_ord mp1 mp2 =
@@ -277,7 +288,7 @@ let initial_path = MPfile Dir_path.initial
 
 (** {6 Kernel names } *)
 
-type kernel_name = module_path * Dir_path.t * label
+type kernel_name = module_path * Dir_path.t * Label.t
 
 let make_kn mp dir l = (mp,dir,l)
 let repr_kn kn = kn
@@ -293,7 +304,7 @@ let string_of_kn (mp,dir,l) =
   | [] -> "."
   | _ -> "#" ^ string_of_dirpath dir ^ "#"
   in
-  string_of_mp mp ^ str_dir ^ string_of_label l
+  string_of_mp mp ^ str_dir ^ Label.to_string l
 
 let pr_kn kn = str (string_of_kn kn)
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 150c04608c..78d2d62169 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -33,6 +33,9 @@ sig
   val to_string : t -> string
   (** Converts a identifier into an string. *)
 
+  val print : t -> Pp.std_ppcmds
+  (** Pretty-printer. *)
+
   module Set : Set.S with type elt = t
   (** Finite sets of identifiers. *)
 
@@ -101,19 +104,33 @@ module ModIdmap : Map.S with type key = module_ident
 
 (** {6 Names of structure elements } *)
 
-type label
+module Label :
+sig
+  type t
+  (** Type of labels *)
 
-val mk_label : string -> label
-val string_of_label : label -> string
-val pr_label : label -> Pp.std_ppcmds
+  val equal : t -> t -> bool
+  (** Equality over labels *)
 
-val label_of_id : Id.t -> label
-val id_of_label : label -> Id.t
+  val make : string -> t
+  (** Create a label out of a string. *)
 
-val eq_label : label -> label -> bool
+  val to_string : t -> string
+  (** Conversion to string. *)
+
+  val of_id : Id.t -> t
+  (** Conversion from an identifier. *)
 
-module Labset : Set.S with type elt = label
-module Labmap : Map.S with type key = label
+  val to_id : t -> Id.t
+  (** Conversion to an identifier. *)
+
+  val print : t -> Pp.std_ppcmds
+  (** Pretty-printer. *)
+
+  module Set : Set.S with type elt = t
+  module Map : Map.S with type key = t
+
+end
 
 (** {6 Unique names for bound modules } *)
 
@@ -136,7 +153,7 @@ val string_of_mbid : mod_bound_id -> string
 type module_path =
   | MPfile of Dir_path.t
   | MPbound of mod_bound_id
-  | MPdot of module_path * label
+  | MPdot of module_path * Label.t
 
 val mp_ord : module_path -> module_path -> int
 val mp_eq : module_path -> module_path -> bool
@@ -156,11 +173,11 @@ val initial_path : module_path (** [= MPfile initial_dir] *)
 type kernel_name
 
 (** Constructor and destructor *)
-val make_kn : module_path -> Dir_path.t -> label -> kernel_name
-val repr_kn : kernel_name -> module_path * Dir_path.t * label
+val make_kn : module_path -> Dir_path.t -> Label.t -> kernel_name
+val repr_kn : kernel_name -> module_path * Dir_path.t * Label.t
 
 val modpath : kernel_name -> module_path
-val label : kernel_name -> label
+val label : kernel_name -> Label.t
 
 val string_of_kn : kernel_name -> string
 val pr_kn : kernel_name -> Pp.std_ppcmds
@@ -200,17 +217,17 @@ module Constrmap_env : Map.S with type key = constructor
 
 val constant_of_kn : kernel_name -> constant
 val constant_of_kn_equiv : kernel_name -> kernel_name -> constant
-val make_con : module_path -> Dir_path.t -> label -> constant
+val make_con : module_path -> Dir_path.t -> Label.t -> constant
 val make_con_equiv : module_path -> module_path -> Dir_path.t 
-  -> label -> constant
+  -> Label.t -> constant
 val user_con : constant -> kernel_name
 val canonical_con : constant -> kernel_name
-val repr_con : constant -> module_path * Dir_path.t * label
+val repr_con : constant -> module_path * Dir_path.t * Label.t
 val eq_constant : constant -> constant -> bool
-val con_with_label : constant -> label -> constant
+val con_with_label : constant -> Label.t -> constant
 
 val string_of_con : constant -> string
-val con_label : constant -> label
+val con_label : constant -> Label.t
 val con_modpath : constant -> module_path
 val pr_con : constant -> Pp.std_ppcmds
 val debug_pr_con : constant -> Pp.std_ppcmds
@@ -220,16 +237,16 @@ val debug_string_of_con : constant -> string
 
 val mind_of_kn : kernel_name -> mutual_inductive
 val mind_of_kn_equiv : kernel_name -> kernel_name -> mutual_inductive
-val make_mind : module_path -> Dir_path.t -> label -> mutual_inductive
+val make_mind : module_path -> Dir_path.t -> Label.t -> mutual_inductive
 val make_mind_equiv : module_path -> module_path -> Dir_path.t 
-  -> label -> mutual_inductive
+  -> Label.t -> mutual_inductive
 val user_mind : mutual_inductive -> kernel_name
 val canonical_mind : mutual_inductive -> kernel_name
-val repr_mind : mutual_inductive -> module_path * Dir_path.t * label
+val repr_mind : mutual_inductive -> module_path * Dir_path.t * Label.t
 val eq_mind : mutual_inductive -> mutual_inductive -> bool
 
 val string_of_mind : mutual_inductive -> string
-val mind_label : mutual_inductive -> label
+val mind_label : mutual_inductive -> Label.t
 val mind_modpath : mutual_inductive -> module_path
 val pr_mind : mutual_inductive -> Pp.std_ppcmds
 val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds
@@ -357,3 +374,26 @@ val string_of_dirpath : dir_path -> string
 
 val initial_dir : Dir_path.t
 (** @deprecated Same as [Dir_path.initial]. *)
+
+(** {5 Labels} *)
+
+type label = Label.t
+(** Alias type *)
+
+val mk_label : string -> label
+(** @deprecated Same as [Label.make]. *)
+
+val string_of_label : label -> string
+(** @deprecated Same as [Label.to_string]. *)
+
+val pr_label : label -> Pp.std_ppcmds
+(** @deprecated Same as [Label.print]. *)
+
+val label_of_id : Id.t -> label
+(** @deprecated Same as [Label.of_id]. *)
+
+val id_of_label : label -> Id.t
+(** @deprecated Same as [Label.to_id]. *)
+
+val eq_label : label -> label -> bool
+(** @deprecated Same as [Label.equal]. *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index c7bc76e579..8230479744 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -80,7 +80,7 @@ type modvariant =
 
 type module_info =
     {modpath : module_path;
-     label : label;
+     label : Label.t;
      variant : modvariant;
      resolver : delta_resolver;
      resolver_of_param : delta_resolver;}
@@ -96,8 +96,8 @@ type safe_environment =
     { old : safe_environment;
       env : env;
       modinfo : module_info;
-      modlabels : Labset.t;
-      objlabels : Labset.t;
+      modlabels : Label.Set.t;
+      objlabels : Label.Set.t;
       revstruct : structure_body;
       univ : Univ.constraints;
       engagement : engagement option;
@@ -105,8 +105,8 @@ type safe_environment =
       loads : (module_path * module_body) list;
       local_retroknowledge : Retroknowledge.action list}
 
-let exists_modlabel l senv = Labset.mem l senv.modlabels
-let exists_objlabel l senv = Labset.mem l senv.objlabels
+let exists_modlabel l senv = Label.Set.mem l senv.modlabels
+let exists_objlabel l senv = Label.Set.mem l senv.objlabels
 
 let check_modlabel l senv =
   if exists_modlabel l senv then error_existing_label l
@@ -114,12 +114,12 @@ let check_objlabel l senv =
   if exists_objlabel l senv then error_existing_label l
 
 let check_objlabels ls senv =
-  Labset.iter (fun l -> check_objlabel l senv) ls
+  Label.Set.iter (fun l -> check_objlabel l senv) ls
 
 let labels_of_mib mib =
   let add,get =
-    let labels = ref Labset.empty in
-    (fun id -> labels := Labset.add (label_of_id id) !labels),
+    let labels = ref Label.Set.empty in
+    (fun id -> labels := Label.Set.add (Label.of_id id) !labels),
     (fun () -> !labels)
   in
   let visit_mip mip =
@@ -135,12 +135,12 @@ let rec empty_environment =
     env = empty_env;
     modinfo = {
       modpath = initial_path;
-      label = mk_label "_";
+      label = Label.make "_";
       variant = NONE;
       resolver = empty_delta_resolver;
       resolver_of_param = empty_delta_resolver};
-    modlabels = Labset.empty;
-    objlabels = Labset.empty;
+    modlabels = Label.Set.empty;
+    objlabels = Label.Set.empty;
     revstruct = [];
     univ = Univ.empty_constraint;
     engagement = None;
@@ -175,11 +175,11 @@ let add_field ((l,sfb) as field) gn senv =
   let mlabs,olabs = match sfb with
     | SFBmind mib ->
       let l = labels_of_mib mib in
-      check_objlabels l senv; (Labset.empty,l)
+      check_objlabels l senv; (Label.Set.empty,l)
     | SFBconst _ ->
-      check_objlabel l senv; (Labset.empty, Labset.singleton l)
+      check_objlabel l senv; (Label.Set.empty, Label.Set.singleton l)
     | SFBmodule _ | SFBmodtype _ ->
-      check_modlabel l senv; (Labset.singleton l, Labset.empty)
+      check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
   in
   let senv = add_constraints (constraints_of_sfb sfb) senv in
   let env' = match sfb, gn with
@@ -191,8 +191,8 @@ let add_field ((l,sfb) as field) gn senv =
   in
   { senv with
     env = env';
-    modlabels = Labset.union mlabs senv.modlabels;
-    objlabels = Labset.union olabs senv.objlabels;
+    modlabels = Label.Set.union mlabs senv.modlabels;
+    objlabels = Label.Set.union olabs senv.objlabels;
     revstruct = field :: senv.revstruct }
 
 (* Applying a certain function to the resolver of a safe environment *)
@@ -291,7 +291,7 @@ let add_mind dir l mie senv =
   | _ -> ()
   in
   let id = (List.nth mie.mind_entry_inds 0).mind_entry_typename in
-  if not (eq_label l (label_of_id id)) then
+  if not (Label.equal l (Label.of_id id)) then
     anomaly ("the label of inductive packet and its first inductive"^
 	     " type do not match");
   let kn = make_mind senv.modinfo.modpath dir l in
@@ -339,8 +339,8 @@ let start_module l senv =
    mp, { old = senv;
 	 env = senv.env;
 	 modinfo = modinfo;
-	 modlabels = Labset.empty;
-	 objlabels = Labset.empty;
+	 modlabels = Label.Set.empty;
+	 objlabels = Label.Set.empty;
 	 revstruct = [];
          univ = Univ.empty_constraint;
          engagement = None;
@@ -361,7 +361,7 @@ let end_module l restype senv =
       | NONE | LIBRARY _ | SIG _ -> error_no_module_to_end ()
       | STRUCT params -> params, (List.length params > 0)
   in
-  if not (eq_label l modinfo.label) then error_incompatible_labels l modinfo.label;
+  if not (Label.equal l modinfo.label) then error_incompatible_labels l modinfo.label;
   if not (empty_context senv.env) then error_non_empty_local_context None;
   let functorize_struct tb =
     List.fold_left
@@ -424,7 +424,7 @@ let end_module l restype senv =
     mp,resolver,{ old = oldsenv.old;
 		  env = newenv;
 		  modinfo = modinfo;
-		  modlabels = Labset.add l oldsenv.modlabels;
+		  modlabels = Label.Set.add l oldsenv.modlabels;
 		  objlabels = oldsenv.objlabels;
 		  revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
 		  univ = Univ.union_constraints senv'.univ oldsenv.univ;
@@ -547,8 +547,8 @@ let start_modtype l senv =
   mp, { old = senv;
 	env = senv.env;
 	modinfo = modinfo;
-	modlabels = Labset.empty;
-	objlabels = Labset.empty;
+	modlabels = Label.Set.empty;
+	objlabels = Label.Set.empty;
 	revstruct = [];
         univ = Univ.empty_constraint;
         engagement = None;
@@ -565,7 +565,7 @@ let end_modtype l senv =
       | LIBRARY _ | NONE | STRUCT _ -> error_no_modtype_to_end ()
       | SIG params -> params
   in
-  if not (eq_label l modinfo.label) then error_incompatible_labels l modinfo.label;
+  if not (Label.equal l modinfo.label) then error_incompatible_labels l modinfo.label;
   if not (empty_context senv.env) then error_non_empty_local_context None;
   let auto_tb =
      SEBstruct (List.rev senv.revstruct)
@@ -599,7 +599,7 @@ let end_modtype l senv =
     mp, { old = oldsenv.old;
 	  env = newenv;
 	  modinfo = oldsenv.modinfo;
-	  modlabels = Labset.add l oldsenv.modlabels;
+	  modlabels = Label.Set.add l oldsenv.modlabels;
 	  objlabels = oldsenv.objlabels;
 	  revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
           univ = Univ.union_constraints senv.univ oldsenv.univ;
@@ -646,7 +646,7 @@ let start_library dir senv =
     match (Dir_path.repr dir) with
 	[] -> anomaly "Empty dirpath in Safe_typing.start_library"
       | hd::tl ->
-	  Dir_path.make tl, label_of_id hd
+	  Dir_path.make tl, Label.of_id hd
   in
   let mp = MPfile dir in
   let modinfo = {modpath = mp;
@@ -658,8 +658,8 @@ let start_library dir senv =
   mp, { old = senv;
 	env = senv.env;
 	modinfo = modinfo;
-	modlabels = Labset.empty;
-	objlabels = Labset.empty;
+	modlabels = Label.Set.empty;
+	objlabels = Label.Set.empty;
 	revstruct = [];
         univ = Univ.empty_constraint;
         engagement = None;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index bfcc3b8a9a..0add7109aa 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -43,22 +43,22 @@ type global_declaration =
   | GlobalRecipe of Cooking.recipe
 
 val add_constant :
-  Dir_path.t -> label -> global_declaration -> safe_environment ->
+  Dir_path.t -> Label.t -> global_declaration -> safe_environment ->
       constant * safe_environment
 
 (** Adding an inductive type *)
 val add_mind :
-  Dir_path.t -> label -> mutual_inductive_entry -> safe_environment ->
+  Dir_path.t -> Label.t -> mutual_inductive_entry -> safe_environment ->
     mutual_inductive * safe_environment
 
 (** Adding a module *)
 val add_module :
-  label -> module_entry -> inline -> safe_environment
+  Label.t -> module_entry -> inline -> safe_environment
     -> module_path * delta_resolver * safe_environment
 
 (** Adding a module type *)
 val add_modtype :
-  label -> module_struct_entry -> inline -> safe_environment
+  Label.t -> module_struct_entry -> inline -> safe_environment
     -> module_path * safe_environment
 
 (** Adding universe constraints *)
@@ -72,20 +72,20 @@ val set_engagement : engagement -> safe_environment -> safe_environment
 (** {6 Interactive module functions } *)
 
 val start_module :
-  label -> safe_environment -> module_path * safe_environment
+  Label.t -> safe_environment -> module_path * safe_environment
 
 val end_module :
-  label -> (module_struct_entry * inline) option
+  Label.t -> (module_struct_entry * inline) option
       -> safe_environment -> module_path * delta_resolver * safe_environment 
 
 val add_module_parameter :
   mod_bound_id -> module_struct_entry -> inline -> safe_environment -> delta_resolver * safe_environment
 
 val start_modtype :
-  label -> safe_environment -> module_path * safe_environment
+  Label.t -> safe_environment -> module_path * safe_environment
 
 val end_modtype :
-  label -> safe_environment -> module_path * safe_environment
+  Label.t -> safe_environment -> module_path * safe_environment
 
 val add_include :
   module_struct_entry -> bool -> inline -> safe_environment ->
@@ -138,7 +138,7 @@ val typing : safe_environment -> constr -> judgment
 
 (** {7 Query } *)
 
-val exists_objlabel : label -> safe_environment -> bool
+val exists_objlabel : Label.t -> safe_environment -> bool
 
 (*spiwack: safe retroknowledge functionalities *)
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index dbc5b01f19..c15681b043 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -45,36 +45,36 @@ let add_mib_nameobjects mp l mib map =
     let map =
       Array.fold_right_i
       (fun i id map ->
-        Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map)
+        Label.Map.add (Label.of_id id) (IndConstr((ip,i+1), mib)) map)
       oib.mind_consnames
       map
     in
-      Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map
+      Label.Map.add (Label.of_id oib.mind_typename) (IndType (ip, mib)) map
   in
   Array.fold_right_i add_mip_nameobjects mib.mind_packets map
 
 
 (* creates (namedobject/namedmodule) map for the whole signature *)
 
-type labmap = { objs : namedobject Labmap.t; mods : namedmodule Labmap.t }
+type labmap = { objs : namedobject Label.Map.t; mods : namedmodule Label.Map.t }
 
-let empty_labmap = { objs = Labmap.empty; mods = Labmap.empty }
+let empty_labmap = { objs = Label.Map.empty; mods = Label.Map.empty }
 
 let get_obj mp map l =
-  try Labmap.find l map.objs
+  try Label.Map.find l map.objs
   with Not_found -> error_no_such_label_sub l (string_of_mp mp)
 
 let get_mod mp map l =
-  try Labmap.find l map.mods
+  try Label.Map.find l map.mods
   with Not_found -> error_no_such_label_sub l (string_of_mp mp)
 
 let make_labmap mp list =
   let add_one (l,e) map =
    match e with
-    | SFBconst cb -> { map with objs = Labmap.add l (Constant cb) map.objs }
+    | SFBconst cb -> { map with objs = Label.Map.add l (Constant cb) map.objs }
     | SFBmind mib -> { map with objs = add_mib_nameobjects mp l mib map.objs }
-    | SFBmodule mb -> { map with mods = Labmap.add l (Module mb) map.mods }
-    | SFBmodtype mtb -> { map with mods = Labmap.add l (Modtype mtb) map.mods }
+    | SFBmodule mb -> { map with mods = Label.Map.add l (Module mb) map.mods }
+    | SFBmodtype mtb -> { map with mods = Label.Map.add l (Modtype mtb) map.mods }
   in
   List.fold_right add_one list empty_labmap