Reorganisation de Goption. Passage des options l'utilisant en synchrone

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2145 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 12 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index e0c1db1690..2026bdb21b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -195,22 +195,22 @@ open Goptions
 let wildcard_value = ref true
 let force_wildcard () = !wildcard_value
 
-let _ =                           
-  declare_async_bool_option 
-    { optasyncname  = "forced wildcard";
-      optasynckey   = SecondaryTable ("Printing","Wildcard");
-      optasyncread  = force_wildcard;
-      optasyncwrite = (fun v -> wildcard_value := v) }
+let _ = declare_bool_option 
+	  { optsync  = true;
+	    optname  = "forced wildcard";
+	    optkey   = SecondaryTable ("Printing","Wildcard");
+	    optread  = force_wildcard;
+	    optwrite = (:=) wildcard_value }
 
 let synth_type_value = ref true
 let synthetize_type () = !synth_type_value
 
-let _ = 
-  declare_async_bool_option 
-    { optasyncname = "synthesizability";
-      optasynckey   = SecondaryTable ("Printing","Synth");
-      optasyncread = synthetize_type;
-      optasyncwrite = (fun v -> synth_type_value := v) }
+let _ = declare_bool_option 
+	  { optsync  = true;
+	    optname  = "synthesizability";
+	    optkey   = SecondaryTable ("Printing","Synth");
+	    optread  = synthetize_type;
+	    optwrite = (:=) synth_type_value }
 
 (* Auxiliary function for MutCase printing *)
 (* [computable] tries to tell if the predicate typing the result is inferable*)