From 72d1a646accdb8252da01eb082986de52bc6052c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 30 Oct 2001 16:10:21 +0000
Subject: 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
---
 pretyping/detyping.ml | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

(limited to 'pretyping')

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*)
-- 
cgit v1.2.3