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.
---
 engine/namegen.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'engine')

diff --git a/engine/namegen.ml b/engine/namegen.ml
index 3b979f206e..5bd62273c8 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -418,8 +418,7 @@ let use_h_based_elimination_names () =
 open Goptions
 
 let _ = declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "use of \"H\"-based proposition names in elimination tactics";
 	    optkey   = ["Standard";"Proposition";"Elimination";"Names"];
 	    optread  = (fun () -> !h_based_elimination_names);
-- 
cgit v1.2.3