Patch de goption.ml pour faire marcher les options synchrones. Passage des options d'extraction en synchrone

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

1 files changed, 8 insertions, 18 deletions

diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index bca08db34e..b798d13e43 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -53,31 +53,21 @@ let refs_of_vargl = List.map reference_of_varg
 
 (*s AutoInline parameter *)
 
-let auto_inline_ref = ref true
-
-let auto_inline () = !auto_inline_ref
-
 let auto_inline_params = 
-  {optasyncname = "Extraction AutoInline";
-   optasynckey = SecondaryTable ("Extraction", "AutoInline");
-   optasyncread = auto_inline;
-   optasyncwrite = (fun b ->auto_inline_ref := b)}
+  {optsyncname = "Extraction AutoInline";
+   optsynckey = SecondaryTable ("Extraction", "AutoInline");
+   optsyncdefault = true }
 
-let _ = declare_async_bool_option auto_inline_params
+let auto_inline = declare_sync_bool_option auto_inline_params
 
 (*s Optimize parameter *)
 
-let optim_ref = ref true
-
-let optim () = !optim_ref
-
 let optim_params = 
-  {optasyncname = "Extraction Optimize";
-   optasynckey = SecondaryTable ("Extraction", "Optimize");
-   optasyncread = optim;
-   optasyncwrite = (fun b ->optim_ref := b)}
+  {optsyncname = "Extraction Optimize";
+   optsynckey = SecondaryTable ("Extraction", "Optimize");
+   optsyncdefault = true }
 
-let _ = declare_async_bool_option optim_params
+let optim = declare_sync_bool_option optim_params
 
 (*s Table for custom inlining *)