diff options
Diffstat (limited to 'plugins/extraction/table.ml')
-rw-r--r-- | plugins/extraction/table.ml | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index d6a334c5f..5837a7196 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -494,8 +494,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 +566,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 +587,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 +599,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); |