Modulification of identifier

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

4 files changed, 41 insertions, 41 deletions

diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml
index 653c2b7bd..3e2c8ade7 100644
--- a/plugins/xml/acic.ml
+++ b/plugins/xml/acic.ml
@@ -34,7 +34,7 @@ type 'constr context_entry =
                                (* is not present in the DTD, but is needed   *)
                                (* to use Coq functions during exportation.   *)
 
-type 'constr hypothesis = identifier * 'constr context_entry
+type 'constr hypothesis = Id.t * 'constr context_entry
 type context = constr hypothesis list
 
 type conjecture = existential_key * context * constr
@@ -57,13 +57,13 @@ type obj =
     inductiveType list *                           (* inductive types ,      *)
     params * int                                   (*  parameters,n ind. pars*)
 and inductiveType =
- identifier * bool * constr *                 (* typename, inductive, arity *)
+ Id.t * bool * constr *                 (* typename, inductive, arity *)
   constructor list                            (*  constructors              *)
 and constructor =
- identifier * constr                          (* id, type *)
+ Id.t * constr                          (* id, type *)
 
 type aconstr =
-  | ARel       of id * int * id * identifier
+  | ARel       of id * int * id * Id.t
   | AVar       of id * uri
   | AEvar      of id * existential_key * aconstr list
   | ASort      of id * sorts
@@ -79,9 +79,9 @@ type aconstr =
   | AFix       of id * int * ainductivefun list
   | ACoFix     of id * int * acoinductivefun list
 and ainductivefun =
- id * identifier * int * aconstr * aconstr
+ id * Id.t * int * aconstr * aconstr
 and acoinductivefun =
- id * identifier * aconstr * aconstr
+ id * Id.t * aconstr * aconstr
 and explicit_named_substitution = id option * (uri * aconstr) list
 
 type acontext = (id * aconstr hypothesis) list
@@ -102,7 +102,7 @@ type aobj =
     anninductiveType list *                        (* inductive types ,      *)
     params * int                                   (*  parameters,n ind. pars*)
 and anninductiveType =
- id * identifier * bool * aconstr *           (* typename, inductive, arity *)
+ id * Id.t * bool * aconstr *           (* typename, inductive, arity *)
   annconstructor list                         (*  constructors              *)
 and annconstructor =
- identifier * aconstr                         (* id, type *)
+ Id.t * aconstr                         (* id, type *)
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index c03b13b5a..34bb1d51f 100644
--- a/plugins/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.ml4
@@ -37,7 +37,7 @@ let print_term ids_to_inner_sorts =
        A.ARel (id,n,idref,b) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
          X.xml_empty "REL"
-          ["value",(string_of_int n) ; "binder",(N.string_of_id b) ;
+          ["value",(string_of_int n) ; "binder",(N.Id.to_string b) ;
            "id",id ; "idref",idref; "sort",sort]
      | A.AVar (id,uri) ->
         let sort = Hashtbl.find ids_to_inner_sorts id in
@@ -71,7 +71,7 @@ let print_term ids_to_inner_sorts =
                   ("id",id)::("type",sort)::
                   match binder with
                      Names.Anonymous -> []
-                   | Names.Name b -> ["binder",Names.string_of_id b]
+                   | Names.Name b -> ["binder",Names.Id.to_string b]
                  in
                   [< X.xml_nempty "decl" attrs (aux s) ; i >]
               ) [< >] prods ;
@@ -96,7 +96,7 @@ let print_term ids_to_inner_sorts =
                   ("id",id)::("type",sort)::
                   match binder with
                      Names.Anonymous -> []
-                   | Names.Name b -> ["binder",Names.string_of_id b]
+                   | Names.Name b -> ["binder",Names.Id.to_string b]
                  in
                   [< X.xml_nempty "decl" attrs (aux s) ; i >]
               ) [< >] lambdas ;
@@ -115,7 +115,7 @@ let print_term ids_to_inner_sorts =
                   ("id",id)::("sort",sort)::
                   match binder with
                      Names.Anonymous -> assert false
-                   | Names.Name b -> ["binder",Names.string_of_id b]
+                   | Names.Name b -> ["binder",Names.Id.to_string b]
                  in
                   [< X.xml_nempty "def" attrs (aux s) ; i >]
               ) [< >] letins ;
@@ -161,7 +161,7 @@ let print_term ids_to_inner_sorts =
               (fun i (id,fi,ai,ti,bi) ->
                 [< i ;
                    X.xml_nempty "FixFunction"
-                    ["id",id ; "name", (Names.string_of_id fi) ;
+                    ["id",id ; "name", (Names.Id.to_string fi) ;
                      "recIndex", (string_of_int ai)]
                     [< X.xml_nempty "type" [] [< aux ti >] ;
                        X.xml_nempty "body" [] [< aux bi >]
@@ -177,7 +177,7 @@ let print_term ids_to_inner_sorts =
               (fun i (id,fi,ti,bi) ->
                 [< i ;
                    X.xml_nempty "CofixFunction"
-                    ["id",id ; "name", Names.string_of_id fi]
+                    ["id",id ; "name", Names.Id.to_string fi]
                     [< X.xml_nempty "type" [] [< aux ti >] ;
                        X.xml_nempty "body" [] [< aux bi >]
                     >]
@@ -229,11 +229,11 @@ let print_object uri ids_to_inner_sorts =
                           [< (match t with
                                 n,A.Decl t ->
                                  X.xml_nempty "Decl"
-                                  ["id",hid;"name",Names.string_of_id n]
+                                  ["id",hid;"name",Names.Id.to_string n]
                                   (print_term ids_to_inner_sorts t)
                               | n,A.Def (t,_) ->
                                  X.xml_nempty "Def"
-                                  ["id",hid;"name",Names.string_of_id n]
+                                  ["id",hid;"name",Names.Id.to_string n]
                                   (print_term ids_to_inner_sorts t)
                              ) ;
                              i
@@ -315,7 +315,7 @@ let print_object uri ids_to_inner_sorts =
                   (fun i (id,typename,finite,arity,cons) ->
                     [< i ;
                        X.xml_nempty "InductiveType"
-                        ["id",id ; "name",Names.string_of_id typename ;
+                        ["id",id ; "name",Names.Id.to_string typename ;
                          "inductive",(string_of_bool finite)
                         ]
                         [< X.xml_nempty "arity" []
@@ -324,7 +324,7 @@ let print_object uri ids_to_inner_sorts =
                             (fun i (name,lc) ->
                               [< i ;
                                  X.xml_nempty "Constructor"
-                                  ["name",Names.string_of_id name]
+                                  ["name",Names.Id.to_string name]
                                   (print_term ids_to_inner_sorts lc)
                               >]) [<>] cons
                            )
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index 62f7cc7cf..d817396f1 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -62,7 +62,7 @@ let get_uri_of_var v pvars =
       [] -> Errors.error ("Variable "^v^" not found")
     | he::tl as modules ->
        let dirpath = N.make_dirpath modules in
-        if List.mem (N.id_of_string v) (D.last_section_hyps dirpath) then
+        if List.mem (N.Id.of_string v) (D.last_section_hyps dirpath) then
          modules
         else
          search_in_open_sections tl
@@ -75,7 +75,7 @@ let get_uri_of_var v pvars =
    in
     "cic:" ^
      List.fold_left
-      (fun i x -> "/" ^ N.string_of_id x ^ i) "" path
+      (fun i x -> "/" ^ N.Id.to_string x ^ i) "" path
 ;;
 
 type tag =
@@ -120,8 +120,8 @@ let subtract l1 l2 =
 let token_list_of_path dir id tag =
  let module N = Names in
   let token_list_of_dirpath dirpath =
-   List.rev_map N.string_of_id (N.repr_dirpath dirpath) in
-  token_list_of_dirpath dir @ [N.string_of_id id ^ "." ^ (ext_of_tag tag)]
+   List.rev_map N.Id.to_string (N.repr_dirpath dirpath) in
+  token_list_of_dirpath dir @ [N.Id.to_string id ^ "." ^ (ext_of_tag tag)]
 
 let token_list_of_kernel_name tag =
  let module N = Names in
@@ -202,7 +202,7 @@ let typeur sigma metamap =
           let (_,_,ty) = Environ.lookup_named id env in
           ty
         with Not_found ->
-          Errors.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
+          Errors.anomaly ("type_of: variable "^(Names.Id.to_string id)^" unbound"))
     | T.Const c ->
         let cb = Environ.lookup_constant c env in
         Typeops.type_of_constant_type env (cb.Declarations.const_type)
@@ -455,8 +455,8 @@ print_endline "PASSATO" ; flush stdout ;
                 let he1' = remove_module_dirpath_from_dirpath ~basedir he1_sp in
                 let he1'' =
                  String.concat "/"
-                  (List.map Names.string_of_id (List.rev he1')) ^ "/"
-                 ^ (Names.string_of_id he1_id) ^ ".var"
+                  (List.map Names.Id.to_string (List.rev he1')) ^ "/"
+                 ^ (Names.Id.to_string he1_id) ^ ".var"
                 in
                  (he1'',he2)::subst, extra_args, uninst
            in
@@ -501,13 +501,13 @@ print_endline "PASSATO" ; flush stdout ;
                A.ARel (fresh_id'', n, List.nth idrefs (n-1), id)
            | T.Var id ->
 	      let pvars = Termops.ids_of_named_context (E.named_context env) in
-	      let pvars = List.map N.string_of_id pvars in
-              let path = get_uri_of_var (N.string_of_id id) pvars in
+	      let pvars = List.map N.Id.to_string pvars in
+              let path = get_uri_of_var (N.Id.to_string id) pvars in
                Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
                if is_a_Prop innersort  && expected_available then
                 add_inner_type fresh_id'' ;
                A.AVar
-                (fresh_id'', path ^ "/" ^ (N.string_of_id id) ^ ".var")
+                (fresh_id'', path ^ "/" ^ (N.Id.to_string id) ^ ".var")
            | T.Evar (n,l) ->
               Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
               if is_a_Prop innersort  && expected_available then
@@ -610,7 +610,7 @@ print_endline "PASSATO" ; flush stdout ;
            | T.LetIn (n,s,t,d) ->
               let id =
                match n with
-                   N.Anonymous -> N.id_of_string "_X"
+                   N.Anonymous -> N.Id.of_string "_X"
                  | N.Name id -> id
               in
               let n' =
@@ -886,7 +886,7 @@ let acic_object_of_cic_object sigma obj =
                          in
                          let dummy_never_used =
                           let s = "dummy_never_used" in
-                           A.ARel (s,99,s,Names.id_of_string s)
+                           A.ARel (s,99,s,Names.Id.of_string s)
                          in
                           final_env,final_idrefs,
                            (hid,(n,A.Def (at,dummy_never_used)))::atl
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 8259266af..35760a51d 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -35,7 +35,7 @@ let filter_params pvars hyps =
       let ids' = id::ids in
       let ids'' =
        "cic:/" ^
-        String.concat "/" (List.rev (List.map Names.string_of_id ids')) in
+        String.concat "/" (List.rev (List.map Names.Id.to_string ids')) in
       let he' =
        ids'', List.rev (List.filter (function x -> List.mem x hyps) he) in
       let tl' = aux ids' tl in
@@ -44,7 +44,7 @@ let filter_params pvars hyps =
         | _,_  -> he'::tl'
  in
   let cwd = Lib.cwd () in
-  let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
+  let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
   let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
    aux (Names.repr_dirpath modulepath) (List.rev pvars)
 ;;
@@ -55,7 +55,7 @@ let filter_params pvars hyps =
 let search_variables () =
  let module N = Names in
   let cwd = Lib.cwd () in
-  let cwdsp = Libnames.make_path cwd (Names.id_of_string "dummy") in
+  let cwdsp = Libnames.make_path cwd (Names.Id.of_string "dummy") in
   let modulepath = Cic2acic.get_module_path_of_full_path cwdsp in
    let rec aux =
     function
@@ -63,7 +63,7 @@ let search_variables () =
      | he::tl as modules ->
         let one_section_variables =
          let dirpath = N.make_dirpath (modules @ N.repr_dirpath modulepath) in
-          let t = List.map N.string_of_id (Decls.last_section_hyps dirpath) in
+          let t = List.map N.Id.to_string (Decls.last_section_hyps dirpath) in
            [he,t]
         in
          one_section_variables @ aux tl
@@ -113,7 +113,7 @@ let theory_filename xml_library_root =
   match xml_library_root with
     None -> None  (* stdout *)
   | Some xml_library_root' ->
-     let toks = List.map N.string_of_id (N.repr_dirpath (Lib.library_dp ())) in
+     let toks = List.map N.Id.to_string (N.repr_dirpath (Lib.library_dp ())) in
      (* theory from A/B/C/F.v goes into A/B/C/F.theory *)
      let alltoks = List.rev toks in
        Some (join_dirs xml_library_root' alltoks ^ ".theory")
@@ -153,7 +153,7 @@ let print_object uri obj sigma filename =
 
 let string_list_of_named_context_list =
  List.map
-  (function (n,_,_) -> Names.string_of_id n)
+  (function (n,_,_) -> Names.Id.to_string n)
 ;;
 
 (* Function to collect the variables that occur in a term. *)
@@ -212,11 +212,11 @@ let mk_variable_obj id body typ =
    | Some bo -> find_hyps bo, Some (Unshare.unshare bo)
  in
   let hyps' = find_hyps typ @ hyps in
-  let hyps'' = List.map Names.string_of_id hyps' in
+  let hyps'' = List.map Names.Id.to_string hyps' in
   let variables = search_variables () in
   let params = filter_params variables hyps'' in
    Acic.Variable
-    (Names.string_of_id id, unsharedbody, Unshare.unshare typ, params)
+    (Names.Id.to_string id, unsharedbody, Unshare.unshare typ, params)
 ;;
 
 
@@ -226,10 +226,10 @@ let mk_constant_obj id bo ty variables hyps =
  let params = filter_params variables hyps in
   match bo with
      None ->
-      Acic.Constant (Names.string_of_id id,None,ty,params)
+      Acic.Constant (Names.Id.to_string id,None,ty,params)
    | Some c ->
       Acic.Constant
-       (Names.string_of_id id, Some (Unshare.unshare (Declarations.force c)),
+       (Names.Id.to_string id, Some (Unshare.unshare (Declarations.force c)),
          ty,params)
 ;;
 
@@ -531,7 +531,7 @@ let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ;
 
 let uri_of_dirpath dir =
   "/" ^ String.concat "/"
-    (List.map Names.string_of_id (List.rev (Names.repr_dirpath dir)))
+    (List.map Names.Id.to_string (List.rev (Names.repr_dirpath dir)))
 ;;
 
 let _ =