2 files changed, 3 insertions, 6 deletions
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);