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/program.ml | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'pretyping/program.ml')

diff --git a/pretyping/program.ml b/pretyping/program.ml
index 42acc5705b..de485dbe84 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -87,8 +87,7 @@ open Goptions
 
 let _ =
   declare_bool_option
-  { optsync  = true;
-    optdepr  = false;
+  { optdepr  = false;
     optname  = "preferred transparency of Program obligations";
     optkey   = ["Transparent";"Obligations"];
     optread  = get_proofs_transparency;
@@ -96,8 +95,7 @@ let _ =
 
 let _ =
   declare_bool_option
-  { optsync  = true;
-    optdepr  = false;
+  { optdepr  = false;
     optname  = "program cases";
     optkey   = ["Program";"Cases"];
     optread  = (fun () -> !program_cases);
@@ -105,8 +103,7 @@ let _ =
 
 let _ =
   declare_bool_option
-  { optsync  = true;
-    optdepr  = false;
+  { optdepr  = false;
     optname  = "program generalized coercion";
     optkey   = ["Program";"Generalized";"Coercion"];
     optread  = (fun () -> !program_generalized_coercion);
-- 
cgit v1.2.3