diff options
| author | Gaëtan Gilbert | 2020-02-04 17:07:34 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-12 16:23:49 +0100 |
| commit | 4563779bf990cf22d88474a68acf4eb9cfd8d173 (patch) | |
| tree | c5333864070ccc9b8746799e9236ba90ef1a432d /plugins/extraction | |
| parent | 6c1de3455d5cd79958a8e26ac728f7d5d1b8d025 (diff) | |
Remove Goptions.opt_name field
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/table.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 7b64706138..9d07cd7d93 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -503,7 +503,6 @@ let my_bool_option name initval = let access = fun () -> !flag in let () = declare_bool_option {optdepr = false; - optname = "Extraction "^name; optkey = ["Extraction"; name]; optread = access; optwrite = (:=) flag } @@ -575,14 +574,12 @@ let optims () = !opt_flag_ref let () = declare_bool_option {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 { optdepr = false; - optname = "Extraction Flag"; optkey = ["Extraction";"Flag"]; optread = (fun _ -> Some !int_flag_ref); optwrite = (function @@ -596,7 +593,6 @@ let conservative_types () = !conservative_types_ref let () = declare_bool_option {optdepr = false; - optname = "Extraction Conservative Types"; optkey = ["Extraction"; "Conservative"; "Types"]; optread = (fun () -> !conservative_types_ref); optwrite = (fun b -> conservative_types_ref := b) } @@ -608,7 +604,6 @@ let file_comment () = !file_comment_ref let () = declare_string_option {optdepr = false; - optname = "Extraction File Comment"; optkey = ["Extraction"; "File"; "Comment"]; optread = (fun () -> !file_comment_ref); optwrite = (fun s -> file_comment_ref := s) } |