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.
---
 plugins/ltac/g_ltac.ml4      | 1 -
 plugins/ltac/profile_ltac.ml | 3 +--
 plugins/ltac/tacinterp.ml    | 6 ++----
 plugins/ltac/tactic_debug.ml | 3 +--
 plugins/ltac/tauto.ml        | 6 ++----
 5 files changed, 6 insertions(+), 13 deletions(-)

(limited to 'plugins/ltac')

diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index d717ed0a53..31fcf6c96b 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 a853576f25..7476698520 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 b8c021f188..ef230348f7 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2138,8 +2138,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);
@@ -2148,8 +2147,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 dac15ff79e..84d771bff6 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 4de2081cf8..c7be996163 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);
-- 
cgit v1.2.3