diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
commit | 67f5c70a480c95cfb819fc68439781b5e5e95794 (patch) | |
tree | 67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /plugins/extraction/table.ml | |
parent | cc03a5f82efa451b6827af9a9b42cee356ed4f8a (diff) |
Modulification of identifier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/table.ml')
-rw-r--r-- | plugins/extraction/table.ml | 34 |
1 files changed, 17 insertions, 17 deletions
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 ()) |