diff options
65 files changed, 48 insertions, 192 deletions
diff --git a/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh b/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh new file mode 100644 index 0000000000..f2a431978d --- /dev/null +++ b/dev/ci/user-overlays/11521-SkySkimmer-no-optname.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "11521" ] || [ "$CI_BRANCH" = "no-optname" ]; then + + coqhammer_CI_REF=no-optname + coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer + + equations_CI_REF=no-optname + equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations + + unicoq_CI_REF=no-optname + unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq + + paramcoq_CI_REF=no-optname + paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq + +fi diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index b0197c500c..f706633da9 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -35,6 +35,11 @@ tactics for solving arithmetic goals over :math:`\mathbb{Q}`, use the Simplex method for solving linear goals. If it is not set, the decision procedures are using Fourier elimination. +.. opt:: Dump Arith + + This option (unset by default) may be set to a file path where + debug info will be written. + .. cmd:: Show Lia Profile This command prints some statistics about the amount of pivoting diff --git a/engine/namegen.ml b/engine/namegen.ml index 56277e8092..bcc8c34a4d 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -216,7 +216,6 @@ let it_mkLambda_or_LetIn_name env sigma b hyps = let get_mangle_names = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"mangle auto-generated names" ~key:["Mangle";"Names"] ~value:false @@ -227,7 +226,6 @@ let set_prefix x = mangle_names_prefix := forget_subscript x let () = Goptions.( declare_string_option { optdepr = false; - optname = "mangled names prefix"; optkey = ["Mangle";"Names";"Prefix"]; optread = (fun () -> Id.to_string !mangle_names_prefix); optwrite = begin fun x -> diff --git a/engine/uState.ml b/engine/uState.ml index 3546ece581..2eaa202246 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -53,7 +53,7 @@ let empty = uctx_weak_constraints = UPairSet.empty; } let elaboration_sprop_cumul = - Goptions.declare_bool_option_and_ref ~depr:false ~name:"SProp cumulativity during elaboration" + Goptions.declare_bool_option_and_ref ~depr:false ~key:["Elaboration";"StrictProp";"Cumulativity"] ~value:true let make ~lbound u = diff --git a/engine/univMinim.ml b/engine/univMinim.ml index fc0770cf75..53ff041fa5 100644 --- a/engine/univMinim.ml +++ b/engine/univMinim.ml @@ -15,7 +15,6 @@ open UnivSubst let get_set_minimization = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"minimization to Set" ~key:["Universe";"Minimization";"ToSet"] ~value:true diff --git a/ide/idetop.ml b/ide/idetop.ml index 7d92cff365..ae2301a0a7 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -360,7 +360,6 @@ let import_option_value = function let export_option_state s = { Interface.opt_sync = true; Interface.opt_depr = s.Goptions.opt_depr; - Interface.opt_name = s.Goptions.opt_name; Interface.opt_value = export_option_value s.Goptions.opt_value; } diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml index 362833743e..be5e305ad3 100644 --- a/ide/protocol/interface.ml +++ b/ide/protocol/interface.ml @@ -71,8 +71,6 @@ type option_state = { (** Whether an option is synchronous *) opt_depr : bool; (** Whether an option is deprecated *) - opt_name : string; - (** A short string that is displayed when using [Test] *) opt_value : option_value; (** The current value of the option *) } diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml index cad65cc5d6..a2c80ea118 100644 --- a/ide/protocol/xmlprotocol.ml +++ b/ide/protocol/xmlprotocol.ml @@ -79,13 +79,11 @@ let of_option_state s = Element ("option_state", [], [ of_bool s.opt_sync; of_bool s.opt_depr; - of_string s.opt_name; of_option_value s.opt_value]) let to_option_state = function - | Element ("option_state", [], [sync; depr; name; value]) -> { + | Element ("option_state", [], [sync; depr; value]) -> { opt_sync = to_bool sync; opt_depr = to_bool depr; - opt_name = to_string name; opt_value = to_option_value value } | x -> raise (Marshal_error("option_state",x)) @@ -429,8 +427,8 @@ end = struct | StringOptValue (Some s) -> s | BoolValue b -> if b then "true" else "false" let pr_option_state (s : option_state) = - Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n" - s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value) + Printf.sprintf "sync := %b; depr := %b; value := %s\n" + s.opt_sync s.opt_depr (pr_option_value s.opt_value) let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]" let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")" let pr_coq_object (o : 'a coq_object) = "FIXME" @@ -513,7 +511,7 @@ end = struct "type which contains a flattened n-tuple. We provide one example.\n"); Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state) (pr_xml (of_option_state { opt_sync = true; opt_depr = false; - opt_name = "name1"; opt_value = IntValue (Some 37) })); + opt_value = IntValue (Some 37) })); end open ReifType diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c55e17e7a3..c198c4eb9b 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -194,7 +194,6 @@ let without_specific_symbols l = let get_record_print = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"record printing" ~key:["Printing";"Records"] ~value:true diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 2ceea58297..b2c572d290 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1615,7 +1615,6 @@ let is_non_zero_pat c = match c with let get_asymmetric_patterns = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"no parameters in constructors" ~key:["Asymmetric";"Patterns"] ~value:false diff --git a/library/goptions.ml b/library/goptions.ml index 6e53bed349..616f6edf72 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -27,7 +27,6 @@ type option_value = (** Summary of an option status *) type option_state = { opt_depr : bool; - opt_name : string; opt_value : option_value; } @@ -190,7 +189,6 @@ module MakeRefTable = type 'a option_sig = { optdepr : bool; - optname : string; optkey : option_name; optread : unit -> 'a; optwrite : 'a -> unit } @@ -229,7 +227,7 @@ let warn_deprecated_option = strbrk " is deprecated") let declare_option cast uncast append ?(preprocess = fun x -> x) - { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = + { optdepr=depr; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in let change = @@ -275,7 +273,7 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) let cread () = cast (read ()) in let cwrite l v = warn (); change l OptSet (uncast v) in let cappend l v = warn (); change l OptAppend (uncast v) in - value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab + value_tab := OptionMap.add key (depr, (cread,cwrite,cappend)) !value_tab let declare_int_option = declare_option @@ -298,13 +296,12 @@ let declare_stringopt_option = (function StringOptValue v -> v | _ -> anomaly (Pp.str "async_option.")) (fun _ _ -> anomaly (Pp.str "async_option.")) -let declare_bool_option_and_ref ~depr ~name ~key ~(value:bool) = +let declare_bool_option_and_ref ~depr ~key ~(value:bool) = let r_opt = ref value in let optwrite v = r_opt := v in let optread () = !r_opt in let _ = declare_bool_option { optdepr = depr; - optname = name; optkey = key; optread; optwrite } in @@ -323,7 +320,7 @@ let set_option_value ?(locality = OptDefault) check_and_cast key v = let opt = try Some (get_option key) with Not_found -> None in match opt with | None -> warn_unknown_option key - | Some (name, depr, (read,write,append)) -> + | Some (depr, (read,write,append)) -> write locality (check_and_cast v (read ())) let show_value_type = function @@ -373,7 +370,7 @@ let set_string_option_append_value_gen ?(locality = OptDefault) key v = let opt = try Some (get_option key) with Not_found -> None in match opt with | None -> warn_unknown_option key - | Some (name, depr, (read,write,append)) -> + | Some (depr, (read,write,append)) -> append locality (check_string_value v (read ())) let set_int_option_value opt v = set_int_option_value_gen opt v @@ -382,7 +379,7 @@ let set_string_option_value opt v = set_string_option_value_gen opt v (* Printing options/tables *) -let msg_option_value (name,v) = +let msg_option_value v = match v with | BoolValue true -> str "on" | BoolValue false -> str "off" @@ -394,19 +391,18 @@ let msg_option_value (name,v) = (* | IdentValue r -> pr_global_env Id.Set.empty r *) let print_option_value key = - let (name, depr, (read,_,_)) = get_option key in + let (depr, (read,_,_)) = get_option key in let s = read () in match s with | BoolValue b -> - Feedback.msg_notice (str "The " ++ str name ++ str " mode is " ++ str (if b then "on" else "off")) + Feedback.msg_notice (prlist_with_sep spc str key ++ str " is " ++ str (if b then "on" else "off")) | _ -> - Feedback.msg_notice (str "Current value of " ++ str name ++ str " is " ++ msg_option_value (name, s)) + Feedback.msg_notice (str "Current value of " ++ prlist_with_sep spc str key ++ str " is " ++ msg_option_value s) let get_tables () = let tables = !value_tab in - let fold key (name, depr, (read,_,_)) accu = + let fold key (depr, (read,_,_)) accu = let state = { - opt_name = name; opt_depr = depr; opt_value = read (); } in @@ -415,15 +411,15 @@ let get_tables () = OptionMap.fold fold tables OptionMap.empty let print_tables () = - let print_option key name value depr = - let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value (name, value) in + let print_option key value depr = + let msg = str " " ++ str (nickname key) ++ str ": " ++ msg_option_value value in if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in str "Options:" ++ fnl () ++ OptionMap.fold - (fun key (name, depr, (read,_,_)) p -> - p ++ print_option key name (read ()) depr) + (fun key (depr, (read,_,_)) p -> + p ++ print_option key (read ()) depr) !value_tab (mt ()) ++ str "Tables:" ++ fnl () ++ List.fold_right diff --git a/library/goptions.mli b/library/goptions.mli index 29af196654..e3791dffb1 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -111,8 +111,6 @@ end type 'a option_sig = { optdepr : bool; (** whether the option is DEPRECATED *) - optname : string; - (** a short string describing the option *) optkey : option_name; (** the low-level name of this option *) optread : unit -> 'a; @@ -133,7 +131,7 @@ val declare_stringopt_option: ?preprocess:(string option -> string option) -> (** Helper to declare a reference controlled by an option. Read-only as to avoid races. *) -val declare_bool_option_and_ref : depr:bool -> name:string -> key:option_name -> value:bool -> (unit -> bool) +val declare_bool_option_and_ref : depr:bool -> key:option_name -> value:bool -> (unit -> bool) (** {6 Special functions supposed to be used only in vernacentries.ml } *) @@ -181,7 +179,6 @@ val set_option_value : ?locality:option_locality -> (** Summary of an option status *) type option_state = { opt_depr : bool; - opt_name : string; opt_value : option_value; } 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 915531cf3c..e45bae19ca 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -54,8 +54,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 } diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 2b7ccbbcad..11c97221ec 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -196,7 +196,6 @@ let cofixp_reducible flgs _ stk = let get_debug_cbv = Goptions.declare_bool_option_and_ref ~depr:false ~value:false - ~name:"cbv visited constants display" ~key:["Debug";"Cbv"] (* Reduction of primitives *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3c7f9a8f00..c4aa3479bf 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -36,7 +36,6 @@ open Globnames let get_use_typeclasses_for_conversion = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"use typeclass resolution during conversion" ~key:["Typeclass"; "Resolution"; "For"; "Conversion"] ~value:true diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index b042437a22..83078660c5 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -228,7 +228,6 @@ let force_wildcard () = !wildcard_value let () = declare_bool_option { optdepr = false; - optname = "forced wildcard"; optkey = ["Printing";"Wildcard"]; optread = force_wildcard; optwrite = (:=) wildcard_value } @@ -237,7 +236,6 @@ let fast_name_generation = ref false let () = declare_bool_option { optdepr = false; - optname = "fast bound name generation algorithm"; optkey = ["Fast";"Name";"Printing"]; optread = (fun () -> !fast_name_generation); optwrite = (:=) fast_name_generation; @@ -248,7 +246,6 @@ let synthetize_type () = !synth_type_value let () = declare_bool_option { optdepr = false; - optname = "pattern matching return type synthesizability"; optkey = ["Printing";"Synth"]; optread = synthetize_type; optwrite = (:=) synth_type_value } @@ -258,7 +255,6 @@ let reverse_matching () = !reverse_matching_value let () = declare_bool_option { optdepr = false; - optname = "pattern-matching reversibility"; optkey = ["Printing";"Matching"]; optread = reverse_matching; optwrite = (:=) reverse_matching_value } @@ -268,7 +264,6 @@ let print_primproj_params () = !print_primproj_params_value let () = declare_bool_option { optdepr = false; - optname = "printing of primitive projection parameters"; optkey = ["Printing";"Primitive";"Projection";"Parameters"]; optread = print_primproj_params; optwrite = (:=) print_primproj_params_value } @@ -348,7 +343,6 @@ let print_factorize_match_patterns = ref true let () = declare_bool_option { optdepr = false; - optname = "factorization of \"match\" patterns in printing"; optkey = ["Printing";"Factorizable";"Match";"Patterns"]; optread = (fun () -> !print_factorize_match_patterns); optwrite = (fun b -> print_factorize_match_patterns := b) } @@ -358,7 +352,6 @@ let print_allow_match_default_clause = ref true let () = declare_bool_option { optdepr = false; - optname = "possible use of \"match\" default pattern in printing"; optkey = ["Printing";"Allow";"Match";"Default";"Clause"]; optread = (fun () -> !print_allow_match_default_clause); optwrite = (fun b -> print_allow_match_default_clause := b) } diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index c21af82659..c67019c7ac 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -50,8 +50,6 @@ let default_flags env = let debug_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print states sent to Evarconv unification"; optkey = ["Debug";"Unification"]; optread = (fun () -> !debug_unification); optwrite = (fun a -> debug_unification:=a); @@ -60,8 +58,6 @@ let () = Goptions.(declare_bool_option { let debug_ho_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print higher-order unification debug information"; optkey = ["Debug";"HO";"Unification"]; optread = (fun () -> !debug_ho_unification); optwrite = (fun a -> debug_ho_unification:=a); diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2d98d48aa0..ac1a4e88ef 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -125,7 +125,6 @@ let esearch_guard ?loc env sigma indexes fix = let is_strict_universe_declarations = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"strict universe declaration" ~key:["Strict";"Universe";"Declaration"] ~value:true diff --git a/pretyping/program.ml b/pretyping/program.ml index 1bc31646dd..9c478844aa 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -78,7 +78,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "preferred transparency of Program obligations"; optkey = ["Transparent";"Obligations"]; optread = get_proofs_transparency; optwrite = set_proofs_transparency; } @@ -86,7 +85,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "program cases"; optkey = ["Program";"Cases"]; optread = (fun () -> !program_cases); optwrite = (:=) program_cases } @@ -94,7 +92,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "program generalized coercion"; optkey = ["Program";"Generalized";"Coercion"]; optread = (fun () -> !program_generalized_coercion); optwrite = (:=) program_generalized_coercion } diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d5beebe690..bfee07e7f0 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -32,8 +32,6 @@ exception Elimconst let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Generate weak constraints between Irrelevant universes"; optkey = ["Cumulativity";"Weak";"Constraints"]; optread = (fun () -> not !UState.drop_weak_constraints); optwrite = (fun a -> UState.drop_weak_constraints:=not a); @@ -972,8 +970,6 @@ module CredNative = RedNative(CNativeEntries) let debug_RAKAM = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print states of the Reductionops abstract machine"; optkey = ["Debug";"RAKAM"]; optread = (fun () -> !debug_RAKAM); optwrite = (fun a -> debug_RAKAM:=a); diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d5c8c3bd19..aa2e96c2d7 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -31,7 +31,6 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen let get_typeclasses_unique_solutions = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"check that typeclasses proof search returns unique solutions" ~key:["Typeclasses";"Unique";"Solutions"] ~value:false diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 2157c4ef6a..5b87603d54 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -46,7 +46,6 @@ module NamedDecl = Context.Named.Declaration let keyed_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Unification is keyed"; optkey = ["Keyed";"Unification"]; optread = (fun () -> !keyed_unification); optwrite = (fun a -> keyed_unification:=a); @@ -57,8 +56,6 @@ let is_keyed_unification () = !keyed_unification let debug_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Print states sent to tactic unification"; optkey = ["Debug";"Tactic";"Unification"]; optread = (fun () -> !debug_unification); optwrite = (fun a -> debug_unification:=a); diff --git a/printing/printer.ml b/printing/printer.ml index 8af4d1d932..cc83a1dde0 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -38,7 +38,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "printing of unfocused goal"; optkey = ["Printing";"Unfocused"]; optread = (fun () -> !enable_unfocused_goal_printing); optwrite = (fun b -> enable_unfocused_goal_printing:=b) } @@ -49,7 +48,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "printing of goal tags"; optkey = ["Printing";"Goal";"Tags"]; optread = (fun () -> !enable_goal_tags_printing); optwrite = (fun b -> enable_goal_tags_printing:=b) } @@ -59,7 +57,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "printing of goal names"; optkey = ["Printing";"Goal";"Names"]; optread = (fun () -> !enable_goal_names_printing); optwrite = (fun b -> enable_goal_names_printing:=b) } @@ -416,7 +413,6 @@ let () = let open Goptions in declare_int_option { optdepr = false; - optname = "the hypotheses limit"; optkey = ["Hyps";"Limit"]; optread = (fun () -> !print_hyps_limit); optwrite = (fun x -> print_hyps_limit := x) } @@ -625,7 +621,6 @@ let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "Printing Dependent Evars Line"; optkey = ["Printing";"Dependent";"Evars";"Line"]; optread = (fun () -> !should_print_dependent_evars); optwrite = (fun v -> should_print_dependent_evars := v) } diff --git a/printing/printmod.ml b/printing/printmod.ml index 85bb287c22..a5fd7f69ed 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -44,7 +44,6 @@ let short = ref false let () = declare_bool_option { optdepr = false; - optname = "short module printing"; optkey = ["Short";"Module";"Printing"]; optread = (fun () -> !short) ; optwrite = ((:=) short) } diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index dec87f8071..d93dd15f91 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -69,7 +69,6 @@ let write_diffs_option opt = let () = Goptions.(declare_string_option { optdepr = false; - optname = "show diffs in proofs"; optkey = ["Diffs"]; optread = read_diffs_option; optwrite = write_diffs_option diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml index a6e27c238f..36b50d9e9f 100644 --- a/proofs/goal_select.ml +++ b/proofs/goal_select.ml @@ -56,7 +56,6 @@ let parse_goal_selector = function let () = let open Goptions in declare_string_option { optdepr = false; - optname = "default goal selector" ; optkey = ["Default";"Goal";"Selector"] ; optread = begin fun () -> Pp.string_of_ppcmds diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index 61e8741973..3ff0533b6b 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -179,7 +179,6 @@ let current_behavior = ref Strict.strict let () = Goptions.(declare_string_option { optdepr = false; - optname = "bullet behavior"; optkey = ["Bullet";"Behavior"]; optread = begin fun () -> (!current_behavior).name diff --git a/stm/stm.ml b/stm/stm.ml index 4c539684e3..5402600041 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2849,7 +2849,6 @@ let process_back_meta_command ~newtip ~head oid aast = let get_allow_nested_proofs = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"Nested Proofs Allowed" ~key:Vernac_classifier.stm_allow_nested_proofs_option_name ~value:false diff --git a/tactics/auto.ml b/tactics/auto.ml index 9c1a975330..1dde820075 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -177,7 +177,6 @@ let global_info_auto = ref false let add_option ls refe = Goptions.(declare_bool_option { optdepr = false; - optname = String.concat " " ls; optkey = ls; optread = (fun () -> !refe); optwrite = (:=) refe }) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ccd88d2c35..28feeecb86 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -83,8 +83,6 @@ open Goptions let () = declare_bool_option { optdepr = false; - optname = "do typeclass search avoiding eta-expansions " ^ - " in proof terms (expensive)"; optkey = ["Typeclasses";"Limit";"Intros"]; optread = get_typeclasses_limit_intros; optwrite = set_typeclasses_limit_intros; } @@ -92,7 +90,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "during typeclass resolution, solve instances according to their dependency order"; optkey = ["Typeclasses";"Dependency";"Order"]; optread = get_typeclasses_dependency_order; optwrite = set_typeclasses_dependency_order; } @@ -100,7 +97,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "use iterative deepening strategy"; optkey = ["Typeclasses";"Iterative";"Deepening"]; optread = get_typeclasses_iterative_deepening; optwrite = set_typeclasses_iterative_deepening; } @@ -108,7 +104,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "compat"; optkey = ["Typeclasses";"Filtered";"Unification"]; optread = get_typeclasses_filtered_unification; optwrite = set_typeclasses_filtered_unification; } @@ -116,7 +111,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "debug output for typeclasses proof search"; optkey = ["Typeclasses";"Debug"]; optread = get_typeclasses_debug; optwrite = set_typeclasses_debug; } @@ -124,7 +118,6 @@ let () = let _ = declare_int_option { optdepr = false; - optname = "verbosity of debug output for typeclasses proof search"; optkey = ["Typeclasses";"Debug";"Verbosity"]; optread = get_typeclasses_verbose; optwrite = set_typeclasses_verbose; } @@ -132,7 +125,6 @@ let _ = let () = declare_int_option { optdepr = false; - optname = "depth for typeclasses proof search"; optkey = ["Typeclasses";"Depth"]; optread = get_typeclasses_depth; optwrite = set_typeclasses_depth; } diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 80ca124912..9a1e6a6736 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -331,7 +331,6 @@ let global_info_eauto = ref false let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Debug Eauto"; optkey = ["Debug";"Eauto"]; optread = (fun () -> !global_debug_eauto); optwrite = (:=) global_debug_eauto }) @@ -339,7 +338,6 @@ let () = let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Info Eauto"; optkey = ["Info";"Eauto"]; optread = (fun () -> !global_info_eauto); optwrite = (:=) global_info_eauto }) diff --git a/tactics/equality.ml b/tactics/equality.ml index 9ef5f478d3..7393454ba9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -72,7 +72,6 @@ let use_injection_in_context = function let () = declare_bool_option { optdepr = false; - optname = "injection in context"; optkey = ["Structural";"Injection"]; optread = (fun () -> !injection_in_context) ; optwrite = (fun b -> injection_in_context := b) } @@ -734,7 +733,6 @@ let keep_proof_equalities_for_injection = ref false let () = declare_bool_option { optdepr = false; - optname = "injection on prop arguments"; optkey = ["Keep";"Proof";"Equalities"]; optread = (fun () -> !keep_proof_equalities_for_injection) ; optwrite = (fun b -> keep_proof_equalities_for_injection := b) } @@ -1686,7 +1684,6 @@ let regular_subst_tactic = ref true let () = declare_bool_option { optdepr = false; - optname = "more regular behavior of tactic subst"; optkey = ["Regular";"Subst";"Tactic"]; optread = (fun () -> !regular_subst_tactic); optwrite = (:=) regular_subst_tactic } diff --git a/tactics/hints.ml b/tactics/hints.ml index 73e8331bcb..86aa046586 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -205,7 +205,6 @@ let write_warn_hint = function let () = Goptions.(declare_string_option { optdepr = false; - optname = "behavior of non-imported hints"; optkey = ["Loose"; "Hint"; "Behavior"]; optread = read_warn_hint; optwrite = write_warn_hint; diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml index a4a06873b8..72204e1d24 100644 --- a/tactics/pfedit.ml +++ b/tactics/pfedit.ml @@ -17,7 +17,6 @@ open Evd let use_unification_heuristics_ref = ref true let () = Goptions.(declare_bool_option { optdepr = false; - optname = "Solve unification constraints at every \".\""; optkey = ["Solve";"Unification";"Constraints"]; optread = (fun () -> !use_unification_heuristics_ref); optwrite = (fun a -> use_unification_heuristics_ref:=a); diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml index b1fd34e43c..4c470519d6 100644 --- a/tactics/proof_global.ml +++ b/tactics/proof_global.ml @@ -143,7 +143,6 @@ let private_poly_univs = let b = ref true in let _ = Goptions.(declare_bool_option { optdepr = false; - optname = "use private polymorphic universes for Qed constants"; optkey = ["Private";"Polymorphic";"Universes"]; optread = (fun () -> !b); optwrite = ((:=) b); diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml index fc7b126ee5..a30c877435 100644 --- a/tactics/redexpr.ml +++ b/tactics/redexpr.ml @@ -56,8 +56,6 @@ let strong_cbn flags = let simplIsCbn = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; - optname = - "Plug the simpl tactic to the new cbn mechanism"; optkey = ["SimplIsCbn"]; optread = (fun () -> !simplIsCbn); optwrite = (fun a -> simplIsCbn:=a); diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2d900a237a..8371da76b2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -67,7 +67,6 @@ let use_clear_hyp_by_default () = !clear_hyp_by_default let () = declare_bool_option { optdepr = false; - optname = "default clearing of hypotheses after use"; optkey = ["Default";"Clearing";"Used";"Hypotheses"]; optread = (fun () -> !clear_hyp_by_default) ; optwrite = (fun b -> clear_hyp_by_default := b) } @@ -83,7 +82,6 @@ let accept_universal_lemma_under_conjunctions () = let () = declare_bool_option { optdepr = false; - optname = "trivial unification in tactics applying under conjunctions"; optkey = ["Universal";"Lemma";"Under";"Conjunction"]; optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } @@ -102,7 +100,6 @@ let use_bracketing_last_or_and_intro_pattern () = let () = declare_bool_option { optdepr = true; - optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; optread = (fun () -> !bracketing_last_or_and_intro_pattern); optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) } diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 5499ae0fa3..e4508e9bfc 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -368,7 +368,7 @@ let top_goal_print ~doc c oldp newp = let exit_on_error = let open Goptions in - declare_bool_option_and_ref ~depr:false ~name:"coqtop-exit-on-error" ~key:["Coqtop";"Exit";"On";"Error"] + declare_bool_option_and_ref ~depr:false ~key:["Coqtop";"Exit";"On";"Error"] ~value:false (* XXX: This is duplicated with Vernacentries.show_proof , at some diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index bcc5f54505..d6db4a735c 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -824,7 +824,6 @@ let register_struct ?local str = match str with let _ = Goptions.declare_bool_option { Goptions.optdepr = false; - Goptions.optname = "print Ltac2 backtrace"; Goptions.optkey = ["Ltac2"; "Backtrace"]; Goptions.optread = (fun () -> !Tac2interp.print_ltac2_backtrace); Goptions.optwrite = (fun b -> Tac2interp.print_ltac2_backtrace := b); diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 68d2c3a00d..194308b77f 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -154,7 +154,6 @@ let program_mode = ref false let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "use of the program extension"; optkey = program_mode_option_name; optread = (fun () -> !program_mode); optwrite = (fun b -> program_mode:=b) } @@ -188,7 +187,6 @@ let is_universe_polymorphism = let () = let open Goptions in declare_bool_option { optdepr = false; - optname = "universe polymorphism"; optkey = universe_polymorphism_option_name; optread = (fun () -> !b); optwrite = ((:=) b) } diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index dce0a70f72..d711c9aea0 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -42,7 +42,6 @@ let should_auto_template = let auto = ref true in let () = declare_bool_option { optdepr = false; - optname = "Automatically make some inductive types template polymorphic"; optkey = ["Auto";"Template";"Polymorphism"]; optread = (fun () -> !auto); optwrite = (fun b -> auto := b); } diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml index b56b9c8ce2..dcb28b898f 100644 --- a/vernac/declareObl.ml +++ b/vernac/declareObl.ml @@ -56,7 +56,7 @@ type program_info = let get_shrink_obligations = Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *) - ~name:"Shrinking of Program obligations" ~key:["Shrink"; "Obligations"] + ~key:["Shrink"; "Obligations"] ~value:true (* XXX: Is this the right place for this? *) @@ -133,7 +133,6 @@ let add_hint local prg cst = let get_hide_obligations = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"Hidding of Program obligations" ~key:["Hide"; "Obligations"] ~value:false diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 2f0b1062a7..227d2f1554 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -44,7 +44,6 @@ let elim_flag = ref true let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of induction schemes"; optkey = ["Elimination";"Schemes"]; optread = (fun () -> !elim_flag) ; optwrite = (fun b -> elim_flag := b) } @@ -53,7 +52,6 @@ let bifinite_elim_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of induction schemes for non-recursive types"; optkey = ["Nonrecursive";"Elimination";"Schemes"]; optread = (fun () -> !bifinite_elim_flag) ; optwrite = (fun b -> bifinite_elim_flag := b) } @@ -62,7 +60,6 @@ let case_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of case analysis schemes"; optkey = ["Case";"Analysis";"Schemes"]; optread = (fun () -> !case_flag) ; optwrite = (fun b -> case_flag := b) } @@ -71,7 +68,6 @@ let eq_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of boolean equality"; optkey = ["Boolean";"Equality";"Schemes"]; optread = (fun () -> !eq_flag) ; optwrite = (fun b -> eq_flag := b) } @@ -82,7 +78,6 @@ let eq_dec_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "automatic declaration of decidable equality"; optkey = ["Decidable";"Equality";"Schemes"]; optread = (fun () -> !eq_dec_flag) ; optwrite = (fun b -> eq_dec_flag := b) } @@ -91,7 +86,6 @@ let rewriting_flag = ref false let () = declare_bool_option { optdepr = false; - optname ="automatic declaration of rewriting schemes for equality types"; optkey = ["Rewriting";"Schemes"]; optread = (fun () -> !rewriting_flag) ; optwrite = (fun b -> rewriting_flag := b) } diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 865eded545..f7606f4ede 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -268,7 +268,6 @@ let warn_let_as_axiom = let get_keep_admitted_vars = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"keep section variables in admitted proofs" ~key:["Keep"; "Admitted"; "Variables"] ~value:true diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index cfb3248c7b..b329463cb0 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -140,7 +140,6 @@ let suggest_proof_using = ref false let () = Goptions.(declare_bool_option { optdepr = false; - optname = "suggest Proof using"; optkey = ["Suggest";"Proof";"Using"]; optread = (fun () -> !suggest_proof_using); optwrite = ((:=) suggest_proof_using) }) @@ -176,7 +175,6 @@ let proof_using_opt_name = ["Default";"Proof";"Using"] let () = Goptions.(declare_stringopt_option { optdepr = false; - optname = "default value for Proof using"; optkey = proof_using_opt_name; optread = (fun () -> Option.map using_to_string !value); optwrite = (fun b -> value := Option.map using_from_string b); diff --git a/vernac/record.ml b/vernac/record.ml index f6945838d7..27bd390714 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -39,7 +39,6 @@ let primitive_flag = ref false let () = declare_bool_option { optdepr = false; - optname = "use of primitive projections"; optkey = ["Primitive";"Projections"]; optread = (fun () -> !primitive_flag) ; optwrite = (fun b -> primitive_flag := b) } @@ -48,7 +47,6 @@ let typeclasses_strict = ref false let () = declare_bool_option { optdepr = false; - optname = "strict typeclass resolution"; optkey = ["Typeclasses";"Strict";"Resolution"]; optread = (fun () -> !typeclasses_strict); optwrite = (fun b -> typeclasses_strict := b); } @@ -57,7 +55,6 @@ let typeclasses_unique = ref false let () = declare_bool_option { optdepr = false; - optname = "unique typeclass instances"; optkey = ["Typeclasses";"Unique";"Instances"]; optread = (fun () -> !typeclasses_unique); optwrite = (fun b -> typeclasses_unique := b); } diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index fd588f5b15..f8eef68997 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -611,7 +611,6 @@ let vernac_assumption ~atts discharge kind l nl = let is_polymorphic_inductive_cumulativity = declare_bool_option_and_ref ~depr:false ~value:false - ~name:"Polymorphic inductive cumulativity" ~key:["Polymorphic"; "Inductive"; "Cumulativity"] let should_treat_as_cumulative cum poly = @@ -627,7 +626,6 @@ let should_treat_as_cumulative cum poly = let get_uniform_inductive_parameters = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"Uniform inductive parameters" ~key:["Uniform"; "Inductive"; "Parameters"] ~value:false @@ -1220,7 +1218,6 @@ let vernac_generalizable ~local = let () = declare_bool_option { optdepr = false; - optname = "allow sprop"; optkey = ["Allow";"StrictProp"]; optread = (fun () -> Global.sprop_allowed()); optwrite = Global.set_allow_sprop } @@ -1228,7 +1225,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "silent"; optkey = ["Silent"]; optread = (fun () -> !Flags.quiet); optwrite = ((:=) Flags.quiet) } @@ -1236,7 +1232,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit arguments"; optkey = ["Implicit";"Arguments"]; optread = Impargs.is_implicit_args; optwrite = Impargs.make_implicit_args } @@ -1244,7 +1239,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "strict implicit arguments"; optkey = ["Strict";"Implicit"]; optread = Impargs.is_strict_implicit_args; optwrite = Impargs.make_strict_implicit_args } @@ -1252,7 +1246,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "strong strict implicit arguments"; optkey = ["Strongly";"Strict";"Implicit"]; optread = Impargs.is_strongly_strict_implicit_args; optwrite = Impargs.make_strongly_strict_implicit_args } @@ -1260,7 +1253,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "contextual implicit arguments"; optkey = ["Contextual";"Implicit"]; optread = Impargs.is_contextual_implicit_args; optwrite = Impargs.make_contextual_implicit_args } @@ -1268,7 +1260,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit status of reversible patterns"; optkey = ["Reversible";"Pattern";"Implicit"]; optread = Impargs.is_reversible_pattern_implicit_args; optwrite = Impargs.make_reversible_pattern_implicit_args } @@ -1276,7 +1267,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "maximal insertion of implicit"; optkey = ["Maximal";"Implicit";"Insertion"]; optread = Impargs.is_maximal_implicit_args; optwrite = Impargs.make_maximal_implicit_args } @@ -1284,7 +1274,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "coercion printing"; optkey = ["Printing";"Coercions"]; optread = (fun () -> !Constrextern.print_coercions); optwrite = (fun b -> Constrextern.print_coercions := b) } @@ -1292,7 +1281,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "printing of existential variable instances"; optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Detyping.print_evar_arguments); optwrite = (:=) Detyping.print_evar_arguments } @@ -1300,7 +1288,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit arguments printing"; optkey = ["Printing";"Implicit"]; optread = (fun () -> !Constrextern.print_implicits); optwrite = (fun b -> Constrextern.print_implicits := b) } @@ -1308,7 +1295,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "implicit arguments defensive printing"; optkey = ["Printing";"Implicit";"Defensive"]; optread = (fun () -> !Constrextern.print_implicits_defensive); optwrite = (fun b -> Constrextern.print_implicits_defensive := b) } @@ -1316,7 +1302,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "projection printing using dot notation"; optkey = ["Printing";"Projections"]; optread = (fun () -> !Constrextern.print_projections); optwrite = (fun b -> Constrextern.print_projections := b) } @@ -1324,7 +1309,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "notations printing"; optkey = ["Printing";"Notations"]; optread = (fun () -> not !Constrextern.print_no_symbol); optwrite = (fun b -> Constrextern.print_no_symbol := not b) } @@ -1332,7 +1316,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "raw printing"; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); optwrite = (fun b -> Flags.raw_print := b) } @@ -1340,7 +1323,6 @@ let () = let () = declare_int_option { optdepr = false; - optname = "the level of inlining during functor application"; optkey = ["Inline";"Level"]; optread = (fun () -> Some (Flags.get_inline_level ())); optwrite = (fun o -> @@ -1350,7 +1332,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; optread = (fun () -> (Global.typing_flags ()).Declarations.share_reduction); optwrite = Global.set_share_reduction } @@ -1358,7 +1339,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "display compact goal contexts"; optkey = ["Printing";"Compact";"Contexts"]; optread = (fun () -> Printer.get_compact_context()); optwrite = (fun b -> Printer.set_compact_context b) } @@ -1366,7 +1346,6 @@ let () = let () = declare_int_option { optdepr = false; - optname = "the printing depth"; optkey = ["Printing";"Depth"]; optread = Topfmt.get_depth_boxes; optwrite = Topfmt.set_depth_boxes } @@ -1374,7 +1353,6 @@ let () = let () = declare_int_option { optdepr = false; - optname = "the printing width"; optkey = ["Printing";"Width"]; optread = Topfmt.get_margin; optwrite = Topfmt.set_margin } @@ -1382,7 +1360,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "printing of universes"; optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); optwrite = (fun b -> Constrextern.print_universes:=b) } @@ -1390,7 +1367,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "dumping bytecode after compilation"; optkey = ["Dump";"Bytecode"]; optread = (fun () -> !Cbytegen.dump_bytecode); optwrite = (:=) Cbytegen.dump_bytecode } @@ -1398,7 +1374,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "dumping VM lambda code after compilation"; optkey = ["Dump";"Lambda"]; optread = (fun () -> !Clambda.dump_lambda); optwrite = (:=) Clambda.dump_lambda } @@ -1406,7 +1381,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "explicitly parsing implicit arguments"; optkey = ["Parsing";"Explicit"]; optread = (fun () -> !Constrintern.parsing_explicit); optwrite = (fun b -> Constrintern.parsing_explicit := b) } @@ -1414,7 +1388,6 @@ let () = let () = declare_string_option ~preprocess:CWarnings.normalize_flags_string { optdepr = false; - optname = "warnings display"; optkey = ["Warnings"]; optread = CWarnings.get_flags; optwrite = CWarnings.set_flags } @@ -1422,7 +1395,6 @@ let () = let () = declare_string_option { optdepr = false; - optname = "native_compute profiler output"; optkey = ["NativeCompute"; "Profile"; "Filename"]; optread = Nativenorm.get_profile_filename; optwrite = Nativenorm.set_profile_filename } @@ -1430,7 +1402,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "enable native compute profiling"; optkey = ["NativeCompute"; "Profiling"]; optread = Nativenorm.get_profiling_enabled; optwrite = Nativenorm.set_profiling_enabled } @@ -1438,7 +1409,6 @@ let () = let () = declare_bool_option { optdepr = false; - optname = "enable native compute timing"; optkey = ["NativeCompute"; "Timing"]; optread = Nativenorm.get_timing_enabled; optwrite = Nativenorm.set_timing_enabled } @@ -1446,7 +1416,6 @@ let () = let _ = declare_bool_option { optdepr = false; - optname = "guard checking"; optkey = ["Guard"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_guarded); optwrite = (fun b -> Global.set_check_guarded b) } @@ -1454,7 +1423,6 @@ let _ = let _ = declare_bool_option { optdepr = false; - optname = "positivity/productivity checking"; optkey = ["Positivity"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_positive); optwrite = (fun b -> Global.set_check_positive b) } @@ -1462,7 +1430,6 @@ let _ = let _ = declare_bool_option { optdepr = false; - optname = "universes checking"; optkey = ["Universe"; "Checking"]; optread = (fun () -> (Global.typing_flags ()).Declarations.check_universes); optwrite = (fun b -> Global.set_check_universes b) } @@ -1777,7 +1744,6 @@ let search_output_name_only = ref false let () = declare_bool_option { optdepr = false; - optname = "output-name-only search"; optkey = ["Search";"Output";"Name";"Only"]; optread = (fun () -> !search_output_name_only); optwrite = (:=) search_output_name_only } diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml index c14fc78462..1ec09b6beb 100644 --- a/vernac/vernacinterp.ml +++ b/vernac/vernacinterp.ml @@ -65,7 +65,6 @@ let proof_mode_opt_name = ["Default";"Proof";"Mode"] let () = Goptions.declare_string_option Goptions.{ optdepr = false; - optname = "default proof mode" ; optkey = proof_mode_opt_name; optread = get_default_proof_mode_opt; optwrite = set_default_proof_mode_opt; @@ -249,7 +248,6 @@ let interp_qed_delayed_control ~proof ~info ~st ~control { CAst.loc; v=pe } = let () = let open Goptions in declare_int_option { optdepr = false; - optname = "the default timeout"; optkey = ["Default";"Timeout"]; optread = (fun () -> !default_timeout); optwrite = ((:=) default_timeout) } |