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

6 files changed, 26 insertions, 51 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index c2d12ebd0..b76c0a96a 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -174,8 +174,7 @@ let global_info_auto = ref false
 
 let add_option ls refe =
   let _ = Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
+    { Goptions.optdepr  = false;
       Goptions.optname  = String.concat " " ls;
       Goptions.optkey   = ls;
       Goptions.optread  = (fun () -> !refe);
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 05eb0a976..918371d55 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -92,8 +92,7 @@ open Goptions
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = true;
+    { optdepr  = true;
       optname  = "do typeclass search modulo eta conversion";
       optkey   = ["Typeclasses";"Modulo";"Eta"];
       optread  = get_typeclasses_modulo_eta;
@@ -101,8 +100,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "do typeclass search avoiding eta-expansions " ^
                    " in proof terms (expensive)";
       optkey   = ["Typeclasses";"Limit";"Intros"];
@@ -111,8 +109,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "during typeclass resolution, solve instances according to their dependency order";
       optkey   = ["Typeclasses";"Dependency";"Order"];
       optread  = get_typeclasses_dependency_order;
@@ -120,8 +117,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "use iterative deepening strategy";
       optkey   = ["Typeclasses";"Iterative";"Deepening"];
       optread  = get_typeclasses_iterative_deepening;
@@ -129,8 +125,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "compat";
       optkey   = ["Typeclasses";"Legacy";"Resolution"];
       optread  = get_typeclasses_legacy_resolution;
@@ -138,8 +133,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "compat";
       optkey   = ["Typeclasses";"Filtered";"Unification"];
       optread  = get_typeclasses_filtered_unification;
@@ -147,8 +141,7 @@ let _ =
 
 let set_typeclasses_debug =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "debug output for typeclasses proof search";
       optkey   = ["Typeclasses";"Debug"];
       optread  = get_typeclasses_debug;
@@ -156,8 +149,7 @@ let set_typeclasses_debug =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "debug output for typeclasses proof search";
       optkey   = ["Debug";"Typeclasses"];
       optread  = get_typeclasses_debug;
@@ -165,8 +157,7 @@ let _ =
 
 let _ =
   declare_int_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "verbosity of debug output for typeclasses proof search";
       optkey   = ["Typeclasses";"Debug";"Verbosity"];
       optread  = get_typeclasses_verbose;
@@ -174,8 +165,7 @@ let _ =
 
 let set_typeclasses_depth =
   declare_int_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "depth for typeclasses proof search";
       optkey   = ["Typeclasses";"Depth"];
       optread  = get_typeclasses_depth;
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 8d1e0e507..e87368dec 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -331,8 +331,7 @@ let global_info_eauto = ref false
 
 let _ =
   Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
+    { Goptions.optdepr  = false;
       Goptions.optname  = "Debug Eauto";
       Goptions.optkey   = ["Debug";"Eauto"];
       Goptions.optread  = (fun () -> !global_debug_eauto);
@@ -340,8 +339,7 @@ let _ =
 
 let _ =
   Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
+    { Goptions.optdepr  = false;
       Goptions.optname  = "Info Eauto";
       Goptions.optkey   = ["Info";"Eauto"];
       Goptions.optread  = (fun () -> !global_info_eauto);
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b0f27663e..70d6fe90c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -57,8 +57,7 @@ let discr_do_intro () =
 open Goptions
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "automatic introduction of hypotheses by discriminate";
       optkey   = ["Discriminate";"Introduction"];
       optread  = (fun () -> !discriminate_introduction);
@@ -72,8 +71,7 @@ let use_injection_pattern_l2r_order () =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "injection left-to-right pattern order and clear by default when with introduction pattern";
       optkey   = ["Injection";"L2R";"Pattern";"Order"];
       optread  = (fun () -> !injection_pattern_l2r_order) ;
@@ -87,8 +85,7 @@ let use_injection_in_context () =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "injection in context";
       optkey   = ["Structural";"Injection"];
       optread  = (fun () -> !injection_in_context) ;
@@ -729,8 +726,7 @@ let keep_proof_equalities_for_injection = ref false
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "injection on prop arguments";
       optkey   = ["Keep";"Proof";"Equalities"];
       optread  = (fun () -> !keep_proof_equalities_for_injection) ;
@@ -1680,8 +1676,7 @@ let regular_subst_tactic = ref true
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "more regular behavior of tactic subst";
       optkey   = ["Regular";"Subst";"Tactic"];
       optread  = (fun () -> !regular_subst_tactic);
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 61bc3d284..0c796b886 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -171,8 +171,7 @@ let write_warn_hint = function
 
 let _ =
   Goptions.declare_string_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
+    { Goptions.optdepr  = false;
       Goptions.optname  = "behavior of non-imported hints";
       Goptions.optkey   = ["Loose"; "Hint"; "Behavior"];
       Goptions.optread  = read_warn_hint;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 11c281985..1975eed9d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -70,8 +70,7 @@ let use_dependent_propositions_elimination () =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "dependent-propositions-elimination tactic";
       optkey   = ["Dependent";"Propositions";"Elimination"];
       optread  = (fun () -> !dependent_propositions_elimination) ;
@@ -79,8 +78,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "trigger bugged context matching compatibility";
       optkey   = ["Tactic";"Compat";"Context"];
       optread  = (fun () -> !Flags.tactic_context_compat) ;
@@ -88,7 +86,7 @@ let _ =
 
 let apply_solve_class_goals = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = true;
+  Goptions.optdepr = true;
   Goptions.optname =
     "Perform typeclass resolution on apply-generated subgoals.";
   Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"];
@@ -102,8 +100,7 @@ let use_clear_hyp_by_default () = !clear_hyp_by_default
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "default clearing of hypotheses after use";
       optkey   = ["Default";"Clearing";"Used";"Hypotheses"];
       optread  = (fun () -> !clear_hyp_by_default) ;
@@ -119,8 +116,7 @@ let accept_universal_lemma_under_conjunctions () =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "trivial unification in tactics applying under conjunctions";
       optkey   = ["Universal";"Lemma";"Under";"Conjunction"];
       optread  = (fun () -> !universal_lemma_under_conjunctions) ;
@@ -132,8 +128,7 @@ let shrink_abstract = ref true
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = true;
+    { optdepr  = true;
       optname  = "shrinking of abstracted proofs";
       optkey   = ["Shrink"; "Abstract"];
       optread  = (fun () -> !shrink_abstract) ;
@@ -153,8 +148,7 @@ let use_bracketing_last_or_and_intro_pattern () =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "bracketing last or-and introduction pattern";
       optkey   = ["Bracketing";"Last";"Introduction";"Pattern"];
       optread  = (fun () -> !bracketing_last_or_and_intro_pattern);