diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 12:49:12 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-05-25 12:49:12 +0200 |
commit | 2f75922ad52e334b7bcc3a26c2ecb1602c85fc2f (patch) | |
tree | 3ba950c021df581a004a4af158880558eb2dbe14 /proofs | |
parent | 03e4f9c3da333d13553b4ea3247b0c36c124995e (diff) | |
parent | cb316573aa1d09433531e7c67e320c14ef05c3e2 (diff) |
Merge PR#481: [option] Remove support for non-synchronous options.
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/pfedit.ml | 2 | ||||
-rw-r--r-- | proofs/proof_global.ml | 19 | ||||
-rw-r--r-- | proofs/proof_using.ml | 6 | ||||
-rw-r--r-- | proofs/redexpr.ml | 2 |
4 files changed, 11 insertions, 18 deletions
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 2396db868..95aee72cb 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 f0854e9aa..f701f7cfe 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"]; |