From cb316573aa1d09433531e7c67e320c14ef05c3e2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 14 Mar 2017 18:38:42 +0100
Subject: [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.
---
 proofs/proof_using.ml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'proofs/proof_using.ml')

diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index 2c489d6ded..a71b98910e 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);
-- 
cgit v1.2.3