diff options
| author | Gaëtan Gilbert | 2018-11-21 20:00:46 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-23 13:21:31 +0100 |
| commit | 74038abdd41161a4c4b1eba5dbbd83f5c0301bf3 (patch) | |
| tree | f1932098c3b1320ebf8629c2b22f9437608e6fcf /plugins/extraction | |
| parent | 99d129b8e4e7fcde8c848520463c4e8c7d8bdc11 (diff) | |
s/let _ =/let () =/ in some places (mostly goptions related)
Diffstat (limited to 'plugins/extraction')
| -rw-r--r-- | plugins/extraction/table.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index f6eea3c5c4..16890ea260 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -500,7 +500,7 @@ let info_file f = let my_bool_option name initval = let flag = ref initval in let access = fun () -> !flag in - let _ = declare_bool_option + let () = declare_bool_option {optdepr = false; optname = "Extraction "^name; optkey = ["Extraction"; name]; @@ -572,14 +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 +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 +let () = declare_int_option { optdepr = false; optname = "Extraction Flag"; optkey = ["Extraction";"Flag"]; @@ -593,7 +593,7 @@ let _ = declare_int_option let conservative_types_ref = ref false let conservative_types () = !conservative_types_ref -let _ = declare_bool_option +let () = declare_bool_option {optdepr = false; optname = "Extraction Conservative Types"; optkey = ["Extraction"; "Conservative"; "Types"]; @@ -605,7 +605,7 @@ let _ = declare_bool_option let file_comment_ref = ref "" let file_comment () = !file_comment_ref -let _ = declare_string_option +let () = declare_string_option {optdepr = false; optname = "Extraction File Comment"; optkey = ["Extraction"; "File"; "Comment"]; |