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.
---
 pretyping/classops.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'pretyping/classops.ml')

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 32da81f96c..9a973cff55 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)
-- 
cgit v1.2.3