diff options
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/common.ml | 4 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.ml | 2 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 12 | ||||
| -rw-r--r-- | plugins/extraction/table.mli | 2 |
4 files changed, 10 insertions, 10 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 11c3b3b5b6..e1edeec37e 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -303,9 +303,9 @@ let ref_renaming_fun (k,r) = if l = [""] (* this happens only at toplevel of the monolithic case *) then let globs = Idset.elements (get_global_ids ()) in - let id = next_ident_away (kindcase_id k (safe_id_of_global r)) globs in + let id = next_ident_away (kindcase_id k (safe_basename_of_global r)) globs in string_of_id id - else modular_rename k (safe_id_of_global r) + else modular_rename k (safe_basename_of_global r) in add_global_ids (id_of_string s); s::l diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 39e2770819..ba4786d37d 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -506,7 +506,7 @@ let simple_extraction r = match locate_ref [r] with let extraction_library is_rec m = init true; let dir_m = - let q = make_short_qualid m in + let q = qualid_of_ident m in try Nametab.full_name_module q with Not_found -> error_unknown_module q in Visit.add_mp (MPfile dir_m); diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 83a780198a..13a730ac20 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -182,7 +182,7 @@ let modular () = !modular_ref WARNING: for inductive objects, an extract_inductive must have been done before. *) -let safe_id_of_global = function +let safe_basename_of_global = function | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename | ConstructRef ((kn,i),j) -> @@ -191,7 +191,7 @@ let safe_id_of_global = function let safe_pr_global r = try Printer.pr_global r - with _ -> pr_id (safe_id_of_global r) + with _ -> pr_id (safe_basename_of_global r) (* idem, but with qualification, and only for constants. *) @@ -207,7 +207,7 @@ let pr_long_mp mp = let lid = repr_dirpath (Nametab.dir_of_mp mp) in str (String.concat "." (List.map string_of_id (List.rev lid))) -let pr_long_global ref = pr_sp (Nametab.sp_of_global ref) +let pr_long_global ref = pr_path (Nametab.path_of_global ref) (*S Warning and Error messages. *) @@ -452,7 +452,7 @@ let (inline_extraction,_) = cache_function = (fun (_,(b,l)) -> add_inline_entries b l); load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); export_function = (fun x -> Some x); - classify_function = (fun (_,o) -> Substitute o); + classify_function = (fun o -> Substitute o); subst_function = (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l))) } @@ -535,7 +535,7 @@ let (blacklist_extraction,_) = cache_function = (fun (_,l) -> add_blacklist_entries l); load_function = (fun _ (_,l) -> add_blacklist_entries l); export_function = (fun x -> Some x); - classify_function = (fun (_,o) -> Libobject.Keep o); + classify_function = (fun o -> Libobject.Keep o); subst_function = (fun (_,_,x) -> x) } @@ -595,7 +595,7 @@ let (in_customs,_) = cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s); export_function = (fun x -> Some x); - classify_function = (fun (_,o) -> Substitute o); + classify_function = (fun o -> Substitute o); subst_function = (fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str)) } diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 6e3f2ec56b..42ed6eef01 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -13,7 +13,7 @@ open Libnames open Miniml open Declarations -val safe_id_of_global : global_reference -> identifier +val safe_basename_of_global : global_reference -> identifier (*s Warning and Error messages. *) |