[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.

4 files changed, 11 insertions, 18 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7e8ed31d1..92b4e788a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -15,7 +15,7 @@ open Evd
 
 let use_unification_heuristics_ref = ref true
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname = "Solve unification constraints at every \".\"";
   Goptions.optkey = ["Solve";"Unification";"Constraints"];
   Goptions.optread = (fun () -> !use_unification_heuristics_ref);
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 99fab0848..ef7e7c924 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -52,8 +52,7 @@ let get_default_proof_mode_name () =
   (CEphemeron.default !default_proof_mode standard).name
 
 let _ =
-  Goptions.declare_string_option {Goptions.
-    optsync = true ;
+  Goptions.(declare_string_option {
     optdepr = false;
     optname = "default proof mode" ;
     optkey = ["Default";"Proof";"Mode"] ;
@@ -63,7 +62,7 @@ let _ =
     optwrite = begin fun n ->
       default_proof_mode := find_proof_mode n
     end
-  }
+  })
 
 (*** Proof Global Environment ***)
 
@@ -268,8 +267,7 @@ let get_universe_binders () = (cur_pstate ()).universe_binders
 
 let proof_using_auto_clear = ref false
 let _ = Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
+    { Goptions.optdepr  = false;
       Goptions.optname  = "Proof using Clear Unused";
       Goptions.optkey   = ["Proof";"Using";"Clear";"Unused"];
       Goptions.optread  = (fun () -> !proof_using_auto_clear);
@@ -628,8 +626,7 @@ module Bullet = struct
   let current_behavior = ref Strict.strict
 
   let _ =
-    Goptions.declare_string_option {Goptions.
-      optsync = true;
+    Goptions.(declare_string_option {
       optdepr = false;
       optname = "bullet behavior";
       optkey = ["Bullet";"Behavior"];
@@ -642,7 +639,7 @@ module Bullet = struct
           with Not_found ->
             CErrors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
       end
-    }
+    })
 
   let put p b =
     (!current_behavior).put p b
@@ -696,9 +693,7 @@ let parse_goal_selector = function
       end
 
 let _ =
-  Goptions.declare_string_option {Goptions.
-                                  optsync = true ;
-                                  optdepr = false;
+  Goptions.(declare_string_option{optdepr = false;
                                   optname = "default goal selector" ;
                                   optkey = ["Default";"Goal";"Selector"] ;
                                   optread = begin fun () ->
@@ -708,7 +703,7 @@ let _ =
                                   optwrite = begin fun n ->
                                     default_goal_selector := parse_goal_selector n
                                   end
-                                 }
+                                 })
 
 
 module V82 = struct
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);
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index cb3538422..7cd526843 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -52,7 +52,7 @@ let strong_cbn flags =
 
 let simplIsCbn = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname =
     "Plug the simpl tactic to the new cbn mechanism";
   Goptions.optkey = ["SimplIsCbn"];