Modulification of Label

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

22 files changed, 51 insertions, 51 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index bd5e2291a..d8e489be7 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 9ddd0f2af..0fd3e7bb7 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 754016715..7f5ad4f66 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 b892ae57a..5ab3647d6 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 14a30ae79..104a4c865 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 bcdee5954..dba77b923 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 9746c39e4..0ed6a2855 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 7742dd783..fbd3fd4ea 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 a54121139..74728f412 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 2cf3c475e..b69715fc9 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 *)
 
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 455f3539b..4c3c48915 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -83,7 +83,7 @@ let string_of_R_constant kn =
     | MPfile dir, sec_dir, id when
 	sec_dir = Dir_path.empty &&
 	Dir_path.to_string dir = "Coq.Reals.Rdefinitions"
-	-> string_of_label id
+	-> Label.to_string id
     | _ -> "constant_not_of_R"
 
 let rec string_of_R_constr c =
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ca73799c1..9c895e6a9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -966,7 +966,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     (Typeops.type_of_constant_type (Global.env()) f_def.const_type) in
   let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in
   let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in
-  let f_id = id_of_label (con_label (destConst f)) in
+  let f_id = Label.to_id (con_label (destConst f)) in
   let prove_replacement =
     tclTHENSEQ
       [
@@ -1000,7 +1000,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
       let finfos = find_Function_infos (destConst f) in
       mkConst (Option.get finfos.equation_lemma)
     with (Not_found | Option.IsNone as e) ->
-      let f_id = id_of_label (con_label (destConst f)) in
+      let f_id = Label.to_id (con_label (destConst f)) in
       (*i The next call to mk_equation_id is valid since we will construct the lemma
 	Ensures by: obvious
 	i*)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1d30ce9a6..9678fb547 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -322,14 +322,14 @@ let generate_functional_principle
     match new_princ_name with
       | Some (id) -> id,id
       | None ->
-	  let id_of_f = id_of_label (con_label f) in
+	  let id_of_f = Label.to_id (con_label f) in
 	  id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort)
   in
   let names = ref [new_princ_name] in
   let hook new_principle_type _ _  =
     if sorts = None
     then
-      (*     let id_of_f = id_of_label (con_label f) in *)
+      (*     let id_of_f = Label.to_id (con_label f) in *)
       let register_with_sort fam_sort =
 	let s = Termops.new_sort_in_family fam_sort in
 	let name = Indrec.make_elimination_ident base_new_princ_name fam_sort in
@@ -390,7 +390,7 @@ let get_funs_constant mp dp =
 	    (fun i na ->
 	       match na with
 		 | Name id ->
-		     let const = make_con mp dp (label_of_id id) in
+		     let const = make_con mp dp (Label.of_id id) in
 		     const,i
 		 | Anonymous ->
 		     anomaly "Anonymous fix"
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 3dfce8bf4..6c3b009f8 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -58,7 +58,7 @@ let functional_induction with_clean c princl pat =
 			  (or f_rec, f_rect) i*)
 			let princ_name =
 			  Indrec.make_elimination_ident
-			    (id_of_label (con_label c'))
+			    (Label.to_id (con_label c'))
 			    (Tacticals.elimination_sort_of_goal g)
 			in
 			try
@@ -810,14 +810,14 @@ let make_graph (f_ref:global_reference) =
 		 in
 		 l
 	     | _ ->
-		 let id = id_of_label (con_label c) in
+		 let id = Label.to_id (con_label c) in
 		 [((Loc.ghost,id),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]]
 	 in
 	 do_generate_principle error_error false false expr_list;
 	 (* We register the infos *)
 	 let mp,dp,_ = repr_con c in
 	 List.iter
-	   (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (label_of_id id)))
+	   (fun (((_,id),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id)))
 	   expr_list);
   Dumpglob.continue ()
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 5942e11b4..dfbfdce3a 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -408,7 +408,7 @@ let update_Function finfo =
 
 
 let add_Function is_general f =
-  let f_id = id_of_label (con_label f) in
+  let f_id = Label.to_id (con_label f) in
   let equation_lemma = find_or_none (mk_equation_id f_id)
   and correctness_lemma = find_or_none (mk_correct_id f_id)
   and completeness_lemma = find_or_none (mk_complete_id f_id)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 4a466175f..eed421159 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -179,7 +179,7 @@ let find_induction_principle f =
 (*     let fname =  *)
 (*       match kind_of_term f with  *)
 (* 	| Const c' ->  *)
-(* 	    id_of_label (con_label c')  *)
+(* 	    Label.to_id (con_label c')  *)
 (* 	| _ -> error "Must be used with a function"  *)
 (*     in *)
 
@@ -1049,7 +1049,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     in
     Array.iteri
       (fun i f_as_constant ->
-	 let f_id = id_of_label (con_label f_as_constant) in
+	 let f_id = Label.to_id (con_label f_as_constant) in
 	 (*i The next call to mk_correct_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	 i*)
@@ -1100,7 +1100,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     in
     Array.iteri
       (fun i f_as_constant ->
-	 let f_id = id_of_label (con_label f_as_constant) in
+	 let f_id = Label.to_id (con_label f_as_constant) in
 	 (*i The next call to mk_complete_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	   i*)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 68c5e16ae..7b77afd07 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -73,7 +73,7 @@ let def_of_const t =
 	     | _ -> assert false)
        with _ ->
 	 anomaly ("Cannot find definition of constant "^
-		    (Id.to_string (id_of_label (con_label sp))))
+		    (Id.to_string (Label.to_id (con_label sp))))
       )
      |_ -> assert false
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index d02d26007..c89e06f7c 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -246,11 +246,11 @@ let my_constant c =
 let new_ring_path =
   Dir_path.make (List.map Id.of_string ["Ring_tac";plugin_dir;"Coq"])
 let ltac s =
-  lazy(make_kn (MPfile new_ring_path) (Dir_path.make []) (mk_label s))
+  lazy(make_kn (MPfile new_ring_path) (Dir_path.make []) (Label.make s))
 let znew_ring_path =
   Dir_path.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"])
 let zltac s =
-  lazy(make_kn (MPfile znew_ring_path) (Dir_path.make []) (mk_label s))
+  lazy(make_kn (MPfile znew_ring_path) (Dir_path.make []) (Label.make s))
 
 let mk_cst l s = lazy (Coqlib.gen_constant "newring" l s);;
 let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;;
@@ -829,7 +829,7 @@ let new_field_path =
   Dir_path.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"])
 
 let field_ltac s =
-  lazy(make_kn (MPfile new_field_path) (Dir_path.make []) (mk_label s))
+  lazy(make_kn (MPfile new_field_path) (Dir_path.make []) (Label.make s))
 
 
 let _ = add_map "field"
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index d6b9f73d5..643dacbab 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -17,10 +17,10 @@ open Glob_term
 let make_dir l = Names.Dir_path.make (List.map Names.Id.of_string (List.rev l))
 let make_path dir id = Libnames.make_path (make_dir dir) (Names.Id.of_string id)
 
-let make_mind mp id = Names.make_mind mp Names.Dir_path.empty (Names.mk_label id)
+let make_mind mp id = Names.make_mind mp Names.Dir_path.empty (Names.Label.make id)
 let make_mind_mpfile dir id = make_mind (Names.MPfile (make_dir dir)) id
 let make_mind_mpdot dir modname id =
-  let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.mk_label modname)
+  let mp = Names.MPdot (Names.MPfile (make_dir dir), Names.Label.make modname)
   in make_mind mp id
 
 
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index fb951b35f..4a8436d76 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -128,12 +128,12 @@ let token_list_of_kernel_name tag =
  let module GN = Globnames in
  let id,dir = match tag with
    | Variable kn ->
-       N.id_of_label (N.label kn), Lib.cwd ()
+       N.Label.to_id (N.label kn), Lib.cwd ()
    | Constant con ->
-       N.id_of_label (N.con_label con),
+       N.Label.to_id (N.con_label con),
        Lib.remove_section_part (GN.ConstRef con)
    | Inductive kn ->
-       N.id_of_label (N.mind_label kn),
+       N.Label.to_id (N.mind_label kn),
        Lib.remove_section_part (GN.IndRef (kn,0))
  in
  token_list_of_path dir id (etag_of_tag tag)
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index b4ec85ab7..864f35e80 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -21,7 +21,7 @@ let cprop =
    (N.MPfile
      (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
    (N.Dir_path.make [])
-   (N.mk_label "CProp")
+   (N.Label.make "CProp")
 ;;
 
 let whd_betadeltaiotacprop env _evar_map ty =
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 50309317e..e16f9dd19 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -384,12 +384,12 @@ let print internal glob_ref kind xml_library_root =
        (* this kn is fake since it is not provided by Coq *)
        let kn =
         let (mod_path,dir_path) = Lib.current_prefix () in
-        N.make_kn mod_path dir_path (N.label_of_id id)
+        N.make_kn mod_path dir_path (N.Label.of_id id)
        in
        let (_,body,typ) = G.lookup_named id in
         Cic2acic.Variable kn,mk_variable_obj id body typ
     | Gn.ConstRef kn ->
-       let id = N.id_of_label (N.con_label kn) in
+       let id = N.Label.to_id (N.con_label kn) in
        let cb = G.lookup_constant kn in
        let val0 = D.body_of_constant cb in
        let typ = cb.D.const_type in
@@ -467,7 +467,7 @@ let _ =
          (* I saved in the Pfedit.set_xml_cook_proof callback.          *)
         let fn = filename_of_path xml_library_root (Cic2acic.Constant kn) in
          show_pftreestate internal fn pftreestate
-	  (Names.id_of_label (Names.con_label kn)) ;
+	  (Names.Label.to_id (Names.con_label kn)) ;
          proof_to_export := None)
 ;;