diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-14 18:38:42 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-05-24 11:47:36 +0200 |
commit | cb316573aa1d09433531e7c67e320c14ef05c3e2 (patch) | |
tree | 02e9e26f826aace38552372979efb7ff7d9e8ef6 | |
parent | bf84180f963a31d1ec850d4ccedd599f2984ea9b (diff) |
[option] Remove support for non-synchronous options.
Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which
this PR solves, I propose to remove support for non-synchronous
options.
It seems the few uses of `optsync = false` we legacy and shouldn't
have any impact.
Moreover, non synchronous options may create particularly tricky
situations as for instance, they won't be propagated to workers.
51 files changed, 157 insertions, 316 deletions
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index fad647291..f27d3115e 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -25,7 +25,7 @@ echo $TRAVIS_PULL_REQUEST echo $TRAVIS_BRANCH echo $TRAVIS_COMMIT -if [ $TRAVIS_PULL_REQUEST == "568" ] || [ $TRAVIS_BRANCH == "remove-tactic-compat" ]; then - fiat_parsers_CI_BRANCH=fix-ml - fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat.git +if [ $TRAVIS_PULL_REQUEST == "481" ] || [ $TRAVIS_BRANCH == "options+remove_non_sync" ]; then + mathcomp_CI_BRANCH=options+remove_non_sync + mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git fi diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 8ea1638c9..b5d12d3c7 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -51,6 +51,13 @@ In Constrexpr_ops: interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones were preserving the original sharing of the type. +In GOption: + + Support for non-synchronous options has been removed. Now all + options are handled as a piece of normal document state, and thus + passed to workers, etc... As a consequence, the field + `Goptions.optsync` has been removed. + ** Tactic API ** - pf_constr_of_global now returns a tactic instead of taking a continuation. diff --git a/engine/namegen.ml b/engine/namegen.ml index 3b979f206..5bd62273c 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -418,8 +418,7 @@ let use_h_based_elimination_names () = open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "use of \"H\"-based proposition names in elimination tactics"; optkey = ["Standard";"Proposition";"Elimination";"Names"]; optread = (fun () -> !h_based_elimination_names); diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index dbca959ea..aeff19afe 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -312,7 +312,7 @@ let import_option_value = function | Interface.StringOptValue s -> Goptions.StringOptValue s let export_option_state s = { - Interface.opt_sync = s.Goptions.opt_sync; + 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/interp/constrextern.ml b/interp/constrextern.ml index 59b8b4e5b..58b38cdac 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -91,8 +91,7 @@ let record_print = ref true let _ = let open Goptions in declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "record printing"; optkey = ["Printing";"Records"]; optread = (fun () -> !record_print); diff --git a/interp/topconstr.ml b/interp/topconstr.ml index e05be65fb..239226b2e 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -21,7 +21,7 @@ open Constrexpr_ops let asymmetric_patterns = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "no parameters in constructors"; Goptions.optkey = ["Asymmetric";"Patterns"]; Goptions.optread = (fun () -> !asymmetric_patterns); diff --git a/library/goptions.ml b/library/goptions.ml index c111113ca..9b4fc9985 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -24,7 +24,6 @@ type option_value = (** Summary of an option status *) type option_state = { - opt_sync : bool; opt_depr : bool; opt_name : string; opt_value : option_value; @@ -62,7 +61,6 @@ module MakeTable = val key : option_name val title : string val member_message : t -> bool -> std_ppcmds - val synchronous : bool end) -> struct type option_mark = @@ -77,13 +75,9 @@ module MakeTable = module MySet = Set.Make (struct type t = A.t let compare = A.compare end) - let t = - if A.synchronous - then Summary.ref MySet.empty ~name:nick - else ref MySet.empty + let t = Summary.ref MySet.empty ~name:nick let (add_option,remove_option) = - if A.synchronous then let cache_options (_,(f,p)) = match f with | GOadd -> t := MySet.add p !t | GOrmv -> t := MySet.remove p !t in @@ -103,9 +97,6 @@ module MakeTable = in ((fun c -> Lib.add_anonymous_leaf (inGo (GOadd, c))), (fun c -> Lib.add_anonymous_leaf (inGo (GOrmv, c)))) - else - ((fun c -> t := MySet.add c !t), - (fun c -> t := MySet.remove c !t)) let print_table table_name printer table = Feedback.msg_notice @@ -141,7 +132,6 @@ sig val key : option_name val title : string val member_message : string -> bool -> std_ppcmds - val synchronous : bool end module StringConvert = functor (A : StringConvertArg) -> @@ -156,7 +146,6 @@ struct let key = A.key let title = A.title let member_message = A.member_message - let synchronous = A.synchronous end module MakeStringTable = @@ -176,7 +165,6 @@ sig val key : option_name val title : string val member_message : t -> bool -> std_ppcmds - val synchronous : bool end module RefConvert = functor (A : RefConvertArg) -> @@ -191,7 +179,6 @@ struct let key = A.key let title = A.title let member_message = A.member_message - let synchronous = A.synchronous end module MakeRefTable = @@ -201,7 +188,6 @@ module MakeRefTable = (* 2- Flags. *) type 'a option_sig = { - optsync : bool; optdepr : bool; optname : string; optkey : option_name; @@ -247,11 +233,10 @@ let get_locality = function | None -> OptDefault let declare_option cast uncast append ?(preprocess = fun x -> x) - { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = + { optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } = check_key key; let default = read() in let change = - if sync then let _ = Summary.declare_summary (nickname key) { Summary.freeze_function = (fun _ -> read ()); Summary.unfreeze_function = write; @@ -275,18 +260,12 @@ let declare_option cast uncast append ?(preprocess = fun x -> x) discharge_function = discharge_options; classify_function = classify_options } in (fun l m v -> let v = preprocess v in Lib.add_anonymous_leaf (options (l, m, v))) - else - (fun _ m v -> - let v = preprocess v in - match m with - | OptSet -> write v - | OptAppend -> write (append (read ()) v)) in let warn () = if depr then warn_deprecated_option key in 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, (sync,cread,cwrite,cappend)) !value_tab; + value_tab := OptionMap.add key (name, depr, (cread,cwrite,cappend)) !value_tab; write type 'a write_function = 'a -> unit @@ -325,7 +304,7 @@ let set_option_value locality 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 (name, depr, (read,write,append)) -> write (get_locality locality) (check_and_cast v (read ())) let bad_type_error () = error "Bad type of value for this option." @@ -366,7 +345,7 @@ let set_string_option_append_value_gen locality 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 (name, depr, (read,write,append)) -> append (get_locality locality) (check_string_value v (read ())) let set_int_option_value = set_int_option_value_gen None @@ -387,7 +366,7 @@ 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 (name, depr, (read,_,_)) = get_option key in let s = read () in match s with | BoolValue b -> @@ -397,9 +376,8 @@ let print_option_value key = let get_tables () = let tables = !value_tab in - let fold key (name, depr, (sync,read,_,_)) accu = + let fold key (name, depr, (read,_,_)) accu = let state = { - opt_sync = sync; opt_name = name; opt_depr = depr; opt_value = read (); @@ -416,15 +394,8 @@ let print_tables () = in str "Synchronous options:" ++ fnl () ++ OptionMap.fold - (fun key (name, depr, (sync,read,_,_)) p -> - if sync then p ++ print_option key name (read ()) depr - else p) - !value_tab (mt ()) ++ - str "Asynchronous options:" ++ fnl () ++ - OptionMap.fold - (fun key (name, depr, (sync,read,_,_)) p -> - if sync then p - else p ++ print_option key name (read ()) depr) + (fun key (name, depr, (read,_,_)) p -> + p ++ print_option key name (read ()) depr) !value_tab (mt ()) ++ str "Tables:" ++ fnl () ++ List.fold_right diff --git a/library/goptions.mli b/library/goptions.mli index 3b3651f39..f612c4e36 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -40,8 +40,8 @@ Unset Tata Tutu Titi. Print Table Tata Tutu Titi. (** synonym: Test Table Tata Tutu Titi. *) - The created table/option may be declared synchronous or not - (synchronous = consistent with the resetting commands) *) + All options are synchronized with the document. +*) open Pp open Libnames @@ -65,7 +65,6 @@ module MakeStringTable : val key : option_name val title : string val member_message : string -> bool -> std_ppcmds - val synchronous : bool end) -> sig val active : string -> bool @@ -93,7 +92,6 @@ module MakeRefTable : val key : option_name val title : string val member_message : t -> bool -> std_ppcmds - val synchronous : bool end) -> sig val active : A.t -> bool @@ -108,8 +106,6 @@ module MakeRefTable : used when printing the option value (command "Print Toto Titi." *) type 'a option_sig = { - optsync : bool; - (** whether the option is synchronous w.r.t to the section/module system. *) optdepr : bool; (** whether the option is DEPRECATED *) optname : string; @@ -120,8 +116,6 @@ type 'a option_sig = { optwrite : 'a -> unit } -(** When an option is declared synchronous ([optsync] is [true]), the output is - a synchronous write function. Otherwise it is [optwrite] *) (** The [preprocess] function is triggered before setting the option. It can be used to emit a warning on certain values, and clean-up the final value. *) @@ -177,7 +171,6 @@ type option_value = (** Summary of an option status *) type option_state = { - opt_sync : bool; opt_depr : bool; opt_name : string; opt_value : option_value; diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index aa71a4565..5dea4631c 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -29,8 +29,7 @@ let debug x = let _= let gdopt= - { optsync=true; - optdepr=false; + { optdepr=false; optname="Congruence Verbose"; optkey=["Congruence";"Verbose"]; optread=(fun ()-> !cc_verbose); 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); diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index b25017535..bbe1476bc 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -30,8 +30,7 @@ let ground_depth=ref 3 let _= let gdopt= - { optsync=true; - optdepr=false; + { optdepr=false; optname="Firstorder Depth"; optkey=["Firstorder";"Depth"]; optread=(fun ()->Some !ground_depth); @@ -46,8 +45,7 @@ let congruence_depth=ref 100 let _= let gdopt= - { optsync=true; - optdepr=false; + { optdepr=false; optname="Congruence Depth"; optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 848b44a60..1c1e6843a 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -422,7 +422,6 @@ open Goptions let functional_induction_rewrite_dependent_proofs_sig = { - optsync = false; optdepr = false; optname = "Functional Induction Rewrite Dependent"; optkey = ["Functional";"Induction";"Rewrite";"Dependent"]; @@ -435,7 +434,6 @@ let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = t let function_debug_sig = { - optsync = false; optdepr = false; optname = "Function debug"; optkey = ["Function_debug"]; @@ -454,7 +452,6 @@ let strict_tcc = ref false let is_strict_tcc () = !strict_tcc let strict_tcc_sig = { - optsync = false; optdepr = false; optname = "Raw Function Tcc"; optkey = ["Function_raw_tcc"]; diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index d717ed0a5..31fcf6c96 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -367,7 +367,6 @@ open Libnames let print_info_trace = ref None let _ = declare_int_option { - optsync = true; optdepr = false; optname = "print info trace"; optkey = ["Info" ; "Level"]; diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index a853576f2..747669852 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -411,8 +411,7 @@ let _ = Declaremods.append_end_library_hook do_print_results_at_close let _ = let open Goptions in declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "Ltac Profiling"; optkey = ["Ltac"; "Profiling"]; optread = get_profiling; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index b8c021f18..ef230348f 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2138,8 +2138,7 @@ let vernac_debug b = let _ = let open Goptions in declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Ltac debug"; optkey = ["Ltac";"Debug"]; optread = (fun () -> get_debug () != Tactic_debug.DebugOff); @@ -2148,8 +2147,7 @@ let _ = let _ = let open Goptions in declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Ltac debug"; optkey = ["Debug";"Ltac"]; optread = (fun () -> get_debug () != Tactic_debug.DebugOff); diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index dac15ff79..84d771bff 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -91,8 +91,7 @@ open Goptions let _ = declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Ltac batch debug"; optkey = ["Ltac";"Batch";"Debug"]; optread = (fun () -> !batch); diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 4de2081cf..c7be99616 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -70,8 +70,7 @@ let unfold_iff () = !iff_unfolding || Flags.version_less_or_equal Flags.V8_2 open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "unfolding of not in intuition"; optkey = ["Intuition";"Negation";"Unfolding"]; optread = (fun () -> !negation_unfolding); @@ -79,8 +78,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "unfolding of iff in intuition"; optkey = ["Intuition";"Iff";"Unfolding"]; optread = (fun () -> !iff_unfolding); diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index a36607ec3..012db04a6 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -65,7 +65,6 @@ let _ = let int_opt l vref = { - optsync = true; optdepr = false; optname = List.fold_right (^) l ""; optkey = l ; @@ -75,7 +74,6 @@ let _ = let lia_enum_opt = { - optsync = true; optdepr = false; optname = "Lia Enum"; optkey = ["Lia";"Enum"]; diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 92b092ffe..334baec8d 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -71,8 +71,7 @@ open Goptions let _ = declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Omega system time displaying flag"; optkey = ["Omega";"System"]; optread = read display_system_flag; @@ -80,8 +79,7 @@ let _ = let _ = declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Omega action display flag"; optkey = ["Omega";"Action"]; optread = read display_action_flag; @@ -89,8 +87,7 @@ let _ = let _ = declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "Omega old style flag"; optkey = ["Omega";"OldStyle"]; optread = read old_style_flag; @@ -98,8 +95,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = true; + { optdepr = true; optname = "Omega automatic reset of generated names"; optkey = ["Stable";"Omega"]; optread = read reset_flag; diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 1ad4d622b..4eef1b0a7 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -46,8 +46,7 @@ let reset_info () = let pruning = ref true let opt_pruning= - {optsync=true; - optdepr=false; + {optdepr=false; optname="Rtauto Pruning"; optkey=["Rtauto";"Pruning"]; optread=(fun () -> !pruning); diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 3655df895..d580fde29 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -236,8 +236,7 @@ open Goptions let verbose = ref false let opt_verbose= - {optsync=true; - optdepr=false; + {optdepr=false; optname="Rtauto Verbose"; optkey=["Rtauto";"Verbose"]; optread=(fun () -> !verbose); @@ -248,8 +247,7 @@ let _ = declare_bool_option opt_verbose let check = ref false let opt_check= - {optsync=true; - optdepr=false; + {optdepr=false; optname="Rtauto Check"; optkey=["Rtauto";"Check"]; optread=(fun () -> !check); diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 72c70750c..edf934c7d 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -64,8 +64,7 @@ let debug b = if b then pp_ref := ssr_pp else pp_ref := fun _ -> () let _ = Goptions.declare_bool_option - { Goptions.optsync = false; - Goptions.optname = "ssrmatching debugging"; + { Goptions.optname = "ssrmatching debugging"; Goptions.optkey = ["Debug";"SsrMatching"]; Goptions.optdepr = false; Goptions.optread = (fun _ -> !pp_ref == ssr_pp); @@ -184,8 +183,7 @@ let profile b = ;; let _ = Goptions.declare_bool_option - { Goptions.optsync = false; - Goptions.optname = "ssrmatching profiling"; + { Goptions.optname = "ssrmatching profiling"; Goptions.optkey = ["SsrMatchingProfiling"]; Goptions.optread = (fun _ -> !profile_now); Goptions.optdepr = false; diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index bd7350dc4..782552583 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -177,7 +177,7 @@ let cofixp_reducible flgs _ stk = let debug_cbv = ref false let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "cbv visited constants display"; Goptions.optkey = ["Debug";"Cbv"]; Goptions.optread = (fun () -> !debug_cbv); diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 32da81f96..9a973cff5 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -428,8 +428,7 @@ let automatically_import_coercions = ref false open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic import of coercions"; optkey = ["Automatic";"Coercions";"Import"]; optread = (fun () -> !automatically_import_coercions); @@ -556,7 +555,6 @@ module CoercionPrinting = let member_message x b = str "Explicit printing of coercion " ++ printer x ++ str (if b then " is set" else " is unset") - let synchronous = true end module PrintingCoercion = Goptions.MakeRefTable(CoercionPrinting) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index e6c0075c5..f785f53f1 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -33,14 +33,13 @@ open Globnames let use_typeclasses_for_conversion = ref true let _ = - Goptions.declare_bool_option - { Goptions.optsync = true; - optdepr = false; + Goptions.(declare_bool_option + { optdepr = false; optname = "use typeclass resolution during conversion"; optkey = ["Typeclass"; "Resolution"; "For"; "Conversion"]; optread = (fun () -> !use_typeclasses_for_conversion); optwrite = (fun b -> use_typeclasses_for_conversion := b) } - + ) (* Typing operations dealing with coercions *) exception NoCoercion diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 0d798b4d9..db6756885 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -135,8 +135,7 @@ let wildcard_value = ref true let force_wildcard () = !wildcard_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "forced wildcard"; optkey = ["Printing";"Wildcard"]; optread = force_wildcard; @@ -146,8 +145,7 @@ let synth_type_value = ref true let synthetize_type () = !synth_type_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "pattern matching return type synthesizability"; optkey = ["Printing";"Synth"]; optread = synthetize_type; @@ -157,8 +155,7 @@ let reverse_matching_value = ref true let reverse_matching () = !reverse_matching_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "pattern-matching reversibility"; optkey = ["Printing";"Matching"]; optread = reverse_matching; @@ -168,8 +165,7 @@ let print_primproj_params_value = ref false let print_primproj_params () = !print_primproj_params_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "printing of primitive projection parameters"; optkey = ["Printing";"Primitive";"Projection";"Parameters"]; optread = print_primproj_params; @@ -179,8 +175,7 @@ let print_primproj_compatibility_value = ref false let print_primproj_compatibility () = !print_primproj_compatibility_value let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "backwards-compatible printing of primitive projections"; optkey = ["Printing";"Primitive";"Projection";"Compatibility"]; optread = print_primproj_compatibility; diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 305eae15a..b8bf540e3 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -34,7 +34,7 @@ type unify_fun = transparent_state -> let debug_unification = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Print states sent to Evarconv unification"; Goptions.optkey = ["Debug";"Unification"]; diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4886423bd..64b13e24f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -175,8 +175,7 @@ let is_strict_universe_declarations () = !strict_universe_declarations let _ = Goptions.(declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "strict universe declaration"; optkey = ["Strict";"Universe";"Declaration"]; optread = is_strict_universe_declarations; @@ -184,8 +183,7 @@ let _ = let _ = Goptions.(declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "minimization to Set"; optkey = ["Universe";"Minimization";"ToSet"]; optread = Universes.is_set_minimization; diff --git a/pretyping/program.ml b/pretyping/program.ml index 42acc5705..de485dbe8 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -87,8 +87,7 @@ open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "preferred transparency of Program obligations"; optkey = ["Transparent";"Obligations"]; optread = get_proofs_transparency; @@ -96,8 +95,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "program cases"; optkey = ["Program";"Cases"]; optread = (fun () -> !program_cases); @@ -105,8 +103,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "program generalized coercion"; optkey = ["Program";"Generalized";"Coercion"]; optread = (fun () -> !program_generalized_coercion); diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 52f424f75..117ed338e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -29,7 +29,7 @@ exception Elimconst let refolding_in_reduction = ref false let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Perform refolding of fixpoints/constants like cbn during reductions"; Goptions.optkey = ["Refolding";"Reduction"]; @@ -811,7 +811,7 @@ let fix_recarg ((recindices,bodynum),_) stack = let debug_RAKAM = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Print states of the Reductionops abstract machine"; Goptions.optkey = ["Debug";"RAKAM"]; diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 93c71e6ea..919e95a8e 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -30,8 +30,7 @@ open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "check that typeclasses proof search returns unique solutions"; optkey = ["Typeclasses";"Unique";"Solutions"]; optread = get_typeclasses_unique_solutions; diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 661c1d865..9294139d4 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -45,7 +45,7 @@ module NamedDecl = Context.Named.Declaration let keyed_unification = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Unification is keyed"; Goptions.optkey = ["Keyed";"Unification"]; Goptions.optread = (fun () -> !keyed_unification); @@ -56,7 +56,7 @@ let is_keyed_unification () = !keyed_unification let debug_unification = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Print states sent to tactic unification"; Goptions.optkey = ["Debug";"Tactic";"Unification"]; @@ -257,8 +257,7 @@ let global_pattern_unification_flag = ref true open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = true; + { optdepr = true; optname = "pattern-unification for existential variables in tactics"; optkey = ["Tactic";"Evars";"Pattern";"Unification"]; optread = (fun () -> !global_pattern_unification_flag); @@ -269,8 +268,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "pattern-unification for existential variables in tactics"; optkey = ["Tactic";"Pattern";"Unification"]; optread = (fun () -> !global_pattern_unification_flag); diff --git a/printing/printer.ml b/printing/printer.ml index e0ca51f0c..0276e6d1d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -44,8 +44,7 @@ let should_gname() = !enable_goal_names_printing let _ = let open Goptions in declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "printing of unfocused goal"; optkey = ["Printing";"Unfocused"]; optread = (fun () -> !enable_unfocused_goal_printing); @@ -56,8 +55,7 @@ let _ = let _ = let open Goptions in declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "printing of goal tags"; optkey = ["Printing";"Goal";"Tags"]; optread = (fun () -> !enable_goal_tags_printing); @@ -67,8 +65,7 @@ let _ = let _ = let open Goptions in declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "printing of goal names"; optkey = ["Printing";"Goal";"Names"]; optread = (fun () -> !enable_goal_names_printing); @@ -449,8 +446,7 @@ let print_hyps_limit = ref (None : int option) let _ = let open Goptions in declare_int_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "the hypotheses limit"; optkey = ["Hyps";"Limit"]; optread = (fun () -> !print_hyps_limit); @@ -635,8 +631,7 @@ let should_print_dependent_evars = ref false let _ = let open Goptions in declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "Printing Dependent Evars Line"; optkey = ["Printing";"Dependent";"Evars";"Line"]; optread = (fun () -> !should_print_dependent_evars); diff --git a/printing/printmod.ml b/printing/printmod.ml index 6f4b162d7..c4affd4ac 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -42,8 +42,7 @@ let short = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "short module printing"; optkey = ["Short";"Module";"Printing"]; optread = (fun () -> !short) ; diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 7e8ed31d1..92b4e788a 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -15,7 +15,7 @@ open Evd let use_unification_heuristics_ref = ref true let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Solve unification constraints at every \".\""; Goptions.optkey = ["Solve";"Unification";"Constraints"]; Goptions.optread = (fun () -> !use_unification_heuristics_ref); diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 99fab0848..ef7e7c924 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -52,8 +52,7 @@ let get_default_proof_mode_name () = (CEphemeron.default !default_proof_mode standard).name let _ = - Goptions.declare_string_option {Goptions. - optsync = true ; + Goptions.(declare_string_option { optdepr = false; optname = "default proof mode" ; optkey = ["Default";"Proof";"Mode"] ; @@ -63,7 +62,7 @@ let _ = optwrite = begin fun n -> default_proof_mode := find_proof_mode n end - } + }) (*** Proof Global Environment ***) @@ -268,8 +267,7 @@ let get_universe_binders () = (cur_pstate ()).universe_binders let proof_using_auto_clear = ref false let _ = Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = "Proof using Clear Unused"; Goptions.optkey = ["Proof";"Using";"Clear";"Unused"]; Goptions.optread = (fun () -> !proof_using_auto_clear); @@ -628,8 +626,7 @@ module Bullet = struct let current_behavior = ref Strict.strict let _ = - Goptions.declare_string_option {Goptions. - optsync = true; + Goptions.(declare_string_option { optdepr = false; optname = "bullet behavior"; optkey = ["Bullet";"Behavior"]; @@ -642,7 +639,7 @@ module Bullet = struct with Not_found -> CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".") end - } + }) let put p b = (!current_behavior).put p b @@ -696,9 +693,7 @@ let parse_goal_selector = function end let _ = - Goptions.declare_string_option {Goptions. - optsync = true ; - optdepr = false; + Goptions.(declare_string_option{optdepr = false; optname = "default goal selector" ; optkey = ["Default";"Goal";"Selector"] ; optread = begin fun () -> @@ -708,7 +703,7 @@ let _ = optwrite = begin fun n -> default_goal_selector := parse_goal_selector n end - } + }) module V82 = struct diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index 2c489d6de..a71b98910 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -144,8 +144,7 @@ let value = ref false let _ = Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = "suggest Proof using"; Goptions.optkey = ["Suggest";"Proof";"Using"]; Goptions.optread = (fun () -> !value); @@ -159,8 +158,7 @@ let value = ref None let _ = Goptions.declare_stringopt_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = "default value for Proof using"; Goptions.optkey = ["Default";"Proof";"Using"]; Goptions.optread = (fun () -> !value); diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index cb3538422..7cd526843 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -52,7 +52,7 @@ let strong_cbn flags = let simplIsCbn = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; + Goptions.optdepr = false; Goptions.optname = "Plug the simpl tactic to the new cbn mechanism"; Goptions.optkey = ["SimplIsCbn"]; diff --git a/tactics/auto.ml b/tactics/auto.ml index c2d12ebd0..b76c0a96a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -174,8 +174,7 @@ let global_info_auto = ref false let add_option ls refe = let _ = Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = String.concat " " ls; Goptions.optkey = ls; Goptions.optread = (fun () -> !refe); diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 05eb0a976..918371d55 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -92,8 +92,7 @@ open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = true; + { optdepr = true; optname = "do typeclass search modulo eta conversion"; optkey = ["Typeclasses";"Modulo";"Eta"]; optread = get_typeclasses_modulo_eta; @@ -101,8 +100,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "do typeclass search avoiding eta-expansions " ^ " in proof terms (expensive)"; optkey = ["Typeclasses";"Limit";"Intros"]; @@ -111,8 +109,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "during typeclass resolution, solve instances according to their dependency order"; optkey = ["Typeclasses";"Dependency";"Order"]; optread = get_typeclasses_dependency_order; @@ -120,8 +117,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "use iterative deepening strategy"; optkey = ["Typeclasses";"Iterative";"Deepening"]; optread = get_typeclasses_iterative_deepening; @@ -129,8 +125,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "compat"; optkey = ["Typeclasses";"Legacy";"Resolution"]; optread = get_typeclasses_legacy_resolution; @@ -138,8 +133,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "compat"; optkey = ["Typeclasses";"Filtered";"Unification"]; optread = get_typeclasses_filtered_unification; @@ -147,8 +141,7 @@ let _ = let set_typeclasses_debug = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "debug output for typeclasses proof search"; optkey = ["Typeclasses";"Debug"]; optread = get_typeclasses_debug; @@ -156,8 +149,7 @@ let set_typeclasses_debug = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "debug output for typeclasses proof search"; optkey = ["Debug";"Typeclasses"]; optread = get_typeclasses_debug; @@ -165,8 +157,7 @@ let _ = let _ = declare_int_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "verbosity of debug output for typeclasses proof search"; optkey = ["Typeclasses";"Debug";"Verbosity"]; optread = get_typeclasses_verbose; @@ -174,8 +165,7 @@ let _ = let set_typeclasses_depth = declare_int_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "depth for typeclasses proof search"; optkey = ["Typeclasses";"Depth"]; optread = get_typeclasses_depth; diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 8d1e0e507..e87368dec 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -331,8 +331,7 @@ let global_info_eauto = ref false let _ = Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = "Debug Eauto"; Goptions.optkey = ["Debug";"Eauto"]; Goptions.optread = (fun () -> !global_debug_eauto); @@ -340,8 +339,7 @@ let _ = let _ = Goptions.declare_bool_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = "Info Eauto"; Goptions.optkey = ["Info";"Eauto"]; Goptions.optread = (fun () -> !global_info_eauto); diff --git a/tactics/equality.ml b/tactics/equality.ml index 18a1f0201..7a447f80f 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -57,8 +57,7 @@ let discr_do_intro () = open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic introduction of hypotheses by discriminate"; optkey = ["Discriminate";"Introduction"]; optread = (fun () -> !discriminate_introduction); @@ -72,8 +71,7 @@ let use_injection_pattern_l2r_order () = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "injection left-to-right pattern order and clear by default when with introduction pattern"; optkey = ["Injection";"L2R";"Pattern";"Order"]; optread = (fun () -> !injection_pattern_l2r_order) ; @@ -87,8 +85,7 @@ let use_injection_in_context () = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "injection in context"; optkey = ["Structural";"Injection"]; optread = (fun () -> !injection_in_context) ; @@ -729,8 +726,7 @@ let keep_proof_equalities_for_injection = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "injection on prop arguments"; optkey = ["Keep";"Proof";"Equalities"]; optread = (fun () -> !keep_proof_equalities_for_injection) ; @@ -1680,8 +1676,7 @@ let regular_subst_tactic = ref true let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "more regular behavior of tactic subst"; optkey = ["Regular";"Subst";"Tactic"]; optread = (fun () -> !regular_subst_tactic); diff --git a/tactics/hints.ml b/tactics/hints.ml index c5bacc5a2..c8abd03f3 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -171,8 +171,7 @@ let write_warn_hint = function let _ = Goptions.declare_string_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = "behavior of non-imported hints"; Goptions.optkey = ["Loose"; "Hint"; "Behavior"]; Goptions.optread = read_warn_hint; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 15cef676e..6d77b4e35 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -72,8 +72,7 @@ let use_dependent_propositions_elimination () = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "dependent-propositions-elimination tactic"; optkey = ["Dependent";"Propositions";"Elimination"]; optread = (fun () -> !dependent_propositions_elimination) ; @@ -81,8 +80,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "trigger bugged context matching compatibility"; optkey = ["Tactic";"Compat";"Context"]; optread = (fun () -> !Flags.tactic_context_compat) ; @@ -90,7 +88,7 @@ let _ = let apply_solve_class_goals = ref (false) let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = true; + Goptions.optdepr = true; Goptions.optname = "Perform typeclass resolution on apply-generated subgoals."; Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"]; @@ -104,8 +102,7 @@ let use_clear_hyp_by_default () = !clear_hyp_by_default let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "default clearing of hypotheses after use"; optkey = ["Default";"Clearing";"Used";"Hypotheses"]; optread = (fun () -> !clear_hyp_by_default) ; @@ -121,8 +118,7 @@ let accept_universal_lemma_under_conjunctions () = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "trivial unification in tactics applying under conjunctions"; optkey = ["Universal";"Lemma";"Under";"Conjunction"]; optread = (fun () -> !universal_lemma_under_conjunctions) ; @@ -134,8 +130,7 @@ let shrink_abstract = ref true let _ = declare_bool_option - { optsync = true; - optdepr = true; + { optdepr = true; optname = "shrinking of abstracted proofs"; optkey = ["Shrink"; "Abstract"]; optread = (fun () -> !shrink_abstract) ; @@ -155,8 +150,7 @@ let use_bracketing_last_or_and_intro_pattern () = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; optread = (fun () -> !bracketing_last_or_and_intro_pattern); diff --git a/vernac/classes.ml b/vernac/classes.ml index d515b0c9b..e760487bd 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -32,7 +32,6 @@ open Entries let refine_instance = ref true let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; Goptions.optname = "definition of instances by refining"; Goptions.optkey = ["Refine";"Instance";"Mode"]; diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 9ba4e46e4..2458c5131 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -45,8 +45,7 @@ open Context.Rel.Declaration let elim_flag = ref true let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic declaration of induction schemes"; optkey = ["Elimination";"Schemes"]; optread = (fun () -> !elim_flag) ; @@ -55,16 +54,14 @@ let _ = let bifinite_elim_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { 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) } let _ = declare_bool_option - { optsync = true; - optdepr = true; (* compatibility 2014-09-03*) + { optdepr = true; (* compatibility 2014-09-03*) optname = "automatic declaration of induction schemes for non-recursive types"; optkey = ["Record";"Elimination";"Schemes"]; optread = (fun () -> !bifinite_elim_flag) ; @@ -73,8 +70,7 @@ let _ = let case_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic declaration of case analysis schemes"; optkey = ["Case";"Analysis";"Schemes"]; optread = (fun () -> !case_flag) ; @@ -83,16 +79,14 @@ let _ = let eq_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic declaration of boolean equality"; optkey = ["Boolean";"Equality";"Schemes"]; optread = (fun () -> !eq_flag) ; optwrite = (fun b -> eq_flag := b) } let _ = (* compatibility *) declare_bool_option - { optsync = true; - optdepr = true; + { optdepr = true; optname = "automatic declaration of boolean equality"; optkey = ["Equality";"Scheme"]; optread = (fun () -> !eq_flag) ; @@ -103,8 +97,7 @@ let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2 let eq_dec_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic declaration of decidable equality"; optkey = ["Decidable";"Equality";"Schemes"]; optread = (fun () -> !eq_dec_flag) ; @@ -113,8 +106,7 @@ let _ = let rewriting_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname ="automatic declaration of rewriting schemes for equality types"; optkey = ["Rewriting";"Schemes"]; optread = (fun () -> !rewriting_flag) ; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index b79795aeb..816cb2478 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -474,8 +474,7 @@ let keep_admitted_vars = ref true let _ = let open Goptions in declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "keep section variables in admitted proofs"; optkey = ["Keep"; "Admitted"; "Variables"]; optread = (fun () -> !keep_admitted_vars); diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 24cb9c886..c43816c9c 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -340,8 +340,7 @@ let get_hide_obligations () = !hide_obligations open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "Hidding of Program obligations"; optkey = ["Hide";"Obligations"]; optread = get_hide_obligations; @@ -354,8 +353,7 @@ let get_shrink_obligations () = !shrink_obligations let _ = declare_bool_option - { optsync = true; - optdepr = true; + { optdepr = true; optname = "Shrinking of Program obligations"; optkey = ["Shrink";"Obligations"]; optread = get_shrink_obligations; diff --git a/vernac/record.ml b/vernac/record.ml index 53722b8f6..fabd11260 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -35,8 +35,7 @@ module RelDecl = Context.Rel.Declaration let primitive_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "use of primitive projections"; optkey = ["Primitive";"Projections"]; optread = (fun () -> !primitive_flag) ; @@ -45,8 +44,7 @@ let _ = let typeclasses_strict = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "strict typeclass resolution"; optkey = ["Typeclasses";"Strict";"Resolution"]; optread = (fun () -> !typeclasses_strict); @@ -55,8 +53,7 @@ let _ = let typeclasses_unique = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "unique typeclass instances"; optkey = ["Typeclasses";"Unique";"Instances"]; optread = (fun () -> !typeclasses_unique); diff --git a/vernac/search.ml b/vernac/search.ml index 5b6e9a9c3..916015800 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -40,7 +40,6 @@ module SearchBlacklist = let title = "Current search blacklist : " let member_message s b = str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s - let synchronous = true end) (* The functions iter_constructors and iter_declarations implement the behavior diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d4e6af995..6c5b0dfb4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1228,8 +1228,7 @@ let vernac_generalizable locality = let _ = declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "silent"; optkey = ["Silent"]; optread = (fun () -> !Flags.quiet); @@ -1237,8 +1236,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "implicit arguments"; optkey = ["Implicit";"Arguments"]; optread = Impargs.is_implicit_args; @@ -1246,8 +1244,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "strict implicit arguments"; optkey = ["Strict";"Implicit"]; optread = Impargs.is_strict_implicit_args; @@ -1255,8 +1252,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "strong strict implicit arguments"; optkey = ["Strongly";"Strict";"Implicit"]; optread = Impargs.is_strongly_strict_implicit_args; @@ -1264,8 +1260,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "contextual implicit arguments"; optkey = ["Contextual";"Implicit"]; optread = Impargs.is_contextual_implicit_args; @@ -1273,8 +1268,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "implicit status of reversible patterns"; optkey = ["Reversible";"Pattern";"Implicit"]; optread = Impargs.is_reversible_pattern_implicit_args; @@ -1282,8 +1276,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "maximal insertion of implicit"; optkey = ["Maximal";"Implicit";"Insertion"]; optread = Impargs.is_maximal_implicit_args; @@ -1291,8 +1284,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic introduction of variables"; optkey = ["Automatic";"Introduction"]; optread = Flags.is_auto_intros; @@ -1300,8 +1292,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "coercion printing"; optkey = ["Printing";"Coercions"]; optread = (fun () -> !Constrextern.print_coercions); @@ -1309,8 +1300,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "printing of existential variable instances"; optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Detyping.print_evar_arguments); @@ -1318,8 +1308,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "implicit arguments printing"; optkey = ["Printing";"Implicit"]; optread = (fun () -> !Constrextern.print_implicits); @@ -1327,8 +1316,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "implicit arguments defensive printing"; optkey = ["Printing";"Implicit";"Defensive"]; optread = (fun () -> !Constrextern.print_implicits_defensive); @@ -1336,8 +1324,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "projection printing using dot notation"; optkey = ["Printing";"Projections"]; optread = (fun () -> !Constrextern.print_projections); @@ -1345,8 +1332,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "notations printing"; optkey = ["Printing";"Notations"]; optread = (fun () -> not !Constrextern.print_no_symbol); @@ -1354,8 +1340,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "raw printing"; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); @@ -1363,8 +1348,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "use of the program extension"; optkey = ["Program";"Mode"]; optread = (fun () -> !Flags.program_mode); @@ -1372,8 +1356,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "universe polymorphism"; optkey = ["Universe"; "Polymorphism"]; optread = Flags.is_universe_polymorphism; @@ -1381,8 +1364,7 @@ let _ = let _ = declare_int_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "the level of inlining during functor application"; optkey = ["Inline";"Level"]; optread = (fun () -> Some (Flags.get_inline_level ())); @@ -1392,8 +1374,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; optread = (fun () -> !CClosure.share); @@ -1404,8 +1385,7 @@ let _ = let _ = declare_int_option - { optsync = false; - optdepr = true; + { optdepr = true; optname = "the undo limit (OBSOLETE)"; optkey = ["Undo"]; optread = (fun _ -> None); @@ -1413,8 +1393,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "display compact goal contexts"; optkey = ["Printing";"Compact";"Contexts"]; optread = (fun () -> Printer.get_compact_context()); @@ -1422,8 +1401,7 @@ let _ = let _ = declare_int_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "the printing depth"; optkey = ["Printing";"Depth"]; optread = Topfmt.get_depth_boxes; @@ -1431,8 +1409,7 @@ let _ = let _ = declare_int_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "the printing width"; optkey = ["Printing";"Width"]; optread = Topfmt.get_margin; @@ -1440,8 +1417,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "printing of universes"; optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); @@ -1449,8 +1425,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "dumping bytecode after compilation"; optkey = ["Dump";"Bytecode"]; optread = Flags.get_dump_bytecode; @@ -1458,8 +1433,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "explicitly parsing implicit arguments"; optkey = ["Parsing";"Explicit"]; optread = (fun () -> !Constrintern.parsing_explicit); @@ -1467,8 +1441,7 @@ let _ = let _ = declare_string_option ~preprocess:CWarnings.normalize_flags_string - { optsync = true; - optdepr = false; + { optdepr = false; optname = "warnings display"; optkey = ["Warnings"]; optread = CWarnings.get_flags; @@ -1739,8 +1712,7 @@ let search_output_name_only = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "output-name-only search"; optkey = ["Search";"Output";"Name";"Only"]; optread = (fun () -> !search_output_name_only); @@ -2137,8 +2109,7 @@ let default_timeout = ref None let _ = Goptions.declare_int_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = "the default timeout"; Goptions.optkey = ["Default";"Timeout"]; Goptions.optread = (fun () -> !default_timeout); |