Modulification of identifier

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

15 files changed, 82 insertions, 82 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 04cc167a8..3269befdb 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -18,7 +18,7 @@ open Miniml
 open Mlutil
 
 let string_of_id id =
-  let s = Names.string_of_id id in
+  let s = Names.Id.to_string id in
   for i = 0 to String.length s - 2 do
     if s.[i] = '_' && s.[i+1] = '_' then warning_id s
   done;
@@ -109,12 +109,12 @@ let pseudo_qualify = qualify "__"
 let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 
-let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
+let lowercase_id id = Id.of_string (String.uncapitalize (string_of_id id))
 let uppercase_id id =
   let s = string_of_id id in
   assert (s<>"");
-  if s.[0] = '_' then id_of_string ("Coq_"^s)
-  else id_of_string (String.capitalize s)
+  if s.[0] = '_' then Id.of_string ("Coq_"^s)
+  else Id.of_string (String.capitalize s)
 
 type kind = Term | Type | Cons | Mod
 
@@ -128,12 +128,12 @@ let kindcase_id k id =
 
 (*s de Bruijn environments for programs *)
 
-type env = identifier list * Idset.t
+type env = Id.t list * Id.Set.t
 
 (*s Generic renaming issues for local variable names. *)
 
 let rec rename_id id avoid =
-  if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id
+  if Id.Set.mem id avoid then rename_id (lift_subscript id) avoid else id
 
 let rec rename_vars avoid = function
   | [] ->
@@ -145,14 +145,14 @@ let rec rename_vars avoid = function
   | id :: idl ->
       let (idl, avoid) = rename_vars avoid idl in
       let id = rename_id (lowercase_id id) avoid in
-      (id :: idl, Idset.add id avoid)
+      (id :: idl, Id.Set.add id avoid)
 
 let rename_tvars avoid l =
   let rec rename avoid = function
     | [] -> [],avoid
     | id :: idl ->
 	let id = rename_id (lowercase_id id) avoid in
-	let idl, avoid = rename (Idset.add id avoid) idl in
+	let idl, avoid = rename (Id.Set.add id avoid) idl in
 	(id :: idl, avoid) in
   fst (rename avoid l)
 
@@ -162,7 +162,7 @@ let push_vars ids (db,avoid) =
 
 let get_db_name n (db,_) =
   let id = List.nth db (pred n) in
-  if id = dummy_name then id_of_string "__" else id
+  if id = dummy_name then Id.of_string "__" else id
 
 
 (*S Renamings of global objects. *)
@@ -179,13 +179,13 @@ let set_phase, get_phase =
   let ph = ref Impl in ((:=) ph), (fun () -> !ph)
 
 let set_keywords, get_keywords =
-  let k = ref Idset.empty in
+  let k = ref Id.Set.empty in
   ((:=) k), (fun () -> !k)
 
 let add_global_ids, get_global_ids =
-  let ids = ref Idset.empty in
+  let ids = ref Id.Set.empty in
   register_cleanup (fun () -> ids := get_keywords ());
-  let add s = ids := Idset.add s !ids
+  let add s = ids := Id.Set.add s !ids
   and get () = !ids
   in (add,get)
 
@@ -309,7 +309,7 @@ let modular_rename k id =
     if upperkind k then "Coq_",is_upper else "coq_",is_lower
   in
   if not (is_ok s) ||
-    (Idset.mem id (get_keywords ())) ||
+    (Id.Set.mem id (get_keywords ())) ||
     (String.length s >= 4 && String.sub s 0 4 = prefix)
   then prefix ^ s
   else s
@@ -320,7 +320,7 @@ let modular_rename k id =
 let modfstlev_rename =
   let add_prefixes,get_prefixes,_ = mktable true in
   fun l ->
-    let coqid = id_of_string "Coq" in
+    let coqid = Id.of_string "Coq" in
     let id = id_of_label l in
     try
       let coqset = get_prefixes id in
@@ -372,12 +372,12 @@ let ref_renaming_fun (k,r) =
     let idg = safe_basename_of_global r in
     if l = [""] (* this happens only at toplevel of the monolithic case *)
     then
-      let globs = Idset.elements (get_global_ids ()) in
+      let globs = Id.Set.elements (get_global_ids ()) in
       let id = next_ident_away (kindcase_id k idg) globs in
       string_of_id id
     else modular_rename k idg
   in
-  add_global_ids (id_of_string s);
+  add_global_ids (Id.of_string s);
   s::l
 
 (* Cached version of the last function *)
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 7233b8c2b..9ddd0f2af 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -33,17 +33,17 @@ val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds
 val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 
-val pr_binding : identifier list -> std_ppcmds
+val pr_binding : Id.t list -> std_ppcmds
 
-val rename_id : identifier -> Idset.t -> identifier
+val rename_id : Id.t -> Id.Set.t -> Id.t
 
-type env = identifier list * Idset.t
+type env = Id.t list * Id.Set.t
 val empty_env : unit -> env
 
-val rename_vars: Idset.t -> identifier list -> env
-val rename_tvars: Idset.t -> identifier list -> identifier list
-val push_vars : identifier list -> env -> identifier list * env
-val get_db_name : int -> env -> identifier
+val rename_vars: Id.Set.t -> Id.t list -> env
+val rename_tvars: Id.Set.t -> Id.t list -> Id.t list
+val push_vars : Id.t list -> env -> Id.t list * env
+val get_db_name : int -> env -> Id.t
 
 type phase = Pre | Impl | Intf
 
@@ -69,7 +69,7 @@ type reset_kind = AllButExternal | Everything
 
 val reset_renaming_tables : reset_kind -> unit
 
-val set_keywords : Idset.t -> unit
+val set_keywords : Id.Set.t -> unit
 
 (** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *)
 
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 0b4047f17..3cd3f7f8a 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -388,7 +388,7 @@ let descr () = match lang () with
 (* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli"
    Works similarly for the other languages. *)
 
-let default_id = id_of_string "Main"
+let default_id = Id.of_string "Main"
 
 let mono_filename f =
   let d = descr () in
@@ -402,7 +402,7 @@ let mono_filename f =
 	in
 	let id =
 	  if lang () <> Haskell then default_id
-	  else try id_of_string (Filename.basename f)
+	  else try Id.of_string (Filename.basename f)
 	  with _ -> error "Extraction: provided filename is not a valid identifier"
 	in
 	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
@@ -412,7 +412,7 @@ let mono_filename f =
 let module_filename mp =
   let f = file_of_modfile mp in
   let d = descr () in
-  Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f
+  Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, Id.of_string f
 
 (*s Extraction of one decl to stdout. *)
 
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 5e14214b9..6c648b981 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -15,7 +15,7 @@ open Globnames
 val simple_extraction : reference -> unit
 val full_extraction : string option -> reference list -> unit
 val separate_extraction : reference list -> unit
-val extraction_library : bool -> identifier -> unit
+val extraction_library : bool -> Id.t -> unit
 
 (* For debug / external output via coqtop.byte + Drop : *)
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6645f1d5d..5b31db3f9 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -192,7 +192,7 @@ let parse_ind_args si args relmax =
   in parse 1 1 si
 
 let oib_equal o1 o2 =
-  id_ord o1.mind_typename o2.mind_typename = 0 &&
+  Id.compare o1.mind_typename o2.mind_typename = 0 &&
   List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
   begin match o1.mind_arity, o2.mind_arity with
   | Monomorphic {mind_user_arity=c1; mind_sort=s1},
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 1eb9ca8e5..3a5fc9794 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -19,7 +19,7 @@ val extract_constant : env -> constant -> constant_body -> ml_decl
 
 val extract_constant_spec : env -> constant -> constant_body -> ml_spec
 
-val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) option
+val extract_with_type : env -> constant_body -> ( Id.t list * ml_type ) option
 
 val extract_fixpoint :
   env -> constant array -> (constr, types) prec_declaration -> ml_decl
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index bdb102b18..5295e2cf9 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -33,7 +33,7 @@ let pr_int_or_id _ _ _ = function
 ARGUMENT EXTEND int_or_id
   TYPED AS int_or_id
   PRINTED BY pr_int_or_id
-| [ preident(id) ] -> [ ArgId (id_of_string id) ]
+| [ preident(id) ] -> [ ArgId (Id.of_string id) ]
 | [ integer(i) ] -> [ ArgInt i ]
 END
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 5de13e53c..3925a2a2f 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -21,16 +21,16 @@ open Common
 
 (*s Haskell renaming issues. *)
 
-let pr_lower_id id = str (String.uncapitalize (string_of_id id))
-let pr_upper_id id = str (String.capitalize (string_of_id id))
+let pr_lower_id id = str (String.uncapitalize (Id.to_string id))
+let pr_upper_id id = str (String.capitalize (Id.to_string id))
 
 let keywords =
-  List.fold_right (fun s -> Idset.add (id_of_string s))
+  List.fold_right (fun s -> Id.Set.add (Id.of_string s))
   [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
     "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
     "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
-  Idset.empty
+  Id.Set.empty
 
 let pp_comment s = str "-- " ++ s ++ fnl ()
 let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}"
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index d170acbb0..14a30ae79 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -65,11 +65,11 @@ type inductive_kind =
 *)
 
 type ml_ind_packet = {
-  ip_typename : identifier;
-  ip_consnames : identifier array;
+  ip_typename : Id.t;
+  ip_consnames : Id.t array;
   ip_logical : bool;
   ip_sign : signature;
-  ip_vars : identifier list;
+  ip_vars : Id.t list;
   ip_types : (ml_type list) array
 }
 
@@ -91,8 +91,8 @@ type ml_ind = {
 
 type ml_ident =
   | Dummy
-  | Id of identifier
-  | Tmp of identifier
+  | Id of Id.t
+  | Tmp of Id.t
 
 (** We now store some typing information on constructors
     and cases to avoid type-unsafe optimisations. This will be
@@ -116,7 +116,7 @@ and ml_ast =
   | MLcons   of ml_type * global_reference * ml_ast list
   | MLtuple  of ml_ast list
   | MLcase   of ml_type * ml_ast * ml_branch array
-  | MLfix    of int * identifier array * ml_ast array
+  | MLfix    of int * Id.t array * ml_ast array
   | MLexn    of string
   | MLdummy
   | MLaxiom
@@ -133,13 +133,13 @@ and ml_pattern =
 
 type ml_decl =
   | Dind  of mutual_inductive * ml_ind
-  | Dtype of global_reference * identifier list * ml_type
+  | Dtype of global_reference * Id.t list * ml_type
   | Dterm of global_reference * ml_ast * ml_type
   | Dfix  of global_reference array * ml_ast array * ml_type array
 
 type ml_spec =
   | Sind  of mutual_inductive * ml_ind
-  | Stype of global_reference * identifier list * ml_type option
+  | Stype of global_reference * Id.t list * ml_type option
   | Sval  of global_reference * ml_type
 
 type ml_specif =
@@ -154,8 +154,8 @@ and ml_module_type =
   | MTwith of ml_module_type * ml_with_declaration
 
 and ml_with_declaration =
-  | ML_With_type of identifier list * identifier list * ml_type
-  | ML_With_module of identifier list * module_path
+  | 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
 
@@ -191,13 +191,13 @@ type unsafe_needs = {
 }
 
 type language_descr = {
-  keywords : Idset.t;
+  keywords : Id.Set.t;
 
   (* Concerning the source file *)
   file_suffix : string;
   (* the second argument is a comment to add to the preamble *)
   preamble :
-    identifier -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
     std_ppcmds;
   pp_struct : ml_structure -> std_ppcmds;
 
@@ -205,7 +205,7 @@ type language_descr = {
   sig_suffix : string option;
   (* the second argument is a comment to add to the preamble *)
   sig_preamble :
-    identifier -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
     std_ppcmds;
   pp_sig : ml_signature -> std_ppcmds;
 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 18c3f840e..d8d1d1eae 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -22,8 +22,8 @@ exception Impossible
 
 (*S Names operations. *)
 
-let anonymous_name = id_of_string "x"
-let dummy_name = id_of_string "_"
+let anonymous_name = Id.of_string "x"
+let dummy_name = Id.of_string "_"
 
 let anonymous = Id anonymous_name
 
@@ -857,7 +857,7 @@ let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
 
 let is_program_branch = function
   | Id id ->
-    let s = string_of_id id in
+    let s = Id.to_string id in
     let br = "program_branch_" in
     let n = String.length br in
     (try
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index be32ba6ed..1c70908b6 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -77,10 +77,10 @@ val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast
 (*s Special identifiers. [dummy_name] is to be used for dead code
     and will be printed as [_] in concrete (Caml) code. *)
 
-val anonymous_name : identifier
-val dummy_name : identifier
-val id_of_name : name -> identifier
-val id_of_mlid : ml_ident -> identifier
+val anonymous_name : Id.t
+val dummy_name : Id.t
+val id_of_name : name -> Id.t
+val id_of_mlid : ml_ident -> Id.t
 val tmp_id : ml_ident -> ml_ident
 
 (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 7640416fd..b8d75d445 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -24,7 +24,7 @@ open Common
 (*s Some utility functions. *)
 
 let pp_tvar id =
-  let s = string_of_id id in
+  let s = Id.to_string id in
   if String.length s < 2 || s.[1]<>'\''
   then str ("'"^s)
   else str ("' "^s)
@@ -48,7 +48,7 @@ let pp_letin pat def body =
 (*s Ocaml renaming issues. *)
 
 let keywords =
-  List.fold_right (fun s -> Idset.add (id_of_string s))
+  List.fold_right (fun s -> Id.Set.add (Id.of_string s))
   [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
     "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
     "for"; "fun"; "function"; "functor"; "if"; "in"; "include";
@@ -57,7 +57,7 @@ let keywords =
     "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
     "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
-  Idset.empty
+  Id.Set.empty
 
 let pp_open mp = str ("open "^ string_of_modfile mp ^"\n")
 
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index bfbcc7b0a..8125b4757 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -20,11 +20,11 @@ open Common
 (*s Scheme renaming issues. *)
 
 let keywords =
-  List.fold_right (fun s -> Idset.add (id_of_string s))
+  List.fold_right (fun s -> Id.Set.add (Id.of_string s))
     [ "define"; "let"; "lambda"; "lambdas"; "match";
       "apply"; "car"; "cdr";
       "error"; "delay"; "force"; "_"; "__"]
-    Idset.empty
+    Id.Set.empty
 
 let pp_comment s = str";; "++h 0 s++fnl ()
 
@@ -40,7 +40,7 @@ let preamble _ comment _ usf =
   (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
 let pr_id id =
-  let s = string_of_id id in
+  let s = Id.to_string id in
   for i = 0 to String.length s - 1 do
     if s.[i] = '\'' then s.[i] <- '~'
   done;
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index dd3b65b90..c7d8d42de 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -56,7 +56,7 @@ let is_modfile = function
   | _ -> false
 
 let raw_string_of_modfile = function
-  | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
+  | MPfile f -> String.capitalize (Id.to_string (List.hd (repr_dirpath f)))
   | _ -> assert false
 
 let current_toplevel () = fst (Lib.current_prefix ())
@@ -256,8 +256,8 @@ let safe_basename_of_global r =
     | VarRef _ -> assert false
 
 let string_of_global r =
- try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
- with _ -> string_of_id (safe_basename_of_global r)
+ try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r)
+ with _ -> Id.to_string (safe_basename_of_global r)
 
 let safe_pr_global r = str (string_of_global r)
 
@@ -273,7 +273,7 @@ let safe_pr_long_global r =
 
 let pr_long_mp mp =
   let lid = repr_dirpath (Nametab.dirpath_of_module mp) in
-  str (String.concat "." (List.map string_of_id (List.rev lid)))
+  str (String.concat "." (List.map Id.to_string (List.rev lid)))
 
 let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 
@@ -411,7 +411,7 @@ let error_MPfile_as_mod mp b =
 let msg_non_implicit r n id =
   let name = match id with
     | Anonymous -> ""
-    | Name id -> "(" ^ string_of_id id ^ ") "
+    | Name id -> "(" ^ Id.to_string id ^ ") "
   in
   "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r)
 
@@ -652,7 +652,7 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 (*s Extraction Implicit *)
 
-type int_or_id = ArgInt of int | ArgId of identifier
+type int_or_id = ArgInt of int | ArgId of Id.t
 
 let implicits_table = ref Refmap'.empty
 
@@ -704,21 +704,21 @@ let extraction_implicit r l =
 
 (*s Extraction Blacklist of filenames not to use while extracting *)
 
-let blacklist_table = ref Idset.empty
+let blacklist_table = ref Id.Set.empty
 
 let modfile_ids = ref []
 let modfile_mps = ref MPmap.empty
 
 let reset_modfile () =
-  modfile_ids := Idset.elements !blacklist_table;
+  modfile_ids := Id.Set.elements !blacklist_table;
   modfile_mps := MPmap.empty
 
 let string_of_modfile mp =
   try MPmap.find mp !modfile_mps
   with Not_found ->
-    let id = id_of_string (raw_string_of_modfile mp) in
+    let id = Id.of_string (raw_string_of_modfile mp) in
     let id' = next_ident_away id !modfile_ids in
-    let s' = string_of_id id' in
+    let s' = Id.to_string id' in
     modfile_ids := id' :: !modfile_ids;
     modfile_mps := MPmap.add mp s' !modfile_mps;
     s'
@@ -727,7 +727,7 @@ let string_of_modfile mp =
 
 let file_of_modfile mp =
   let s0 = match mp with
-    | MPfile f -> string_of_id (List.hd (repr_dirpath f))
+    | MPfile f -> Id.to_string (List.hd (repr_dirpath f))
     | _ -> assert false
   in
   let s = String.copy (string_of_modfile mp) in
@@ -736,7 +736,7 @@ let file_of_modfile mp =
 
 let add_blacklist_entries l =
   blacklist_table :=
-    List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s)))
+    List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s)))
       l !blacklist_table
 
 (* Registration of operations for rollback. *)
@@ -752,26 +752,26 @@ let blacklist_extraction : string list -> obj =
 let _ = declare_summary "Extraction Blacklist"
 	  { freeze_function = (fun () -> !blacklist_table);
 	    unfreeze_function = ((:=) blacklist_table);
-	    init_function = (fun () -> blacklist_table := Idset.empty) }
+	    init_function = (fun () -> blacklist_table := Id.Set.empty) }
 
 (* Grammar entries. *)
 
 let extraction_blacklist l =
-  let l = List.rev_map string_of_id l in
+  let l = List.rev_map Id.to_string l in
   Lib.add_anonymous_leaf (blacklist_extraction l)
 
 (* Printing part *)
 
 let print_extraction_blacklist () =
-  prlist_with_sep fnl pr_id (Idset.elements !blacklist_table)
+  prlist_with_sep fnl pr_id (Id.Set.elements !blacklist_table)
 
 (* Reset part *)
 
 let reset_blacklist : unit -> obj =
   declare_object
     {(default_object "Reset Extraction Blacklist") with
-       cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
-       load_function = (fun _ (_,_)-> blacklist_table := Idset.empty)}
+       cache_function = (fun (_,_)-> blacklist_table := Id.Set.empty);
+       load_function = (fun _ (_,_)-> blacklist_table := Id.Set.empty)}
 
 let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 16c2275f1..fbf48889f 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -15,7 +15,7 @@ open Declarations
 module Refset' : Set.S with type elt = global_reference
 module Refmap' : Map.S with type key = global_reference
 
-val safe_basename_of_global : global_reference -> identifier
+val safe_basename_of_global : global_reference -> Id.t
 
 (*s Warning and Error messages. *)
 
@@ -30,7 +30,7 @@ val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
 val error_module_clash : module_path -> module_path -> 'a
 val error_no_module_expr : module_path -> 'a
-val error_singleton_become_prop : identifier -> 'a
+val error_singleton_become_prop : Id.t -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
@@ -193,12 +193,12 @@ val extract_inductive :
   reference -> string -> string list -> string option -> unit
 
 
-type int_or_id = ArgInt of int | ArgId of identifier
+type int_or_id = ArgInt of int | ArgId of Id.t
 val extraction_implicit : reference -> int_or_id list -> unit
 
 (*s Table of blacklisted filenames *)
 
-val extraction_blacklist : identifier list -> unit
+val extraction_blacklist : Id.t list -> unit
 val reset_extraction_blacklist : unit -> unit
 val print_extraction_blacklist : unit -> Pp.std_ppcmds