aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/proof_using.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof_using.ml')
-rw-r--r--proofs/proof_using.ml6
1 files changed, 2 insertions, 4 deletions
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);