From 4563779bf990cf22d88474a68acf4eb9cfd8d173 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 4 Feb 2020 17:07:34 +0100 Subject: 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. --- plugins/cc/ccalgo.ml | 1 - plugins/extraction/table.ml | 5 ----- plugins/firstorder/g_ground.mlg | 1 - plugins/funind/indfun_common.ml | 3 --- plugins/ltac/g_ltac.mlg | 1 - plugins/ltac/profile_ltac.ml | 1 - plugins/ltac/tacinterp.ml | 2 -- plugins/ltac/tactic_debug.ml | 1 - plugins/ltac/tauto.ml | 1 - plugins/micromega/coq_micromega.ml | 7 ------- plugins/omega/coq_omega.ml | 5 ----- plugins/rtauto/proof_search.ml | 1 - plugins/rtauto/refl_tauto.ml | 2 -- plugins/ssr/ssrequality.ml | 3 +-- plugins/ssr/ssrfwd.ml | 3 +-- plugins/ssr/ssrparser.mlg | 6 ++---- plugins/ssr/ssrprinters.ml | 3 +-- plugins/ssrmatching/ssrmatching.ml | 3 +-- 18 files changed, 6 insertions(+), 43 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index fdc70ccaa8..f9078c4bdc 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -33,7 +33,6 @@ let debug x = let () = let gdopt= { optdepr=false; - optname="Congruence Verbose"; optkey=["Congruence";"Verbose"]; optread=(fun ()-> !cc_verbose); optwrite=(fun b -> cc_verbose := b)} 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) } diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 9d208e1c86..930801f6fd 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -36,7 +36,6 @@ let ground_depth=ref 3 let ()= let gdopt= { optdepr=false; - optname="Firstorder Depth"; optkey=["Firstorder";"Depth"]; optread=(fun ()->Some !ground_depth); optwrite= diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index bce09d8fbd..b2ee0f9370 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -320,7 +320,6 @@ open Goptions let functional_induction_rewrite_dependent_proofs_sig = { optdepr = false; - optname = "Functional Induction Rewrite Dependent"; optkey = ["Functional";"Induction";"Rewrite";"Dependent"]; optread = (fun () -> !functional_induction_rewrite_dependent_proofs); optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b) @@ -332,7 +331,6 @@ let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = t let function_debug_sig = { optdepr = false; - optname = "Function debug"; optkey = ["Function_debug"]; optread = (fun () -> !function_debug); optwrite = (fun b -> function_debug := b) @@ -416,7 +414,6 @@ let is_strict_tcc () = !strict_tcc let strict_tcc_sig = { optdepr = false; - optname = "Raw Function Tcc"; optkey = ["Function_raw_tcc"]; optread = (fun () -> !strict_tcc); optwrite = (fun b -> strict_tcc := b) diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 81a6651745..7ea843ca69 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -368,7 +368,6 @@ let print_info_trace = ref None let () = declare_int_option { optdepr = false; - optname = "print info trace"; optkey = ["Info" ; "Level"]; optread = (fun () -> !print_info_trace); optwrite = fun n -> print_info_trace := n; diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index fe5ebf1172..7529f9fce6 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -450,7 +450,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Ltac Profiling"; optkey = ["Ltac"; "Profiling"]; optread = get_profiling; optwrite = set_profiling } diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 98aa649b62..6e620b71db 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2082,7 +2082,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Ltac debug"; optkey = ["Ltac";"Debug"]; optread = (fun () -> get_debug () != Tactic_debug.DebugOff); optwrite = vernac_debug } @@ -2091,7 +2090,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Ltac Backtrace"; optkey = ["Ltac"; "Backtrace"]; optread = (fun () -> !log_trace); optwrite = (fun b -> log_trace := b) } diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 539536911c..0e9465839a 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -86,7 +86,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "Ltac batch debug"; optkey = ["Ltac";"Batch";"Debug"]; optread = (fun () -> !batch); optwrite = (fun x -> batch := x) } diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index ba759441e5..92110d7a43 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -68,7 +68,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "unfolding of not in intuition"; optkey = ["Intuition";"Negation";"Unfolding"]; optread = (fun () -> !negation_unfolding); optwrite = (:=) negation_unfolding } diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index cdadde8621..4b656f8e61 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -55,7 +55,6 @@ let use_csdp_cache = ref true let () = let int_opt l vref = { optdepr = false - ; optname = List.fold_right ( ^ ) l "" ; optkey = l ; optread = (fun () -> Some !vref) ; optwrite = @@ -63,42 +62,36 @@ let () = in let lia_enum_opt = { optdepr = false - ; optname = "Lia Enum" ; optkey = ["Lia"; "Enum"] ; optread = (fun () -> !lia_enum) ; optwrite = (fun x -> lia_enum := x) } in let solver_opt = { optdepr = false - ; optname = "Use the Simplex instead of Fourier elimination" ; optkey = ["Simplex"] ; optread = (fun () -> !Certificate.use_simplex) ; optwrite = (fun x -> Certificate.use_simplex := x) } in let dump_file_opt = { optdepr = false - ; optname = "Generate Coq goals in file from calls to 'lia' 'nia'" ; optkey = ["Dump"; "Arith"] ; optread = (fun () -> !Certificate.dump_file) ; optwrite = (fun x -> Certificate.dump_file := x) } in let lia_cache_opt = { optdepr = false - ; optname = "cache of lia (.lia.cache)" ; optkey = ["Lia"; "Cache"] ; optread = (fun () -> !use_lia_cache) ; optwrite = (fun x -> use_lia_cache := x) } in let nia_cache_opt = { optdepr = false - ; optname = "cache of nia (.nia.cache)" ; optkey = ["Nia"; "Cache"] ; optread = (fun () -> !use_nia_cache) ; optwrite = (fun x -> use_nia_cache := x) } in let nra_cache_opt = { optdepr = false - ; optname = "cache of nra (.nra.cache)" ; optkey = ["Nra"; "Cache"] ; optread = (fun () -> !use_nra_cache) ; optwrite = (fun x -> use_nra_cache := x) } diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 979e5bb8d8..118db01ecb 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -67,7 +67,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "Omega system time displaying flag"; optkey = ["Omega";"System"]; optread = read display_system_flag; optwrite = write display_system_flag } @@ -75,7 +74,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "Omega action display flag"; optkey = ["Omega";"Action"]; optread = read display_action_flag; optwrite = write display_action_flag } @@ -83,7 +81,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "Omega old style flag"; optkey = ["Omega";"OldStyle"]; optread = read old_style_flag; optwrite = write old_style_flag } @@ -91,7 +88,6 @@ let () = let () = declare_bool_option { optdepr = true; - optname = "Omega automatic reset of generated names"; optkey = ["Stable";"Omega"]; optread = read reset_flag; optwrite = write reset_flag } @@ -99,7 +95,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "Omega takes advantage of context variables with body"; optkey = ["Omega";"UseLocalDefs"]; optread = read letin_flag; optwrite = write letin_flag } diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 4cc32cfb26..ab34489de9 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -49,7 +49,6 @@ let pruning = ref true let opt_pruning= {optdepr=false; - optname="Rtauto Pruning"; optkey=["Rtauto";"Pruning"]; optread=(fun () -> !pruning); optwrite=(fun b -> pruning:=b)} diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 0c155c9d0a..b86c8d096c 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -227,7 +227,6 @@ let verbose = ref false let opt_verbose= {optdepr=false; - optname="Rtauto Verbose"; optkey=["Rtauto";"Verbose"]; optread=(fun () -> !verbose); optwrite=(fun b -> verbose:=b)} @@ -238,7 +237,6 @@ let check = ref false let opt_check= {optdepr=false; - optname="Rtauto Check"; optkey=["Rtauto";"Check"]; optread=(fun () -> !check); optwrite=(fun b -> check:=b)} diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index cdda84a18d..df001b6084 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -34,8 +34,7 @@ open Tacmach let ssroldreworder = Summary.ref ~name:"SSR:oldreworder" false let () = Goptions.(declare_bool_option - { optname = "ssreflect 1.3 compatibility flag"; - optkey = ["SsrOldRewriteGoalsOrder"]; + { optkey = ["SsrOldRewriteGoalsOrder"]; optread = (fun _ -> !ssroldreworder); optdepr = false; optwrite = (fun b -> ssroldreworder := b) }) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index f486d1e457..235dfc257d 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -69,8 +69,7 @@ let ssrhaveNOtcresolution = Summary.ref ~name:"SSR:havenotcresolution" false let () = Goptions.(declare_bool_option - { optname = "have type classes"; - optkey = ["SsrHave";"NoTCResolution"]; + { optkey = ["SsrHave";"NoTCResolution"]; optread = (fun _ -> !ssrhaveNOtcresolution); optdepr = false; optwrite = (fun b -> ssrhaveNOtcresolution := b); diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 22325f3fc3..21b832a326 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -1662,8 +1662,7 @@ let ssr_reserved_ids = Summary.ref ~name:"SSR:idents" true let () = Goptions.(declare_bool_option - { optname = "ssreflect identifiers"; - optkey = ["SsrIdents"]; + { optkey = ["SsrIdents"]; optdepr = false; optread = (fun _ -> !ssr_reserved_ids); optwrite = (fun b -> ssr_reserved_ids := b) @@ -2395,8 +2394,7 @@ let ssr_rw_syntax = Summary.ref ~name:"SSR:rewrite" true let () = Goptions.(declare_bool_option - { optname = "ssreflect rewrite"; - optkey = ["SsrRewrite"]; + { optkey = ["SsrRewrite"]; optread = (fun _ -> !ssr_rw_syntax); optdepr = false; optwrite = (fun b -> ssr_rw_syntax := b) }) diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml index f0aed1a934..22250202b5 100644 --- a/plugins/ssr/ssrprinters.ml +++ b/plugins/ssr/ssrprinters.ml @@ -134,8 +134,7 @@ let ppdebug_ref = ref (fun _ -> ()) let ssr_pp s = Feedback.msg_debug (str"SSR: "++Lazy.force s) let () = Goptions.(declare_bool_option - { optname = "ssreflect debugging"; - optkey = ["Debug";"Ssreflect"]; + { optkey = ["Debug";"Ssreflect"]; optdepr = false; optread = (fun _ -> !ppdebug_ref == ssr_pp); optwrite = (fun b -> diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 6cb464918a..2f6d69935a 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -55,8 +55,7 @@ let debug b = if b then pp_ref := ssr_pp else pp_ref := fun _ -> () let _ = Goptions.declare_bool_option - { Goptions.optname = "ssrmatching debugging"; - Goptions.optkey = ["Debug";"SsrMatching"]; + { Goptions.optkey = ["Debug";"SsrMatching"]; Goptions.optdepr = false; Goptions.optread = (fun _ -> !pp_ref == ssr_pp); Goptions.optwrite = debug } -- cgit v1.2.3