[option] Remove support for non-synchronous options.

Inspired by https://coq.inria.fr/bugs/show_bug.cgi?id=5229 , which
this PR solves, I propose to remove support for non-synchronous
options.

It seems the few uses of `optsync = false` we legacy and shouldn't
have any impact.

Moreover, non synchronous options may create particularly tricky
situations as for instance, they won't be propagated to workers.

10 files changed, 23 insertions, 39 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index bd7350dc4..782552583 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -177,7 +177,7 @@ let cofixp_reducible flgs _ stk =
 
 let debug_cbv = ref false
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname = "cbv visited constants display";
   Goptions.optkey = ["Debug";"Cbv"];
   Goptions.optread = (fun () -> !debug_cbv);
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 32da81f96..9a973cff5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -428,8 +428,7 @@ let automatically_import_coercions = ref false
 open Goptions
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "automatic import of coercions";
       optkey   = ["Automatic";"Coercions";"Import"];
       optread  = (fun () -> !automatically_import_coercions);
@@ -556,7 +555,6 @@ module CoercionPrinting =
     let member_message x b =
       str "Explicit printing of coercion " ++ printer x ++
       str (if b then " is set" else " is unset")
-    let synchronous = true
   end
 
 module PrintingCoercion  = Goptions.MakeRefTable(CoercionPrinting)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index e6c0075c5..f785f53f1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -33,14 +33,13 @@ open Globnames
 let use_typeclasses_for_conversion = ref true
 
 let _ =
-  Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      optdepr  = false;
+  Goptions.(declare_bool_option
+    { optdepr  = false;
       optname  = "use typeclass resolution during conversion";
       optkey   = ["Typeclass"; "Resolution"; "For"; "Conversion"];
       optread  = (fun () -> !use_typeclasses_for_conversion);
       optwrite = (fun b -> use_typeclasses_for_conversion := b) }
-
+    )
 
 (* Typing operations dealing with coercions *)
 exception NoCoercion
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0d798b4d9..db6756885 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -135,8 +135,7 @@ let wildcard_value = ref true
 let force_wildcard () = !wildcard_value
 
 let _ = declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "forced wildcard";
 	    optkey   = ["Printing";"Wildcard"];
 	    optread  = force_wildcard;
@@ -146,8 +145,7 @@ let synth_type_value = ref true
 let synthetize_type () = !synth_type_value
 
 let _ = declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "pattern matching return type synthesizability";
 	    optkey   = ["Printing";"Synth"];
 	    optread  = synthetize_type;
@@ -157,8 +155,7 @@ let reverse_matching_value = ref true
 let reverse_matching () = !reverse_matching_value
 
 let _ = declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "pattern-matching reversibility";
 	    optkey   = ["Printing";"Matching"];
 	    optread  = reverse_matching;
@@ -168,8 +165,7 @@ let print_primproj_params_value = ref false
 let print_primproj_params () = !print_primproj_params_value
 
 let _ = declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "printing of primitive projection parameters";
 	    optkey   = ["Printing";"Primitive";"Projection";"Parameters"];
 	    optread  = print_primproj_params;
@@ -179,8 +175,7 @@ let print_primproj_compatibility_value = ref false
 let print_primproj_compatibility () = !print_primproj_compatibility_value
 
 let _ = declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "backwards-compatible printing of primitive projections";
 	    optkey   = ["Printing";"Primitive";"Projection";"Compatibility"];
 	    optread  = print_primproj_compatibility;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 305eae15a..b8bf540e3 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -34,7 +34,7 @@ type unify_fun = transparent_state ->
 
 let debug_unification = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname =
     "Print states sent to Evarconv unification";
   Goptions.optkey = ["Debug";"Unification"];
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 4886423bd..64b13e24f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -175,8 +175,7 @@ let is_strict_universe_declarations () = !strict_universe_declarations
 
 let _ =
   Goptions.(declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "strict universe declaration";
 	    optkey   = ["Strict";"Universe";"Declaration"];
 	    optread  = is_strict_universe_declarations;
@@ -184,8 +183,7 @@ let _ =
 
 let _ =
   Goptions.(declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "minimization to Set";
 	    optkey   = ["Universe";"Minimization";"ToSet"];
 	    optread  = Universes.is_set_minimization;
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 42acc5705..de485dbe8 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -87,8 +87,7 @@ open Goptions
 
 let _ =
   declare_bool_option
-  { optsync  = true;
-    optdepr  = false;
+  { optdepr  = false;
     optname  = "preferred transparency of Program obligations";
     optkey   = ["Transparent";"Obligations"];
     optread  = get_proofs_transparency;
@@ -96,8 +95,7 @@ let _ =
 
 let _ =
   declare_bool_option
-  { optsync  = true;
-    optdepr  = false;
+  { optdepr  = false;
     optname  = "program cases";
     optkey   = ["Program";"Cases"];
     optread  = (fun () -> !program_cases);
@@ -105,8 +103,7 @@ let _ =
 
 let _ =
   declare_bool_option
-  { optsync  = true;
-    optdepr  = false;
+  { optdepr  = false;
     optname  = "program generalized coercion";
     optkey   = ["Program";"Generalized";"Coercion"];
     optread  = (fun () -> !program_generalized_coercion);
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 52f424f75..117ed338e 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,7 +29,7 @@ exception Elimconst
 
 let refolding_in_reduction = ref false
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname =
     "Perform refolding of fixpoints/constants like cbn during reductions";
   Goptions.optkey = ["Refolding";"Reduction"];
@@ -811,7 +811,7 @@ let fix_recarg ((recindices,bodynum),_) stack =
 
 let debug_RAKAM = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname =
     "Print states of the Reductionops abstract machine";
   Goptions.optkey = ["Debug";"RAKAM"];
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 93c71e6ea..919e95a8e 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,8 +30,7 @@ open Goptions
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "check that typeclasses proof search returns unique solutions";
       optkey   = ["Typeclasses";"Unique";"Solutions"];
       optread  = get_typeclasses_unique_solutions;
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 661c1d865..9294139d4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -45,7 +45,7 @@ module NamedDecl = Context.Named.Declaration
 
 let keyed_unification = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname = "Unification is keyed";
   Goptions.optkey = ["Keyed";"Unification"];
   Goptions.optread = (fun () -> !keyed_unification);
@@ -56,7 +56,7 @@ let is_keyed_unification () = !keyed_unification
 
 let debug_unification = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname =
     "Print states sent to tactic unification";
   Goptions.optkey = ["Debug";"Tactic";"Unification"];
@@ -257,8 +257,7 @@ let global_pattern_unification_flag = ref true
 open Goptions
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = true;
+    { optdepr  = true;
       optname  = "pattern-unification for existential variables in tactics";
       optkey   = ["Tactic";"Evars";"Pattern";"Unification"];
       optread  = (fun () -> !global_pattern_unification_flag);
@@ -269,8 +268,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "pattern-unification for existential variables in tactics";
       optkey   = ["Tactic";"Pattern";"Unification"];
       optread  = (fun () -> !global_pattern_unification_flag);