suite du seisme

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

4 files changed, 27 insertions, 16 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 02e2da741..64373877d 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -184,7 +184,7 @@ let extract_to_file = function
 let _ = 
   vinterp_add "ExtractionFile"
     (function 
-       | VARG_STRING lang :: VARG_VARGLIST o :: VARG_STRING f :: vl ->
+       | VARG_STRING lang :: VARG_STRING f :: vl ->
 	   (fun () -> 
 	      let refs = refs_of_vargl vl in
 	      let prm = {strict=strict_language lang;
@@ -230,7 +230,7 @@ let file_suffix = function
 let _ = 
   vinterp_add "ExtractionModule"
     (function 
-       | [VARG_STRING lang; VARG_VARGLIST o; VARG_IDENTIFIER m] ->
+       | [VARG_STRING lang; VARG_IDENTIFIER m] ->
 	   (fun () -> 
 	      Ocaml.current_module := Some m;
 	      let ms = Names.string_of_id m in
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 649d816f6..d0f0e1224 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -15,6 +15,7 @@ open Declarations
 open Util
 open Miniml
 open Table
+open Options
 
 (*s Dummy names. *)
 
@@ -460,10 +461,10 @@ let subst_glob_decl r m = function
   | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t')
   | d -> d
 
-let warning_expansion r t= 
+let warning_expansion r = 
   wARN (hOV 0 [< 'sTR "The constant"; 'sPC;
 		 Printer.pr_global r; 
-    'sTR (" of size "^ (string_of_int (ml_size t))^" "); 
+(*    'sTR (" of size "^ (string_of_int (ml_size t))); *)
     'sPC; 'sTR "is expanded." >])
 
 type extraction_params =  
@@ -496,7 +497,7 @@ let rec optimize prm = function
       let b = expand prm.strict r t in
       let l = if b then 
 	begin
-	  (*i if_verbose i*) warning_expansion r t;
+	  if_verbose warning_expansion r;
 	  List.map (subst_glob_decl r t) l
 	end
       else l in 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index e50b08744..855db902e 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -93,10 +93,11 @@ let module_option r =
   else (String.capitalize (string_of_id m)) ^ "."
 
 let check_ml r d = 
-  if to_inline r then d else 
+  if to_inline r then 
     try 
       find_ml_extraction r 
     with Not_found -> d
+  else d
 
 (*s de Bruijn environments for programs *)
 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 85f1887e2..bca08db34 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -53,22 +53,31 @@ 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 = 
-  {optsyncname = "Extraction AutoInline";
-   optsynckey = SecondaryTable ("Extraction", "AutoInline");
-   optsyncdefault = true}
+  {optasyncname = "Extraction AutoInline";
+   optasynckey = SecondaryTable ("Extraction", "AutoInline");
+   optasyncread = auto_inline;
+   optasyncwrite = (fun b ->auto_inline_ref := b)}
 
-let auto_inline = declare_sync_bool_option auto_inline_params
+let _ = declare_async_bool_option auto_inline_params
 
 (*s Optimize parameter *)
 
-let optim_params = 
-  {optsyncname = "Extraction Optimize";
-   optsynckey = SecondaryTable ("Extraction", "Optimize");
-   optsyncdefault = true}
+let optim_ref = ref true
 
-let optim = declare_sync_bool_option optim_params
+let optim () = !optim_ref
+
+let optim_params = 
+  {optasyncname = "Extraction Optimize";
+   optasynckey = SecondaryTable ("Extraction", "Optimize");
+   optasyncread = optim;
+   optasyncwrite = (fun b ->optim_ref := b)}
 
+let _ = declare_async_bool_option optim_params
 
 (*s Table for custom inlining *)
 
@@ -194,7 +203,7 @@ let extract_inductive r (id2,l2) = match r with
 	[< Printer.pr_global r; 'sPC; 'sTR "is not an inductive type" >]
 
 let _ = 
-  vinterp_add "ExtarctInductive"
+  vinterp_add "ExtractInductive"
     (function 
        | [q1; VARG_VARGLIST (id2 :: l2)] ->
 	   (fun () ->