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.
---
 interp/constrextern.ml | 3 +--
 interp/topconstr.ml    | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 59b8b4e5b9..58b38cdacc 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -91,8 +91,7 @@ let record_print = ref true
 let _ =
   let open Goptions in
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "record printing";
       optkey   = ["Printing";"Records"];
       optread  = (fun () -> !record_print);
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index e05be65fb0..239226b2ea 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -21,7 +21,7 @@ open Constrexpr_ops
 
 let asymmetric_patterns = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname = "no parameters in constructors";
   Goptions.optkey = ["Asymmetric";"Patterns"];
   Goptions.optread = (fun () -> !asymmetric_patterns);
-- 
cgit v1.2.3