Modulification of Label

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

10 files changed, 24 insertions, 24 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index 1f6c8eeeb..84e870499 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -60,12 +60,12 @@ let modcache = ref (MPmap.empty : structure_body MPmap.t)
 
 let rec search_mod_label lab = function
   | [] -> raise Not_found
-  | (l, SFBmodule mb) :: _ when eq_label l lab -> mb
+  | (l, SFBmodule mb) :: _ when Label.equal l lab -> mb
   | _ :: fields -> search_mod_label lab fields
 
 let rec search_cst_label lab = function
   | [] -> raise Not_found
-  | (l, SFBconst cb) :: _ when eq_label l lab -> cb
+  | (l, SFBconst cb) :: _ when Label.equal l lab -> cb
   | _ :: fields -> search_cst_label lab fields
 
 let rec lookup_module_in_impl mp =
diff --git a/library/declare.ml b/library/declare.ml
index 015fc9894..20e5bdddc 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -117,7 +117,7 @@ let open_constant i ((sp,kn),_) =
     Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
 let exists_name id =
-  variable_exists id or Global.exists_objlabel (label_of_id id)
+  variable_exists id or Global.exists_objlabel (Label.of_id id)
 
 let check_exists sp =
   let id = basename sp in
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 10b04c588..763aa5ffd 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -440,7 +440,7 @@ let rec replace_module_object idl (mbids,mp,lib_stack) (mbids2,mp2,objs) mp1 =
       if not (String.equal (object_tag obj) "MODULE") then anomaly "MODULE expected!";
       let substobjs = match idl with
       | [] ->
-        let mp' = MPdot(mp, label_of_id id) in
+        let mp' = MPdot(mp, Label.of_id id) in
         mbids, mp', subst_objects (map_mp mp1 mp' empty_delta_resolver) objs
       | _ ->
         replace_module_object idl (out_module obj) (mbids2,mp2,objs) mp
diff --git a/library/global.ml b/library/global.ml
index c2bd55128..f56cb7d61 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -46,7 +46,7 @@ let push_named_def d =
 
 
 let add_thing add dir id thing =
-  let kn, newenv = add dir (label_of_id id) thing !global_env in
+  let kn, newenv = add dir (Label.of_id id) thing !global_env in
     global_env := newenv;
     kn
 
@@ -56,7 +56,7 @@ let add_modtype x y inl = add_thing (fun _ x y -> add_modtype x y inl) () x y
 
 
 let add_module id me inl =
-  let l = label_of_id id in
+  let l = Label.of_id id in
   let mp,resolve,new_env = add_module l me inl !global_env in
     global_env := new_env;
     mp,resolve
@@ -72,13 +72,13 @@ let add_include me is_module inl =
     resolve
 
 let start_module id =
-  let l = label_of_id id in
+  let l = Label.of_id id in
   let mp,newenv = start_module l !global_env in
     global_env := newenv;
     mp
 
 let end_module fs id mtyo =
-  let l = label_of_id id in
+  let l = Label.of_id id in
   let mp,resolve,newenv = end_module l mtyo !global_env in
     Summary.unfreeze_summaries fs;
     global_env := newenv;
@@ -92,13 +92,13 @@ let add_module_parameter mbid mte inl =
 
 
 let start_modtype id =
-  let l = label_of_id id in
+  let l = Label.of_id id in
   let mp,newenv = start_modtype l !global_env in
     global_env := newenv;
     mp
 
 let end_modtype fs id =
-  let l = label_of_id id in
+  let l = Label.of_id id in
   let kn,newenv = end_modtype l !global_env in
     Summary.unfreeze_summaries fs;
     global_env := newenv;
diff --git a/library/global.mli b/library/global.mli
index dac230a44..d49dd836b 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -87,7 +87,7 @@ val lookup_module    : module_path -> module_body
 val lookup_modtype   : module_path -> module_type_body
 val constant_of_delta_kn : kernel_name -> constant
 val mind_of_delta_kn : kernel_name -> mutual_inductive
-val exists_objlabel  : label -> bool
+val exists_objlabel  : Label.t -> bool
 
 (** Compiled modules *)
 val start_library : Dir_path.t -> module_path
diff --git a/library/globnames.ml b/library/globnames.ml
index efc46a7ac..c37e370a3 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -138,9 +138,9 @@ let constr_of_global_or_constr = function
 
 (** {6 Temporary function to brutally form kernel names from section paths } *)
 
-let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (label_of_id id)
+let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (Label.of_id id)
 
-let encode_con dir id = make_con (MPfile dir) Dir_path.empty (label_of_id id)
+let encode_con dir id = make_con (MPfile dir) Dir_path.empty (Label.of_id id)
 
 let decode_mind kn =
   let rec dir_of_mp = function
@@ -149,18 +149,18 @@ let decode_mind kn =
 	let _,_,dp = repr_mbid mbid in
 	let id = id_of_mbid mbid in
 	  id::(Dir_path.repr dp)
-    | MPdot(mp,l) -> (id_of_label l)::(dir_of_mp mp)
+    | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp)
   in
   let mp,sec_dir,l = repr_mind kn in
     if (Dir_path.repr sec_dir) = [] then
-     (Dir_path.make (dir_of_mp mp)),id_of_label l
+     (Dir_path.make (dir_of_mp mp)),Label.to_id l
     else
       anomaly "Section part should be empty!"
 
 let decode_con kn =
   let mp,sec_dir,l = repr_con kn in
     match mp,(Dir_path.repr sec_dir) with
-	MPfile dir,[] -> (dir,id_of_label l)
+	MPfile dir,[] -> (dir,Label.to_id l)
       | _ , [] -> anomaly "MPfile expected!"
       | _ -> anomaly "Section part should be empty!"
 
diff --git a/library/lib.ml b/library/lib.ml
index ed64b1f40..9ac9b7c71 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -61,7 +61,7 @@ let classify_segment seg =
   let rec clean ((substl,keepl,anticipl) as acc) = function
     | (_,CompilingLibrary _) :: _ | [] -> acc
     | ((sp,kn),Leaf o) :: stk ->
-	let id = Names.id_of_label (Names.label kn) in
+	let id = Names.Label.to_id (Names.label kn) in
 	  (match classify_object o with
 	     | Dispose -> clean acc stk
 	     | Keep o' ->
@@ -136,11 +136,11 @@ let current_prefix () = snd !path_prefix
 
 let make_kn id =
   let mp,dir = current_prefix () in
-    Names.make_kn mp dir (Names.label_of_id id)
+    Names.make_kn mp dir (Names.Label.of_id id)
 
 let make_con id =
   let mp,dir = current_prefix () in
-    Names.make_con mp dir (Names.label_of_id id)
+    Names.make_con mp dir (Names.Label.of_id id)
 
 
 let make_oname id = make_path id, make_kn id
@@ -657,7 +657,7 @@ let rec split_mp mp =
     | Names.MPfile dp -> dp,  Names.Dir_path.empty
     | Names.MPdot (prfx, lbl) ->
 	let mprec, dprec = split_mp prfx in
-	  mprec, Names.Dir_path.make (Names.Id.of_string (Names.string_of_label lbl) :: (Names.Dir_path.repr dprec))
+	  mprec, Names.Dir_path.make (Names.Id.of_string (Names.Label.to_string lbl) :: (Names.Dir_path.repr dprec))
     | Names.MPbound mbid -> let (_, id, dp) = Names.repr_mbid mbid in  library_dp(), Names.Dir_path.make [id]
 
 let split_modpath mp =
@@ -666,7 +666,7 @@ let split_modpath mp =
     | Names.MPbound mbid ->
 	library_dp (), [Names.id_of_mbid mbid]
     | Names.MPdot (mp,l) -> let (mp', lab) = aux mp in
-			      (mp', Names.id_of_label l :: lab)
+			      (mp', Names.Label.to_id l :: lab)
   in
   let (mp, l) = aux mp in
     mp, l
diff --git a/library/libnames.ml b/library/libnames.ml
index 8e026d8c2..7680e5248 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -151,7 +151,7 @@ type object_name = full_path * kernel_name
 type object_prefix = Dir_path.t * (module_path * Dir_path.t)
 
 let make_oname (dirpath,(mp,dir)) id =
-  make_path dirpath id, make_kn mp dir (label_of_id id)
+  make_path dirpath id, make_kn mp dir (Label.of_id id)
 
 (* to this type are mapped Dir_path.t's in the nametab *)
 type global_dir_reference =
diff --git a/library/nameops.ml b/library/nameops.ml
index 361a53d6b..a8803e7a5 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -136,7 +136,7 @@ let name_fold_map f e = function
   | Name id -> let (e,id) = f e id in (e,Name id)
   | Anonymous -> e,Anonymous
 
-let pr_lab l = str (string_of_label l)
+let pr_lab l = str (Label.to_string l)
 
 let default_library = Names.Dir_path.initial (* = ["Top"] *)
 
diff --git a/library/nameops.mli b/library/nameops.mli
index 6e9bde839..0f71d28a1 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -36,7 +36,7 @@ val name_app : (Id.t -> Id.t) -> name -> name
 val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> name -> 'a * name
 
 
-val pr_lab : label -> Pp.std_ppcmds
+val pr_lab : Label.t -> Pp.std_ppcmds
 
 (** some preset paths *)