diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 35 |
1 files changed, 17 insertions, 18 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ff66d915f5..607ca1b3a9 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open API open Names open Term open Declarations @@ -20,6 +21,11 @@ open Util open Pp open Miniml +[@@@ocaml.warning "-3"] (* String.capitalize_ascii since 4.03.0 GPR#124 *) +let capitalize = String.capitalize +[@@@ocaml.warning "+3"] + + (** Sets and maps for [global_reference] that use the "user" [kernel_name] instead of the canonical one *) @@ -55,7 +61,7 @@ let is_modfile = function | _ -> false let raw_string_of_modfile = function - | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f))) + | MPfile f -> capitalize (Id.to_string (List.hd (DirPath.repr f))) | _ -> assert false let is_toplevel mp = @@ -256,7 +262,7 @@ let safe_basename_of_global r = let last_chance r = try Nametab.basename_of_global r with Not_found -> - anomaly (Pp.str "Inductive object unknown to extraction and not globally visible") + anomaly (Pp.str "Inductive object unknown to extraction and not globally visible.") in match r with | ConstRef kn -> Label.to_id (con_label kn) @@ -293,7 +299,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref) (*S Warning and Error messages. *) -let err s = errorlabstrm "Extraction" s +let err s = user_err ~hdr:"Extraction" s let warn_extraction_axiom_to_realize = CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction" @@ -494,8 +500,7 @@ let my_bool_option name initval = let flag = ref initval in let access = fun () -> !flag in let _ = declare_bool_option - {optsync = true; - optdepr = false; + {optdepr = false; optname = "Extraction "^name; optkey = ["Extraction"; name]; optread = access; @@ -567,16 +572,14 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n let optims () = !opt_flag_ref let _ = declare_bool_option - {optsync = true; - optdepr = false; + {optdepr = false; optname = "Extraction Optimize"; optkey = ["Extraction"; "Optimize"]; optread = (fun () -> not (Int.equal !int_flag_ref 0)); optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))} let _ = declare_int_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "Extraction Flag"; optkey = ["Extraction";"Flag"]; optread = (fun _ -> Some !int_flag_ref); @@ -590,8 +593,7 @@ let conservative_types_ref = ref false let conservative_types () = !conservative_types_ref let _ = declare_bool_option - {optsync = true; - optdepr = false; + {optdepr = false; optname = "Extraction Conservative Types"; optkey = ["Extraction"; "Conservative"; "Types"]; optread = (fun () -> !conservative_types_ref); @@ -603,8 +605,7 @@ let file_comment_ref = ref "" let file_comment () = !file_comment_ref let _ = declare_string_option - {optsync = true; - optdepr = false; + {optdepr = false; optname = "Extraction File Comment"; optkey = ["Extraction"; "File"; "Comment"]; optread = (fun () -> !file_comment_ref); @@ -773,13 +774,11 @@ let file_of_modfile mp = | MPfile f -> Id.to_string (List.hd (DirPath.repr f)) | _ -> assert false in - let s = String.copy (string_of_modfile mp) in - if s.[0] != s0.[0] then s.[0] <- s0.[0]; - s + String.mapi (fun i c -> if i = 0 then s0.[0] else c) (string_of_modfile mp) let add_blacklist_entries l = blacklist_table := - List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s))) + List.fold_right (fun s -> Id.Set.add (Id.of_string (capitalize s))) l !blacklist_table (* Registration of operations for rollback. *) @@ -894,7 +893,7 @@ let extract_constant_inline inline r ids s = let extract_inductive r s l optstr = check_inside_section (); let g = Smartlocate.global_with_alias r in - Dumpglob.add_glob (loc_of_reference r) g; + Dumpglob.add_glob ?loc:(loc_of_reference r) g; match g with | IndRef ((kn,i) as ip) -> let mib = Global.lookup_mind kn in |