Modulification of identifier

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

12 files changed, 44 insertions, 44 deletions

diff --git a/checker/check.ml b/checker/check.ml
index a3fc6d0f78..31f75f4f90 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -21,12 +21,12 @@ type section_path = {
   dirpath : string list ;
   basename : string }
 let dir_of_path p =
-  make_dirpath (List.map id_of_string p.dirpath)
+  make_dirpath (List.map Id.of_string p.dirpath)
 let path_of_dirpath dir =
   match repr_dirpath dir with
       [] -> failwith "path_of_dirpath"
     | l::dir ->
-        {dirpath=List.map string_of_id dir;basename=string_of_id l}
+        {dirpath=List.map Id.to_string dir;basename=Id.to_string l}
 let pr_dirlist dp =
   prlist_with_sep (fun _ -> str".") str (List.rev dp)
 let pr_path sp =
@@ -203,7 +203,7 @@ let locate_absolute_library dir =
   let loadpath = load_paths_of_dir_path pref in
   if loadpath = [] then raise LibUnmappedDir;
   try
-    let name = string_of_id base^".vo" in
+    let name = Id.to_string base^".vo" in
     let _, file = System.where_in_path ~warn:false loadpath name in
     (dir, file)
   with Not_found ->
@@ -226,7 +226,7 @@ let locate_qualified_library qid =
     let name =  qid.basename^".vo" in
     let path, file = System.where_in_path loadpath name in
     let dir =
-      extend_dirpath (find_logical_path path) (id_of_string qid.basename) in
+      extend_dirpath (find_logical_path path) (Id.of_string qid.basename) in
     (* Look if loaded *)
     try
       (dir, library_full_filename dir)
diff --git a/checker/checker.ml b/checker/checker.ml
index 8e0a2a1e5c..5a7efacf88 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -19,7 +19,7 @@ let () = at_exit flush_all
 let fatal_error info =
   pperrnl info; flush_all (); exit 1
 
-let coq_root = id_of_string "Coq"
+let coq_root = Id.of_string "Coq"
 let parse_dir s =
   let len = String.length s in
   let rec decoupe_dirs dirs n =
@@ -36,7 +36,7 @@ let parse_dir s =
 let dirpath_of_string s =
   match parse_dir s with
       [] -> Check.default_root_prefix
-    | dir -> make_dirpath (List.map id_of_string dir)
+    | dir -> make_dirpath (List.map Id.of_string dir)
 let path_of_string s =
   match parse_dir s with
       [] -> invalid_arg "path_of_string"
@@ -69,7 +69,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
     msg_warning (str ("Cannot open " ^ dir))
 
 let convert_string d =
-  try id_of_string d
+  try Id.of_string d
   with _ ->
     if_verbose msg_warning (str ("Directory "^d^" cannot be used as a Coq identifier (skipped)"));
     raise Exit
diff --git a/checker/closure.ml b/checker/closure.ml
index c515bdb24b..9677680e6e 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -48,11 +48,11 @@ let with_stats c =
   end else
     Lazy.force c
 
-type transparent_state = Idpred.t * Cpred.t
-let all_opaque = (Idpred.empty, Cpred.empty)
-let all_transparent = (Idpred.full, Cpred.full)
+type transparent_state = Id.Pred.t * Cpred.t
+let all_opaque = (Id.Pred.empty, Cpred.empty)
+let all_transparent = (Id.Pred.full, Cpred.full)
 
-let is_transparent_variable (ids, _) id = Idpred.mem id ids
+let is_transparent_variable (ids, _) id = Id.Pred.mem id ids
 let is_transparent_constant (_, csts) cst = Cpred.mem cst csts
 
 module type RedFlagsSig = sig
@@ -63,7 +63,7 @@ module type RedFlagsSig = sig
   val fIOTA : red_kind
   val fZETA : red_kind
   val fCONST : constant -> red_kind
-  val fVAR : identifier -> red_kind
+  val fVAR : Id.t -> red_kind
   val no_red : reds
   val red_add : reds -> red_kind -> reds
   val mkflags : red_kind list -> reds
@@ -85,7 +85,7 @@ module RedFlags = (struct
     r_iota : bool }
 
   type red_kind = BETA | DELTA | IOTA | ZETA
-	      | CONST of constant | VAR of identifier
+	      | CONST of constant | VAR of Id.t
   let fBETA = BETA
   let fDELTA = DELTA
   let fIOTA = IOTA
@@ -110,7 +110,7 @@ module RedFlags = (struct
     | ZETA -> { red with r_zeta = true }
     | VAR id ->
 	let (l1,l2) = red.r_const in
-	{ red with r_const = Idpred.add id l1, l2 }
+	{ red with r_const = Id.Pred.add id l1, l2 }
 
   let mkflags = List.fold_left red_add no_red
 
@@ -122,7 +122,7 @@ module RedFlags = (struct
 	incr_cnt c delta
     | VAR id -> (* En attendant d'avoir des kn pour les Var *)
 	let (l,_) = red.r_const in
-	let c = Idpred.mem id l in
+	let c = Id.Pred.mem id l in
 	incr_cnt c delta
     | ZETA -> incr_cnt red.r_zeta zeta
     | IOTA -> incr_cnt red.r_iota iota
@@ -162,7 +162,7 @@ let betaiotazeta = mkflags [fBETA;fIOTA;fZETA]
 
 type table_key =
   | ConstKey of constant
-  | VarKey of identifier
+  | VarKey of Id.t
   | RelKey of int
 
 type 'a infos = {
@@ -170,7 +170,7 @@ type 'a infos = {
   i_repr : 'a infos -> constr -> 'a;
   i_env : env;
   i_rels : int * (int * constr) list;
-  i_vars : (identifier * constr) list;
+  i_vars : (Id.t * constr) list;
   i_tab : (table_key, 'a) Hashtbl.t }
 
 let ref_value_cache info ref =
@@ -544,7 +544,7 @@ let rec to_constr constr_fun lfts v =
         let fr = mk_clos2 env t in
         let unfv = update v (fr.norm,fr.term) in
         to_constr constr_fun lfts unfv
-    | FLOCKED -> assert false (*mkVar(id_of_string"_LOCK_")*)
+    | FLOCKED -> assert false (*mkVar(Id.of_string"_LOCK_")*)
 
 (* This function defines the correspondance between constr and
    fconstr. When we find a closure whose substitution is the identity,
diff --git a/checker/closure.mli b/checker/closure.mli
index 428197fa8f..443eeb6aa1 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -25,7 +25,7 @@ val with_stats: 'a Lazy.t -> 'a
   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
   a LetIn expression is Letin reduction *)
 
-type transparent_state = Idpred.t * Cpred.t
+type transparent_state = Id.Pred.t * Cpred.t
 
 val all_opaque      : transparent_state
 val all_transparent : transparent_state
@@ -44,7 +44,7 @@ module type RedFlagsSig = sig
   val fIOTA : red_kind
   val fZETA : red_kind
   val fCONST : constant -> red_kind
-  val fVAR : identifier -> red_kind
+  val fVAR : Id.t -> red_kind
 
   (* No reduction at all *)
   val no_red : reds
@@ -69,7 +69,7 @@ val betadeltaiotanolet : reds
 (***********************************************************************)
 type table_key =
   | ConstKey of constant
-  | VarKey of identifier
+  | VarKey of Id.t
   | RelKey of int
 
 type 'a infos
diff --git a/checker/declarations.ml b/checker/declarations.ml
index df0134e029..7e368dcad7 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -607,7 +607,7 @@ type one_inductive_body = {
 (* Primitive datas *)
 
  (* Name of the type: [Ii] *)
-    mind_typename : identifier;
+    mind_typename : Id.t;
 
  (* Arity context of [Ii] with parameters: [forall params, Ui] *)
     mind_arity_ctxt : rel_context;
@@ -616,7 +616,7 @@ type one_inductive_body = {
     mind_arity : inductive_arity;
 
  (* Names of the constructors: [cij] *)
-    mind_consnames : identifier array;
+    mind_consnames : Id.t array;
 
  (* Types of the constructors with parameters: [forall params, Tij],
     where the Ik are replaced by de Bruijn index in the context
@@ -764,8 +764,8 @@ and struct_expr_body =
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path
-  | With_definition_body of  identifier list * constant_body
+    With_module_body of Id.t list * module_path
+  | With_definition_body of  Id.t list * constant_body
 
 and module_body =
     { mod_mp : module_path;
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 7dfe609c35..c14d8b73a6 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -91,7 +91,7 @@ type one_inductive_body = {
 (* Primitive datas *)
 
  (* Name of the type: [Ii] *)
-    mind_typename : identifier;
+    mind_typename : Id.t;
 
  (* Arity context of [Ii] with parameters: [forall params, Ui] *)
     mind_arity_ctxt : rel_context;
@@ -100,7 +100,7 @@ type one_inductive_body = {
     mind_arity : inductive_arity;
 
  (* Names of the constructors: [cij] *)
-    mind_consnames : identifier array;
+    mind_consnames : Id.t array;
 
  (* Types of the constructors with parameters: [forall params, Tij],
     where the Ik are replaced by de Bruijn index in the context
@@ -191,8 +191,8 @@ and struct_expr_body =
   | SEBwith of struct_expr_body * with_declaration_body
 
 and with_declaration_body =
-    With_module_body of identifier list * module_path
-  | With_definition_body of  identifier list * constant_body
+    With_module_body of Id.t list * module_path
+  | With_definition_body of  Id.t list * constant_body
 
 and module_body =
     { mod_mp : module_path;
diff --git a/checker/environ.mli b/checker/environ.mli
index 628febbb09..36b76960f6 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -40,8 +40,8 @@ val push_rec_types : name array * constr array * 'a -> env -> env
 (* Named variables *)
 val named_context : env -> named_context
 val push_named : named_declaration -> env -> env
-val lookup_named : identifier -> env -> named_declaration
-val named_type : identifier -> env -> constr
+val lookup_named : Id.t -> env -> named_declaration
+val named_type : Id.t -> env -> constr
 
 (* Universes *)
 val universes : env -> Univ.universes
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 3539289e70..edd970f6b7 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -76,10 +76,10 @@ type inductive_error =
   | NotEnoughArgs of env * constr * constr
   | NotConstructor of env * constr * constr
   | NonPar of env * constr * int * constr * constr
-  | SameNamesTypes of identifier
-  | SameNamesConstructors of identifier
-  | SameNamesOverlap of identifier list
-  | NotAnArity of identifier
+  | SameNamesTypes of Id.t
+  | SameNamesConstructors of Id.t
+  | SameNamesOverlap of Id.t list
+  | NotAnArity of Id.t
   | BadEntry
 
 exception InductiveError of inductive_error
diff --git a/checker/indtypes.mli b/checker/indtypes.mli
index 691c9466f5..5c032a0ca2 100644
--- a/checker/indtypes.mli
+++ b/checker/indtypes.mli
@@ -27,10 +27,10 @@ type inductive_error =
   | NotEnoughArgs of env * constr * constr
   | NotConstructor of env * constr * constr
   | NonPar of env * constr * int * constr * constr
-  | SameNamesTypes of identifier
-  | SameNamesConstructors of identifier
-  | SameNamesOverlap of identifier list
-  | NotAnArity of identifier
+  | SameNamesTypes of Id.t
+  | SameNamesConstructors of Id.t
+  | SameNamesOverlap of Id.t list
+  | NotAnArity of Id.t
   | BadEntry
 
 exception InductiveError of inductive_error
diff --git a/checker/term.ml b/checker/term.ml
index 0c3fc741dd..6bafeda7f5 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -88,7 +88,7 @@ let val_cast = val_enum "cast_kind" 2
 
 type constr =
   | Rel       of int
-  | Var       of identifier
+  | Var       of Id.t
   | Meta      of metavariable
   | Evar      of constr pexistential
   | Sort      of sorts
@@ -318,7 +318,7 @@ let val_rdecl =
 let val_nctxt = val_list val_ndecl
 let val_rctxt = val_list val_rdecl
 
-type named_declaration = identifier * constr option * constr
+type named_declaration = Id.t * constr option * constr
 type rel_declaration = name * constr option * constr
 
 type named_context = named_declaration list
diff --git a/checker/term.mli b/checker/term.mli
index 0340c79b43..c417cd14e9 100644
--- a/checker/term.mli
+++ b/checker/term.mli
@@ -26,7 +26,7 @@ type 'a pcofixpoint = int * 'a prec_declaration
 type cast_kind = VMcast | DEFAULTcast
 type constr =
     Rel of int
-  | Var of identifier
+  | Var of Id.t
   | Meta of metavariable
   | Evar of constr pexistential
   | Sort of sorts
@@ -71,7 +71,7 @@ val substnl : constr list -> int -> constr -> constr
 val substl : constr list -> constr -> constr
 val subst1 : constr -> constr -> constr
 
-type named_declaration = identifier * constr option * constr
+type named_declaration = Id.t * constr option * constr
 type rel_declaration = name * constr option * constr
 type named_context = named_declaration list
 val empty_named_context : named_context
diff --git a/checker/typeops.ml b/checker/typeops.ml
index ad05f96b70..129c242b9b 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -395,7 +395,7 @@ let check_named_ctxt env ctxt =
     let _ =
       try
         let _ = lookup_named id env in
-        failwith ("variable "^string_of_id id^" defined twice")
+        failwith ("variable "^Id.to_string id^" defined twice")
       with Not_found -> () in
     match d with
         (_,None,ty) ->