Merge PR#481: [option] Remove support for non-synchronous options.

10 files changed, 23 insertions, 39 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index bd7350dc4e..782552583d 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -177,7 +177,7 @@ let cofixp_reducible flgs _ stk =
 
 let debug_cbv = ref false
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname = "cbv visited constants display";
   Goptions.optkey = ["Debug";"Cbv"];
   Goptions.optread = (fun () -> !debug_cbv);
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)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 98a00f4332..3ef17912f7 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -33,14 +33,13 @@ open Globnames
 let use_typeclasses_for_conversion = ref true
 
 let _ =
-  Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      optdepr  = false;
+  Goptions.(declare_bool_option
+    { optdepr  = false;
       optname  = "use typeclass resolution during conversion";
       optkey   = ["Typeclass"; "Resolution"; "For"; "Conversion"];
       optread  = (fun () -> !use_typeclasses_for_conversion);
       optwrite = (fun b -> use_typeclasses_for_conversion := b) }
-
+    )
 
 (* Typing operations dealing with coercions *)
 exception NoCoercion
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 92359420e9..752819aa39 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -133,8 +133,7 @@ let wildcard_value = ref true
 let force_wildcard () = !wildcard_value
 
 let _ = declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "forced wildcard";
 	    optkey   = ["Printing";"Wildcard"];
 	    optread  = force_wildcard;
@@ -144,8 +143,7 @@ let synth_type_value = ref true
 let synthetize_type () = !synth_type_value
 
 let _ = declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "pattern matching return type synthesizability";
 	    optkey   = ["Printing";"Synth"];
 	    optread  = synthetize_type;
@@ -155,8 +153,7 @@ let reverse_matching_value = ref true
 let reverse_matching () = !reverse_matching_value
 
 let _ = declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "pattern-matching reversibility";
 	    optkey   = ["Printing";"Matching"];
 	    optread  = reverse_matching;
@@ -166,8 +163,7 @@ let print_primproj_params_value = ref false
 let print_primproj_params () = !print_primproj_params_value
 
 let _ = declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "printing of primitive projection parameters";
 	    optkey   = ["Printing";"Primitive";"Projection";"Parameters"];
 	    optread  = print_primproj_params;
@@ -177,8 +173,7 @@ let print_primproj_compatibility_value = ref false
 let print_primproj_compatibility () = !print_primproj_compatibility_value
 
 let _ = declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "backwards-compatible printing of primitive projections";
 	    optkey   = ["Printing";"Primitive";"Projection";"Compatibility"];
 	    optread  = print_primproj_compatibility;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6fcbaa8ef5..42aaf3a227 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -34,7 +34,7 @@ type unify_fun = transparent_state ->
 
 let debug_unification = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname =
     "Print states sent to Evarconv unification";
   Goptions.optkey = ["Debug";"Unification"];
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 53df5aa4a5..75fda97b80 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -175,8 +175,7 @@ let is_strict_universe_declarations () = !strict_universe_declarations
 
 let _ =
   Goptions.(declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "strict universe declaration";
 	    optkey   = ["Strict";"Universe";"Declaration"];
 	    optread  = is_strict_universe_declarations;
@@ -184,8 +183,7 @@ let _ =
 
 let _ =
   Goptions.(declare_bool_option
-	  { optsync  = true;
-            optdepr  = false;
+	  { optdepr  = false;
 	    optname  = "minimization to Set";
 	    optkey   = ["Universe";"Minimization";"ToSet"];
 	    optread  = Universes.is_set_minimization;
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);
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 52f424f751..117ed338ee 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,7 +29,7 @@ exception Elimconst
 
 let refolding_in_reduction = ref false
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname =
     "Perform refolding of fixpoints/constants like cbn during reductions";
   Goptions.optkey = ["Refolding";"Reduction"];
@@ -811,7 +811,7 @@ let fix_recarg ((recindices,bodynum),_) stack =
 
 let debug_RAKAM = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname =
     "Print states of the Reductionops abstract machine";
   Goptions.optkey = ["Debug";"RAKAM"];
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 93c71e6ea9..919e95a8ee 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -30,8 +30,7 @@ open Goptions
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "check that typeclasses proof search returns unique solutions";
       optkey   = ["Typeclasses";"Unique";"Solutions"];
       optread  = get_typeclasses_unique_solutions;
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 74fbd2a851..cac6c50572 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -45,7 +45,7 @@ module NamedDecl = Context.Named.Declaration
 
 let keyed_unification = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname = "Unification is keyed";
   Goptions.optkey = ["Keyed";"Unification"];
   Goptions.optread = (fun () -> !keyed_unification);
@@ -56,7 +56,7 @@ let is_keyed_unification () = !keyed_unification
 
 let debug_unification = ref (false)
 let _ = Goptions.declare_bool_option {
-  Goptions.optsync = true; Goptions.optdepr = false;
+  Goptions.optdepr = false;
   Goptions.optname =
     "Print states sent to tactic unification";
   Goptions.optkey = ["Debug";"Tactic";"Unification"];
@@ -257,8 +257,7 @@ let global_pattern_unification_flag = ref true
 open Goptions
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = true;
+    { optdepr  = true;
       optname  = "pattern-unification for existential variables in tactics";
       optkey   = ["Tactic";"Evars";"Pattern";"Unification"];
       optread  = (fun () -> !global_pattern_unification_flag);
@@ -269,8 +268,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
+    { optdepr  = false;
       optname  = "pattern-unification for existential variables in tactics";
       optkey   = ["Tactic";"Pattern";"Unification"];
       optread  = (fun () -> !global_pattern_unification_flag);