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/proof_global.ml | |
| parent | 03e4f9c3da333d13553b4ea3247b0c36c124995e (diff) | |
| parent | cb316573aa1d09433531e7c67e320c14ef05c3e2 (diff) | |
Merge PR#481: [option] Remove support for non-synchronous options.
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 19 |
1 files changed, 7 insertions, 12 deletions
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 |