Modulification of identifier

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

9 files changed, 31 insertions, 31 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index ebda3cb76f..6d34b10bc9 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -138,7 +138,7 @@ let pr_opt_type_spc pr = function
 let pr_lident (loc,id) =
   if loc <> Loc.ghost then
     let (b,_) = Loc.unloc loc in
-    pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id)
+    pr_located pr_id (Loc.make_loc (b,b+String.length(Id.to_string id)),id)
   else pr_id id
 
 let pr_lname = function
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 1d7f5f7f57..7343140d22 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -30,9 +30,9 @@ val prec_less : int -> int * Ppextend.parenRelation -> bool
 val pr_tight_coma : unit -> std_ppcmds
 
 val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
-val pr_metaid : identifier -> std_ppcmds
+val pr_metaid : Id.t -> std_ppcmds
 
-val pr_lident : identifier located -> std_ppcmds
+val pr_lident : Id.t located -> std_ppcmds
 val pr_lname : name located -> std_ppcmds
 
 val pr_with_comments : Loc.t -> std_ppcmds -> std_ppcmds
@@ -42,7 +42,7 @@ val pr_sep_com :
   (constr_expr -> std_ppcmds) ->
   constr_expr -> std_ppcmds
 
-val pr_id : identifier -> std_ppcmds
+val pr_id : Id.t -> std_ppcmds
 val pr_name : name -> std_ppcmds
 val pr_qualid : qualid -> std_ppcmds
 val pr_patvar : patvar -> std_ppcmds
@@ -59,7 +59,7 @@ val pr_may_eval :
 val pr_glob_sort : glob_sort -> std_ppcmds
 val pr_guard_annot : (constr_expr -> std_ppcmds) ->
   local_binder list ->
-  ('a * Names.identifier) option * recursion_order_expr ->
+  ('a * Names.Id.t) option * recursion_order_expr ->
   std_ppcmds
 
 val pr_binders : local_binder list -> std_ppcmds
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 5c65f55b50..5b33f89cb3 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -24,7 +24,7 @@ open Genredexpr
 open Ppconstr
 open Printer
 
-let pr_global x = Nametab.pr_global_env Idset.empty x
+let pr_global x = Nametab.pr_global_env Id.Set.empty x
 
 type grammar_terminals = string option list
 
@@ -606,7 +606,7 @@ let pr_fix_tac (id,n,c) =
           match List.chop (n-1) nal with
               _, (_,Name id) :: _ -> id, (nal,ty)::bll
             | bef, (loc,Anonymous) :: aft ->
-                let id = next_ident_away (id_of_string"y") avoid in
+                let id = next_ident_away (Id.of_string"y") avoid in
                 id, ((bef@(loc,Name id)::aft, ty)::bll)
             | _ -> assert false
         else
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 41882acb4b..24b0dc6cde 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -28,11 +28,11 @@ let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr
 let pr_lident (loc,id) =
   if loc <> Loc.ghost then
     let (b,_) = Loc.unloc loc in
-    pr_located pr_id (Loc.make_loc (b,b+String.length(string_of_id id)),id)
+    pr_located pr_id (Loc.make_loc (b,b+String.length(Id.to_string id)),id)
   else pr_id id
 
 let string_of_fqid fqid =
- String.concat "." (List.map string_of_id fqid)
+ String.concat "." (List.map Id.to_string fqid)
 
 let pr_fqid fqid = str (string_of_fqid fqid)
 
@@ -104,8 +104,8 @@ let pr_set_entry_type = function
   | ETBinderList _ | ETConstrList _ -> failwith "Internal entry type"
 
 let strip_meta id =
-  let s = string_of_id id in
-  if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
+  let s = Id.to_string id in
+  if s.[0]='$' then Id.of_string (String.sub s 1 (String.length s - 1))
   else id
 
 let pr_production_item = function
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 1e17a8ab08..dee144b951 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -36,7 +36,7 @@ type object_pr = {
   print_syntactic_def       : kernel_name -> std_ppcmds;
   print_module              : bool -> Names.module_path -> std_ppcmds;
   print_modtype             : module_path -> std_ppcmds;
-  print_named_decl          : identifier * constr option * types -> std_ppcmds;
+  print_named_decl          : Id.t * constr option * types -> std_ppcmds;
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
   print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
   print_typed_value_in_env  : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
@@ -325,9 +325,9 @@ let print_located_qualid ref =
   let module N = Nametab in
   let expand = function
     | TrueGlobal ref ->
-	Term ref, N.shortest_qualid_of_global Idset.empty ref
+	Term ref, N.shortest_qualid_of_global Id.Set.empty ref
     | SynDef kn ->
-	Syntactic kn, N.shortest_qualid_of_syndef Idset.empty kn in
+	Syntactic kn, N.shortest_qualid_of_syndef Id.Set.empty kn in
   match List.map expand (N.locate_extended_all qid) with
     | [] ->
 	let (dir,id) = repr_qualid qid in
@@ -370,7 +370,7 @@ let print_named_assum name typ =
   str "*** [" ++ str name ++ str " : " ++ pr_ltype typ ++ str "]"
 
 let gallina_print_named_decl (id,c,typ) =
-  let s = string_of_id id in
+  let s = Id.to_string id in
   match c with
     | Some body -> print_named_def s body typ
     | None -> print_named_assum s typ
@@ -430,7 +430,7 @@ let gallina_print_constant_with_infos sp =
   with_line_skip (print_name_infos (ConstRef sp))
 
 let gallina_print_syntactic_def kn =
-  let qid = Nametab.shortest_qualid_of_syndef Idset.empty kn
+  let qid = Nametab.shortest_qualid_of_syndef Id.Set.empty kn
   and (vars,a) = Syntax_def.search_syntactic_definition kn in
   let c = Notation_ops.glob_constr_of_notation_constr Loc.ghost a in
   hov 2
diff --git a/printing/prettyp.mli b/printing/prettyp.mli
index f9e77bec9f..7a3395f1bf 100644
--- a/printing/prettyp.mli
+++ b/printing/prettyp.mli
@@ -64,7 +64,7 @@ type object_pr = {
   print_syntactic_def       : kernel_name -> std_ppcmds;
   print_module              : bool -> Names.module_path -> std_ppcmds;
   print_modtype             : module_path -> std_ppcmds;
-  print_named_decl          : identifier * constr option * types -> std_ppcmds;
+  print_named_decl          : Id.t * constr option * types -> std_ppcmds;
   print_library_entry       : bool -> (object_name * Lib.node) -> std_ppcmds option;
   print_context             : bool -> int option -> Lib.library_segment -> std_ppcmds;
   print_typed_value_in_env  : Environ.env -> Term.constr * Term.types -> Pp.std_ppcmds;
diff --git a/printing/printer.ml b/printing/printer.ml
index 4f09460d8d..a3e2fd9c2b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -92,12 +92,12 @@ let pr_glob_constr_env env c =
   pr_constr_expr (extern_glob_constr (Termops.vars_of_env env) c)
 
 let pr_lglob_constr c =
-  pr_lconstr_expr (extern_glob_constr Idset.empty c)
+  pr_lconstr_expr (extern_glob_constr Id.Set.empty c)
 let pr_glob_constr c =
-  pr_constr_expr (extern_glob_constr Idset.empty c)
+  pr_constr_expr (extern_glob_constr Id.Set.empty c)
 
 let pr_cases_pattern t =
-  pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
+  pr_cases_pattern_expr (extern_cases_pattern Id.Set.empty t)
 
 let pr_lconstr_pattern_env env c =
   pr_lconstr_pattern_expr (extern_constr_pattern (Termops.names_of_rel_context env) c)
@@ -124,7 +124,7 @@ let pr_univ_cstr (c:Univ.constraints) =
 (* Global references *)
 
 let pr_global_env = pr_global_env
-let pr_global = pr_global_env Idset.empty
+let pr_global = pr_global_env Id.Set.empty
 
 let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst)
 let pr_existential env ev = pr_lconstr_env env (mkEvar ev)
@@ -135,7 +135,7 @@ let pr_evaluable_reference ref =
   pr_global (Tacred.global_of_evaluable_reference ref)
 
 (*let pr_glob_constr t =
-  pr_lconstr (Constrextern.extern_glob_constr Idset.empty t)*)
+  pr_lconstr (Constrextern.extern_glob_constr Id.Set.empty t)*)
 
 (*open Pattern
 
@@ -257,7 +257,7 @@ let pr_predicate pr_elt (b, elts) =
       if elts = [] then str"none" else pr_elts
 
 let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p)
-let pr_idpred p = pr_predicate Nameops.pr_id (Idpred.elements p)
+let pr_idpred p = pr_predicate Nameops.pr_id (Id.Pred.elements p)
 
 let pr_transparent_state (ids, csts) =
   hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++
@@ -596,7 +596,7 @@ let pr_assumptionset env s =
       let (v, a, o, tr) = accu in
       match t with
       | Variable id ->
-        let var = str (string_of_id id) ++ str " : " ++ pr_ltype typ in
+        let var = str (Id.to_string id) ++ str " : " ++ pr_ltype typ in
         (var :: v, a, o, tr)
       | Axiom kn ->
         let ax = safe_pr_constant env kn ++ safe_pr_ltype typ in
@@ -688,10 +688,10 @@ let get_fields =
   let rec prodec_rec l subst c =
     match kind_of_term c with
     | Prod (na,t,c) ->
-	let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
+	let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in
 	prodec_rec ((id,true,substl subst t)::l) (mkVar id::subst) c
     | LetIn (na,b,_,c) ->
-	let id = match na with Name id -> id | Anonymous -> id_of_string "_" in
+	let id = match na with Name id -> id | Anonymous -> Id.of_string "_" in
 	prodec_rec ((id,false,substl subst b)::l) (mkVar id::subst) c
     | _               -> List.rev l
   in
diff --git a/printing/printer.mli b/printing/printer.mli
index 47dfa32b9c..2340b310f5 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -76,7 +76,7 @@ val pr_univ_cstr           : Univ.constraints -> std_ppcmds
 
 (** Printing global references using names as short as possible *)
 
-val pr_global_env          : Idset.t -> global_reference -> std_ppcmds
+val pr_global_env          : Id.Set.t -> global_reference -> std_ppcmds
 val pr_global              : global_reference -> std_ppcmds
 
 val pr_constant            : env -> constant -> std_ppcmds
@@ -102,7 +102,7 @@ val pr_context_of          : env -> std_ppcmds
 
 val pr_predicate           : ('a -> std_ppcmds) -> (bool * 'a list) -> std_ppcmds
 val pr_cpred               : Cpred.t -> std_ppcmds
-val pr_idpred              : Idpred.t -> std_ppcmds
+val pr_idpred              : Id.Pred.t -> std_ppcmds
 val pr_transparent_state   : transparent_state -> std_ppcmds
 
 (** Proofs *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index b5a633cd20..44c2466616 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -70,7 +70,7 @@ let print_kn locals kn =
 	    Not_found -> print_modpath locals kn
 
 let nametab_register_dir mp =
-  let id = id_of_string "FAKETOP" in
+  let id = Id.of_string "FAKETOP" in
   let fp = Libnames.make_path empty_dirpath id in
   let dir = make_dirpath [id] in
   Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,empty_dirpath)));
@@ -175,11 +175,11 @@ let rec print_modtype env mp locals mty =
 		 prlist_with_sep spc (print_modpath locals) mapp ++ str")")
   | SEBwith(seb,With_definition_body(idl,cb))->
       let env' = None in (* TODO: build a proper environment if env <> None *)
-      let s = (String.concat "." (List.map string_of_id idl)) in
+      let s = (String.concat "." (List.map Id.to_string idl)) in
       hov 2 (print_modtype env' mp locals seb ++ spc() ++ str "with" ++ spc() ++
 	       str "Definition"++ spc() ++ str s ++ spc() ++  str ":="++ spc())
   | SEBwith(seb,With_module_body(idl,mp))->
-      let s =(String.concat "." (List.map string_of_id idl)) in
+      let s =(String.concat "." (List.map Id.to_string idl)) in
       hov 2 (print_modtype env mp locals seb ++ spc() ++ str "with" ++ spc() ++
 	       str "Module"++ spc() ++ str s ++ spc() ++ str ":="++ spc())