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, 18 insertions, 10 deletions

diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 6b5abf41c2..7953f1182c 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -22,21 +22,29 @@ open Declarations
 
 (*s AutoInline parameter *)
 
-let auto_inline_params = 
-  {optsyncname = "Extraction AutoInline";
-   optsynckey = SecondaryTable ("Extraction", "AutoInline");
-   optsyncdefault = true }
+let auto_inline_ref = ref true
 
-let auto_inline = declare_sync_bool_option auto_inline_params
+let auto_inline () = !auto_inline_ref
+
+let _ = declare_bool_option 
+	  {optsync = true;
+	   optname = "Extraction AutoInline";
+	   optkey = SecondaryTable ("Extraction", "AutoInline");
+	   optread = auto_inline; 
+	   optwrite = (:=) auto_inline_ref}
 
 (*s Optimize parameter *)
 
-let optim_params = 
-  {optsyncname = "Extraction Optimize";
-   optsynckey = SecondaryTable ("Extraction", "Optimize");
-   optsyncdefault = true }
+let optim_ref = ref true
+
+let optim () = !optim_ref 
 
-let optim = declare_sync_bool_option optim_params
+let _ = declare_bool_option 
+	  {optsync = true; 
+	   optname = "Extraction Optimize";
+	   optkey = SecondaryTable ("Extraction", "Optimize");
+	   optread = optim; 
+	   optwrite = (:=) optim_ref}
 
 
 (*s Set and Map over global reference *)