Modulification of Label

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

10 files changed, 25 insertions, 25 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index bd5e2291ac..d8e489be74 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -255,7 +255,7 @@ let params_ren_add, params_ren_mem =
 
 type visible_layer = { mp : module_path;
 		       params : module_path list;
-		       content : ((kind*string),label) Hashtbl.t }
+		       content : ((kind*string),Label.t) Hashtbl.t }
 
 let pop_visible, push_visible, get_visible =
   let vis = ref [] in
@@ -321,7 +321,7 @@ let modfstlev_rename =
   let add_prefixes,get_prefixes,_ = mktable true in
   fun l ->
     let coqid = Id.of_string "Coq" in
-    let id = id_of_label l in
+    let id = Label.to_id l in
     try
       let coqset = get_prefixes id in
       let nextcoq = next_ident_away coqid coqset in
@@ -341,7 +341,7 @@ let rec mp_renaming_fun mp = match mp with
   | MPdot (mp,l) ->
       let lmp = mp_renaming mp in
       if lmp = [""] then (modfstlev_rename l)::lmp
-      else (modular_rename Mod (id_of_label l))::lmp
+      else (modular_rename Mod (Label.to_id l))::lmp
   | MPbound mbid ->
       let s = modular_rename Mod (id_of_mbid mbid) in
       if not (params_ren_mem mp) then [s]
@@ -584,7 +584,7 @@ let pp_module mp =
     the constants are directly turned into chars *)
 
 let mk_ind path s =
-  make_mind (MPfile (dirpath_of_string path)) Dir_path.empty (mk_label s)
+  make_mind (MPfile (dirpath_of_string path)) Dir_path.empty (Label.make s)
 
 let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
 
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 9ddd0f2aff..0fd3e7bb7b 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -63,7 +63,7 @@ val top_visible_mp : unit -> module_path
 val push_visible : module_path -> module_path list -> unit
 val pop_visible : unit -> unit
 
-val check_duplicate : module_path -> label -> string
+val check_duplicate : module_path -> Label.t -> string
 
 type reset_kind = AllButExternal | Everything
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7540167158..7f5ad4f660 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -208,7 +208,7 @@ let env_for_mtb_with_def env mp seb idl =
     | SEBstruct(sig_b) -> sig_b
     | _ -> assert false
   in
-  let l = label_of_id (List.hd idl) in
+  let l = Label.of_id (List.hd idl) in
   let spot = function (l',SFBconst _) -> l = l' | _ -> false in
   let before = fst (List.split_when spot sig_b) in
   Modops.add_signature mp before empty_delta_resolver env
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b892ae57a5..5ab3647d67 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -450,7 +450,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | Anonymous::l, typ::typs ->
 	      None :: (select_fields l typs)
 	  | Name id::l, typ::typs ->
-	      let knp = make_con mp d (label_of_id id) in
+	      let knp = make_con mp d (Label.of_id id) in
 	      (* Is it safe to use [id] for projections [foo.id] ? *)
 	      if List.for_all ((=) Keep) (type2signature env typ)
 	      then projs := Cset.add knp !projs;
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 14a30ae796..104a4c8657 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -157,7 +157,7 @@ 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
 
-and ml_module_sig = (label * ml_specif) list
+and ml_module_sig = (Label.t * ml_specif) list
 
 type ml_structure_elem =
   | SEdecl of ml_decl
@@ -170,7 +170,7 @@ and ml_module_expr =
   | MEstruct of module_path * ml_module_structure
   | MEapply of ml_module_expr * ml_module_expr
 
-and ml_module_structure = (label * ml_structure_elem) list
+and ml_module_structure = (Label.t * ml_structure_elem) list
 
 and ml_module =
     { ml_mod_expr : ml_module_expr;
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index bcdee5954d..dba77b923a 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1306,7 +1306,7 @@ let inline_test r t =
 let con_of_string s =
   let null = Dir_path.empty in
   match Dir_path.repr (dirpath_of_string s) with
-    | id :: d -> make_con (MPfile (Dir_path.make d)) null (label_of_id id)
+    | id :: d -> make_con (MPfile (Dir_path.make d)) null (Label.of_id id)
     | [] -> assert false
 
 let manual_inline_set =
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 9746c39e49..0ed6a28558 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -32,14 +32,14 @@ let se_iter do_decl do_spec do_mp =
 	let mp_mt = msid_of_mt mt in
 	let l',idl' = List.sep_last idl in
 	let mp_w =
-	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
+	  List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
 	in
-	let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l')) in
+	let r = ConstRef (make_con mp_w Dir_path.empty (Label.of_id l')) in
 	mt_iter mt; do_decl (Dtype(r,l,t))
     | MTwith (mt,ML_With_module(idl,mp))->
         let mp_mt = msid_of_mt mt in
         let mp_w =
-	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl
+	  List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl
 	in
 	mt_iter mt; do_mp mp_w; do_mp mp
     | MTsig (_, sign) -> List.iter spec_iter sign
@@ -249,7 +249,7 @@ let dfix_to_mlfix rv av i =
 	(try MLrel (n + (Refmap'.find refe s)) with Not_found -> t)
     | _ -> ast_map_lift subst n t
   in
-  let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in
+  let ids = Array.map (fun r -> Label.to_id (label_of_r r)) rv in
   let c = Array.map (subst 0) av
   in MLfix(i, ids, c)
 
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 7742dd7834..fbd3fd4ea8 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -648,9 +648,9 @@ and pp_module_type params = function
       let mp_mt = msid_of_mt mt in
       let l,idl' = List.sep_last idl in
       let mp_w =
-	List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
+	List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
       in
-      let r = ConstRef (make_con mp_w Dir_path.empty (label_of_id l)) in
+      let r = ConstRef (make_con mp_w Dir_path.empty (Label.of_id l)) in
       push_visible mp_mt [];
       let pp_w = str " with type " ++ ids ++ pp_global Type r in
       pop_visible();
@@ -658,7 +658,7 @@ and pp_module_type params = function
   | MTwith(mt,ML_With_module(idl,mp)) ->
       let mp_mt = msid_of_mt mt in
       let mp_w =
-	List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl
+	List.fold_left (fun mp id -> MPdot(mp,Label.of_id id)) mp_mt idl
       in
       push_visible mp_mt [];
       let pp_w = str " with module " ++ pp_modname mp_w in
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index a541211391..74728f4124 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -175,7 +175,7 @@ let add_recursors env kn =
     make_con_equiv
       (modpath (user_mind kn))
       (modpath (canonical_mind kn))
-      Dir_path.empty (label_of_id id)
+      Dir_path.empty (Label.of_id id)
   in
   let mib = Environ.lookup_mind kn env in
   Array.iter
@@ -245,8 +245,8 @@ let safe_basename_of_global r =
       anomaly "Inductive object unknown to extraction and not globally visible"
   in
   match r with
-    | ConstRef kn -> id_of_label (con_label kn)
-    | IndRef (kn,0) -> id_of_label (mind_label kn)
+    | ConstRef kn -> Label.to_id (con_label kn)
+    | IndRef (kn,0) -> Label.to_id (mind_label kn)
     | IndRef (kn,i) ->
       (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename
        with Not_found -> last_chance r)
@@ -268,7 +268,7 @@ let safe_pr_long_global r =
   with _ -> match r with
     | ConstRef kn ->
 	let mp,_,l = repr_con kn in
-	str ((string_of_mp mp)^"."^(string_of_label l))
+	str ((string_of_mp mp)^"."^(Label.to_string l))
     | _ -> assert false
 
 let pr_long_mp mp =
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 2cf3c475ed..b69715fc93 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -46,9 +46,9 @@ 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 * Dir_path.t * label
+val repr_of_r : global_reference -> module_path * Dir_path.t * Label.t
 val modpath_of_r : global_reference -> module_path
-val label_of_r : global_reference -> label
+val label_of_r : global_reference -> Label.t
 val current_toplevel : unit -> module_path
 val base_mp : module_path -> module_path
 val is_modfile : module_path -> bool
@@ -61,8 +61,8 @@ val mp_length : module_path -> int
 val prefixes_mp : module_path -> MPset.t
 val common_prefix_from_list :
   module_path -> module_path list -> module_path option
-val get_nth_label_mp : int -> module_path -> label
-val labels_of_ref : global_reference -> module_path * label list
+val get_nth_label_mp : int -> module_path -> Label.t
+val labels_of_ref : global_reference -> module_path * Label.t list
 
 (*s Some table-related operations *)