diff options
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); |