Merge PR#481: [option] Remove support for non-synchronous options.

14 files changed, 23 insertions, 52 deletions

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 0cdb10a37..fc1ed335a 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 90e5f3ca5..bbb9feae2 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 8ec3d9b3e..ea985ddec 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 b5028190f..36ac10bfe 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 c5dbc8a14..3ff7b53c7 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 f63c38d4f..8a10a4d76 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2136,8 +2136,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);
@@ -2146,8 +2145,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 20a2013a5..294cba4d7 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 1e46c253d..4ec111e01 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 b6ad784d9..053bb6fa1 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 8be060e19..862e44cca 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -63,8 +63,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);
@@ -183,8 +182,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;