chambardement important des fichiers auxiliaires. Nouvelle syntaxe pour les options

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

13 files changed, 413 insertions, 333 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index f32b3e96db..51574bda0d 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -16,34 +16,42 @@ Grammar vernac vernac : ast :=
 
 (* Monolithic extraction to a file *)
 | extr_file
-     [ "Extraction" stringarg($f) options($o) ne_qualidarg_list($l) "." ] 
-  -> [ (ExtractionFile "ocaml" $o $f ($LIST $l)) ]
+     [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] 
+  -> [ (ExtractionFile "ocaml" $f ($LIST $l)) ]
 | haskell_extr_file
-     [ "Haskell" "Extraction" stringarg($f) options($o) 
-       ne_qualidarg_list($l) "." ] 
-  -> [ (ExtractionFile "haskell" $o $f ($LIST $l)) ]
+     [ "Haskell" "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] 
+  -> [ (ExtractionFile "haskell" $f ($LIST $l)) ]
 
 (* Modular extraction (one Coq module = one ML module) *)
 | extr_module 
-     [ "Extraction" "Module" options($o) identarg($m) "." ]
-  -> [ (ExtractionModule "ocaml" $o $m) ]
+     [ "Extraction" "Module" identarg($m) "." ]
+  -> [ (ExtractionModule "ocaml" $m) ]
 | haskell_extr_module 
-     [ "Haskell" "Extraction" "Module" options($o) identarg($m) "." ]
-  -> [ (ExtractionModule "haskell" $o $m) ]
+     [ "Haskell" "Extraction" "Module" identarg($m) "." ]
+  -> [ (ExtractionModule "haskell" $m) ]
+
+(* Custum inlining directives *)
+| inline_constant
+     [ "Extraction" "Inline" ne_qualidarg_list($l) "." ] 
+  -> [ (ExtractionInline ($LIST $l)) ]
+     
+| no_inline_constant 
+     [ "Extraction" "NoInline" ne_qualidarg_list($l) "." ] 
+  -> [ (ExtractionNoInline ($LIST $l)) ]
 
 (* Overriding of a Coq object by an ML one *)
 | extract_constant 
      [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ]
-  -> [ (EXTRACT_CONSTANT $x $y) ]
+  -> [ (ExtractConstant $x $y) ]
 
 | extract_inlined_constant 
      [ "Extract" "Inlined" "Constant" qualidarg($x) 
       "=>" idorstring($y) "." ]
-  -> [ (EXTRACT_INLINED_CONSTANT $x $y) ]
+  -> [ (ExtractInlinedConstant $x $y) ]
 
 | extract_inductive 
      [ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."]
-  -> [ (EXTRACT_INDUCTIVE $x $y) ]
+  -> [ (ExtractInductive $x $y) ]
 
 (* Utility entries *)
 with mindnames : ast :=
@@ -57,9 +65,4 @@ with idorstring_list: ast list :=
 with idorstring : ast :=
   ids_ident  [ identarg($id) ] -> [ $id ]
 | ids_string [ stringarg($s) ] -> [ $s ]
-
-with options : ast :=
-| ext_opt_noopt [ "[" "noopt" "]" ] -> [ (VERNACARGLIST "noopt") ]
-| ext_op_expand [ "[" "expand" ne_qualidarg_list($l) "]" ] -> 
-                [ (VERNACARGLIST "expand" ($LIST $l)) ]
-| ext_opt_none  [ ] -> [ (VERNACARGLIST "nooption") ].
+.
\ No newline at end of file
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index d726d4fa33..02e2da7419 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -15,7 +15,9 @@ open Term
 open Lib
 open Extraction
 open Miniml
+open Table
 open Mlutil
+open Vernacinterp
 
 (*s Recursive computation of the global references to extract. 
     We use a set of functions visiting the extracted objects in
@@ -85,6 +87,7 @@ and visit_decl eenv = function
       visit_type eenv t
   | Dglob (_,a) ->
       visit_ast eenv a
+  | Dcustom _ -> ()
 
 (*s Recursive extracted environment for a list of reference: we just
     iterate [visit_reference] on the list, starting with an empty
@@ -110,17 +113,16 @@ end
 
 module Pp = Ocaml.Make(ToplevelParams)
 
-open Vernacinterp
-
 let refs_set_of_list l = List.fold_right Refset.add l Refset.empty 
 
 let decl_of_refs refs =
-  let params = 
-    { modular = false ; module_name = "" ; 
-    optimization = true ; to_keep = refs_set_of_list refs;
-    to_expand = Refset.empty } in
-  let rl = List.map extract_declaration (extract_env refs) in
-  optimize params rl
+  List.map extract_declaration (extract_env refs) 
+
+let local_optimize refs = 
+  let prm = 
+    { strict = true ; modular = false ; 
+      module_name = "" ; to_appear = refs} in
+  optimize prm (decl_of_refs refs)
 
 let print_user_extract r = 
   mSGNL [< 'sTR "User defined extraction:"; 'sPC; 'sTR (find_ml_extraction r) ; 'fNL>]
@@ -129,7 +131,7 @@ let extract_reference r =
   if is_ml_extraction r then
     print_user_extract r 
   else
-    mSGNL (Pp.pp_decl (list_last (decl_of_refs [r])))
+    mSGNL (Pp.pp_decl (list_last (local_optimize [r])))
 
 let _ = 
   vinterp_add "Extraction"
@@ -153,17 +155,6 @@ let _ =
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
     to get the saturated environment to extract. *)
 
-let no_such_reference q =
-  errorlabstrm "reference_of_varg" 
-    [< Nametab.pr_qualid q; 'sTR ": no such reference" >]
-
-let reference_of_varg = function
-  | VARG_QUALID q -> 
-      (try Nametab.locate q with Not_found -> no_such_reference q)
-  | _ -> assert false
-
-let refs_of_vargl = List.map reference_of_varg
-
 let _ = 
   vinterp_add "ExtractionRec"
     (fun vl () ->
@@ -181,22 +172,6 @@ let strict_language = function
   | "haskell" -> false
   | _ -> assert false
 
-let interp_options lang keep modular m = function
-  | [VARG_STRING "noopt"] ->
-      { optimization = false; modular = modular; module_name = m;
-	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
-  | [VARG_STRING "nooption"] ->
-      { optimization = strict_language lang; 
-	modular = modular; module_name = m;
-	to_keep = refs_set_of_list keep; to_expand = Refset.empty }
-  | VARG_STRING "expand" :: l ->
-      { optimization = strict_language lang; 
-	modular = modular; module_name = m;
-	to_keep = refs_set_of_list keep; 
-	to_expand = refs_set_of_list (refs_of_vargl l) }
-  | _ -> 
-      assert false
-
 (*s Extraction to a file (necessarily recursive). 
     The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn].
     We just call [extract_to_file] on the saturated environment. *)
@@ -212,15 +187,14 @@ let _ =
        | VARG_STRING lang :: VARG_VARGLIST o :: VARG_STRING f :: vl ->
 	   (fun () -> 
 	      let refs = refs_of_vargl vl in
-	      let prm = interp_options lang refs false "" o in
+	      let prm = {strict=strict_language lang;
+			 modular=false;
+			 module_name="";
+			 to_appear= refs} in 
 	      let decls = decl_of_refs refs in 
+	      let decls = add_ml_decls prm decls in 
 	      let decls = optimize prm decls in
-	      let ml_decls = 
-		list_subtract 
-		  (List.filter is_ml_extraction refs)
-		  (fst (ml_cst_extractions ()))
-	      in
-	      extract_to_file lang f prm decls ml_decls)
+	      extract_to_file lang f prm decls)
        | _ -> assert false)
 
 (*s Extraction of a module. The vernacular command is \verb!Extraction Module!
@@ -246,6 +220,7 @@ let decl_mem rl = function
   | Dabbrev (r,_,_) -> List.mem r rl 
   | Dtype ((_,r,_)::_, _) -> List.mem r rl
   | Dtype ([],_) -> false
+  | Dcustom (r,s) ->  List.mem r rl 
 
 let file_suffix = function
   | "ocaml" -> ".ml"
@@ -260,9 +235,13 @@ let _ =
 	      Ocaml.current_module := Some m;
 	      let ms = Names.string_of_id m in
 	      let f = (String.uncapitalize ms) ^ (file_suffix lang) in
-	      let prm = interp_options lang [] true ms o in
+	      let prm = {strict=strict_language lang;
+			 modular=true;
+			 module_name= Names.string_of_id m;
+			 to_appear= []} in 
 	      let rl = extract_module m in 
 	      let decls = optimize prm (decl_of_refs rl) in
+	      let decls = add_ml_decls prm decls in 
 	      let decls = List.filter (decl_mem rl) decls in
-	      extract_to_file lang f prm decls [])
+	      extract_to_file lang f prm decls)
        | _ -> assert false)
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index f5b28598c7..23264fb075 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -18,6 +18,7 @@ open Reduction
 open Inductive
 open Instantiate
 open Miniml
+open Table
 open Mlutil
 open Closure
 open Summary
@@ -892,7 +893,7 @@ and extract_inductive_declaration sp =
 (*s Extraction of a global reference i.e. a constant or an inductive. *)
 
 let false_rec_sp = path_of_string "Coq.Init.Specif.False_rec"
-let false_rec_e = MLlam (prop_name, MLexn (id_of_string "False_rec"))
+let false_rec_e = MLlam (prop_name, MLexn "False_rec")
 
 let extract_declaration r = match r with
   | ConstRef sp when sp = false_rec_sp -> Dglob (r, false_rec_e)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 057767f5e6..9549829862 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -196,9 +196,8 @@ let rec pp_expr par env args =
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args
-    | MLexn id -> 
-	[< open_par par; 'sTR "error"; 'sPC; 
-	   'qS (string_of_id id); close_par par >]
+    | MLexn str -> 
+	[< open_par par; 'sTR "error"; 'sPC; 'qS str; close_par par >]
     | MLprop ->
 	string "prop"
     | MLarity ->
@@ -223,10 +222,7 @@ and pp_pat env pv =
 	     end;
 	     'sTR " ->"; 'sPC; pp_expr par env' [] t >]
   in 
-  if pv = [||] then
-    [< 'sTR "_ -> error \"shouldn't happen\" -- empty inductive" >]
-  else
-    [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "  " >]) pp_one_pat pv >]
+  [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "  " >]) pp_one_pat pv >]
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)
@@ -313,6 +309,9 @@ let pp_decl = function
 	   [< >] >]
   | Dglob (r, a) ->
       hOV 0 [< pp_function (empty_env ()) (pp_global r) a; 'fNL >]
+  | Dcustom (r,s) -> 
+      hOV 0  [< 'sTR (string_of_r r); 'sTR " ="; 
+		'sPC; 'sTR s; 'fNL  >]
 
 let pp_type = pp_type false
 
@@ -407,23 +406,11 @@ let haskell_preamble prm =
      'sTR "type Arity = ()"; 'fNL;
      'sTR "arity = ()"; 'fNL; 'fNL >]
 
-let haskell_header ft b ml_decls =
-  let l,l' = ml_cst_extractions () in
-  List.iter2 
-    (fun r s -> 
-       if (not b) or (Some (module_of_r r) = !current_module)  then 
-       pP_with ft (hV 0  
-	 [< 'sTR (string_of_r r); 'sTR " ="; 'sPC; 'sTR s; 'fNL ; 'fNL >]))
-    ((List.rev l) @ ml_decls)
-    ((List.rev l') @ (List.map find_ml_extraction ml_decls))
-
-
-let extract_to_file f prm decls ml_decls=
+let extract_to_file f prm decls=
   let pp_decl = if prm.modular then ModularPp.pp_decl else MonoPp.pp_decl in
   let cout = open_out f in
   let ft = Pp_control.with_output_to cout in
   pP_with ft (hV 0 (haskell_preamble prm));
-  haskell_header ft prm.modular ml_decls;
   begin 
     try
       List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 4f380271f5..fa10cb1bd9 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -15,4 +15,4 @@ open Mlutil
 open Names
 
 val extract_to_file : 
-  string -> extraction_params -> ml_decl list -> global_reference list -> unit
+  string -> extraction_params -> ml_decl list -> unit
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index c2ed8e7a97..d8a9597e18 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -40,7 +40,7 @@ type ml_ast =
   | MLcons  of global_reference * ml_ast list
   | MLcase  of ml_ast * (global_reference * identifier list * ml_ast) array
   | MLfix   of int * identifier array * ml_ast array
-  | MLexn   of identifier
+  | MLexn   of string
   | MLprop
   | MLarity
   | MLcast  of ml_ast * ml_type
@@ -52,6 +52,7 @@ type ml_decl =
   | Dtype   of ml_ind list * bool (* cofix *)
   | Dabbrev of global_reference * identifier list * ml_type
   | Dglob   of global_reference * ml_ast
+  | Dcustom of global_reference * string
 
 (*s Pretty-printing of MiniML in a given concrete syntax is parameterized
     by a function [pp_global] that pretty-prints global references. 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index cb555a67a4..649d816f6d 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -9,14 +9,12 @@
 (*i $Id$ i*)
 
 open Pp
-open Options
 open Names
 open Term
 open Declarations
-open Libobject
-open Lib
 open Util
 open Miniml
+open Table
 
 (*s Dummy names. *)
 
@@ -218,12 +216,10 @@ let check_identity_case br =
 	  check_list (List.length l) l'
       | _ -> raise Impossible
   in 
-  if br=[||] then raise Impossible;
   Array.iter check_one_branch br
 
 
 let check_constant_case br = 
-  if br = [||] then raise Impossible; 
   let (r,l,t) = br.(0) in
   let n = List.length l in 
   if occurs_itvl 1 n t then raise Impossible; 
@@ -234,7 +230,19 @@ let check_constant_case br =
     if (occurs_itvl 1 n t) || (cst <> (ml_lift (-n) t)) 
     then raise Impossible
   done; cst
-      
+
+
+let all_constr br = 
+  try 
+    Array.iter 
+      (fun (_,_,t)-> 
+	 match t with 
+	   | MLcons _ -> () 
+	   | _ -> raise Impossible) 
+      br;
+    true
+  with Impossible -> false
+  
 
 let rec betaiota = function
   | MLapp (f, []) ->
@@ -261,26 +269,37 @@ let rec betaiota = function
       	       	 (fun (n,l,t) -> 
 		    let k = List.length l in
 		    let a'' = List.map (ml_lift k) a' in
-      	       	    (n, l, betaiota (MLapp (t,a'')))) 
+      	       	      (n, l, betaiota (MLapp (t,a'')))) 
 		 br 
-	     in
-      	     betaiota (MLcase (e,br'))
+	     in betaiota (MLcase (e,br'))
 	 | _ ->
 	     MLapp (f',a'))
+  | MLcase (e,[||]) ->
+      MLexn "Empty inductive"
   | MLcase (e,br) ->
       (match betaiota e with
-	 (* iota redex *)
-	 | MLcons (r,a) ->
-	     let j = constructor_index r in
-	     let (_,ids,c) = br.(j) in
+	   (* iota redex *)
+	 | MLcons (r,a) ->  
+	     let (_,ids,c) = br.(constructor_index r) in
 	     let c' = List.fold_right (fun id t -> MLlam (id,t)) ids c in
 	     betaiota (MLapp (c',a))
+	 | MLcase(e',br') when (all_constr br') ->
+	     let new_br= 
+	       Array.map 
+		 (function 
+		    | (n, i, MLcons (r,a))-> 
+			let (_,ids,c) = br.(constructor_index r) in
+			let c = ml_lift (List.length i) c in 
+			let c' = List.fold_right (fun id t -> MLlam (id,t)) ids c in
+			(n,i,betaiota (MLapp (c',a)))
+		    | _ -> assert false) br'
+	     in MLcase(e', new_br)
 	 | e' -> 
 	     let br' = Array.map (fun (n,l,t) -> (n,l,betaiota t)) br in 
-	     try check_identity_case br'; e' 
-	     with Impossible -> 
-	       try check_constant_case br' 
-	       with Impossible -> MLcase (e', br'))
+		 try check_identity_case br'; e' 
+		 with Impossible -> 
+		   try check_constant_case br' 
+		   with Impossible -> MLcase (e', br'))
   | MLletin(_,c,e) when (is_atomic c) || (nb_occur e <= 1) -> 
       (* expansion of a letin in special cases *)
       betaiota (ml_subst c e)
@@ -289,23 +308,12 @@ let rec betaiota = function
     
 let normalize a = betaiota (merge_app a)
 
+let optional_normalize a = a (* TODO *)
+
 let normalize_decl = function
  | Dglob (id, a) -> Dglob (id, normalize a)
  | d -> d
 
-(*s Extraction parameters *)
-
-module Refset = 
-  Set.Make(struct type t = global_reference let compare = compare end)
-
-type extraction_params = {
-  modular : bool;       (* modular extraction *)
-  module_name : string; (* module name if [modular] *)
-  optimization : bool;  (* we need optimization *)
-  to_keep : Refset.t;   (* globals to keep *)
-  to_expand : Refset.t; (* globals to expand *)
-}
-
 (*s Utility functions used for the decision of expansion *)
 
 let rec ml_size = function
@@ -344,7 +352,7 @@ exception Toplevel
 
 let lift n l = List.map ((+) n) l
 
-let pop n l = List.map (fun x -> if x-n<0 then raise Toplevel else x-n) l 
+let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l 
 
 (* This function returns a list of de Bruijn indices of non-strict variables,
    or raises [Toplevel] if it has an internal non-strict variable. 
@@ -361,10 +369,11 @@ let rec non_stricts add cand = function
       pop 1 (non_stricts add cand t)
   | MLrel n -> 
       List.filter ((<>) n) cand  
-(*i old particular case 
   | MLapp (MLrel n, _) -> 
-      List.filter ((<>) n) cand  
-	(* In [(x y)] we say that only x is strict. (WHY?) *) i*)
+      List.filter ((<>) n) cand
+	(* In [(x y)] we say that only x is strict. Cf [sig_rec]. 
+	   We may gain something if x is replaced by a function like
+	   a projection *)
   | MLapp (t,l)-> 
       let cand = non_stricts false cand t in 
       List.fold_left (non_stricts false) cand l 
@@ -412,30 +421,31 @@ let is_not_strict t =
    If we could expand [t] (the user said nothing special), 
    should we expand ? 
    
-   We don't expand fixpoints, but always inductive constructors.
-   Last case of expansion is a term not to big with at least one 
-   non-strict variable (i.e. a variable that may not be evaluated). *)
+   We don't expand fixpoints, but always inductive constructors
+   and small terms.
+   Last case of expansion is a term with at least one non-strict 
+   variable (i.e. a variable that may not be evaluated). *)
 
 let expansion_test t = 
   (not (is_fix t))
   &&
-  ((is_constr t) 
-   ||
-   (ml_size t < 10 && is_not_strict t))
+  ((is_constr t) ||
+   (ml_size t < 3) ||
+   ((ml_size t < 12) && (is_not_strict t)))
 
 (* If the user doesn't say he wants to keep [t], we expand in two cases:
    \begin{itemize}
    \item the user explicitly requests it 
    \item [expansion_test] answers that the expansion is a good idea, and 
-   we are free to act (no [noopt] given as argument)
+   we are free to act (AutoInline is set)
    \end{itemize} *)
 
-let expand prm r t = 
-  (not (Refset.mem r prm.to_keep)) (* the user DOES want to keep it *)
+let expand strict_lang r t = 
+  (not (to_keep r)) (* the user DOES want to keep it *)
   &&
-  (Refset.mem r prm.to_expand (* the user DOES want to expand it *) 
+  ((to_inline r) (* the user DOES want to expand it *) 
    || 
-   (prm.optimization && expansion_test t)) 
+   (auto_inline () && strict_lang && expansion_test t)) 
 
 (*s Optimization *)
 
@@ -450,178 +460,47 @@ let subst_glob_decl r m = function
   | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t')
   | d -> d
 
-let warning_expansion r = 
+let warning_expansion r t= 
   wARN (hOV 0 [< 'sTR "The constant"; 'sPC;
-		 Printer.pr_global r; 'sPC; 'sTR "is expanded." >])
+		 Printer.pr_global r; 
+    'sTR (" of size "^ (string_of_int (ml_size t))^" "); 
+    'sPC; 'sTR "is expanded." >])
+
+type extraction_params =  
+  { strict : bool ; 
+    modular : bool ; 
+    module_name : string ; 
+    to_appear : global_reference list }
+
+let print_ml_decl prm (r,_) = 
+  not (to_inline r) || List.mem r prm.to_appear
+
+let add_ml_decls prm decls = 
+  let l = sorted_ml_extractions () in 
+  let l = List.filter (print_ml_decl prm) l in 
+  let l = List.map (fun (r,s)-> Dcustom (r,s)) l in 
+  (List.rev l @ decls)
 
 let rec optimize prm = function
   | [] -> 
       []
-  | (Dtype _ | Dabbrev _) as d :: l -> 
+  | (Dtype _ | Dabbrev _ | Dcustom _) as d :: l -> 
       d :: (optimize prm l)
   | Dglob (r, MLprop) as d :: l ->
-      if Refset.mem r prm.to_keep then
+      if List.mem r prm.to_appear then
 	d :: (optimize prm l) 
       else optimize prm l
-  (*i
-  | Dglob(id,(MLexn _ as t)) as d :: l ->
-      let l' = List.map (expand (id,t)) l in optimize prm l'
-  i*)	    
   | Dglob (r,t) :: l ->
       let t = normalize t in
-      let b = expand prm r t in
+      let t = if optim() then optional_normalize t else t in 
+      let b = expand prm.strict r t in
       let l = if b then 
 	begin
-	  if_verbose warning_expansion r;
+	  (*i if_verbose i*) warning_expansion r t;
 	  List.map (subst_glob_decl r t) l
 	end
       else l in 
-      if prm.modular || l = [] || not b then 
+      if prm.modular || List.mem r prm.to_appear || not b then 
 	Dglob (r,t) :: (optimize prm l)
       else
 	optimize prm l
-
-(*s Table for direct ML extractions. *)
-
-module Refmap = 
-  Map.Make(struct type t = global_reference let compare = compare end)
-
-let empty_extractions = (Refmap.empty, Refset.empty)
-
-let extractions = ref empty_extractions
-
-let ml_extractions () = snd !extractions
-
-let add_ml_extraction r s = 
-  let (map,set) = !extractions in
-  extractions := (Refmap.add r s map, Refset.add r set)
-
-let is_ml_extraction r = Refset.mem r (snd !extractions)
-
-let find_ml_extraction r = Refmap.find r (fst !extractions)
-
-(*s Registration of operations for rollback. *)
-
-let (in_ml_extraction,_) = 
-  declare_object ("ML extractions",
-		  { cache_function = (fun (_,(r,s)) -> add_ml_extraction r s);
-		    load_function = (fun (_,(r,s)) -> add_ml_extraction r s);
-		    open_function = (fun _ -> ());
-		    export_function = (fun x -> Some x) })
-
-(*s Registration of the table for rollback. *)
-
-open Summary
-
-let _ = declare_summary "ML extractions"
-	  { freeze_function = (fun () -> !extractions);
-	    unfreeze_function = ((:=) extractions);
-	    init_function = (fun () -> extractions := empty_extractions);
-	    survive_section = true }
-
-(*s List of Extract Constant directives *)
-
-let cst_extractions = ref ([],[])
-
-let ml_cst_extractions () = !cst_extractions
-
-let add_ml_cst_extraction r s = 
-  let l,l' = !cst_extractions in 
-  cst_extractions := r::l,s::l'
-
-let (in_ml_cst_extraction,_) = 
-  declare_object ("ML constants extractions",
-		  { cache_function = (fun (_,(r,s)) -> add_ml_cst_extraction r s);
-		    load_function = (fun (_,(r,s)) -> add_ml_cst_extraction r s);
-		    open_function = (fun _ -> ());
-		    export_function = (fun x -> Some x) })
-
-let _ = declare_summary "ML constants extractions"
-	  { freeze_function = (fun () -> !cst_extractions);
-	    unfreeze_function = ((:=) cst_extractions);
-	    init_function = (fun () -> cst_extractions := [],[]);
-	    survive_section = true }
-
-(*s Grammar entries. *)
-
-open Vernacinterp
-
-let string_of_varg = function
-  | VARG_IDENTIFIER id -> string_of_id id
-  | VARG_STRING s -> s
-  | _ -> assert false
-
-let no_such_reference q =
-  errorlabstrm "reference_of_varg" 
-    [< Nametab.pr_qualid q; 'sTR ": no such reference" >]
-
-let reference_of_varg = function
-  | VARG_QUALID q -> 
-      (try Nametab.locate q with Not_found -> no_such_reference q)
-  | _ -> assert false
-
-(*s \verb!Extract Constant qualid => string! *)
-
-let extract_constant r s = match r with
-  | ConstRef sp -> 
-      let rs = string_of_id (basename sp) in
-      add_anonymous_leaf (in_ml_cst_extraction (r,s));
-      add_anonymous_leaf (in_ml_extraction (r,rs))
-  | _ -> 
-      errorlabstrm "extract_constant"
-	[< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >]
-
-let _ = 
-  vinterp_add "EXTRACT_CONSTANT"
-    (function 
-       | [id; s] -> 
-	   (fun () -> 
-	      extract_constant 
-		(reference_of_varg id)
-		(string_of_varg s))
-       | _ -> assert false)
-
-(*s \verb!Extract Inlined Constant qualid => string! *)
-
-let extract_inlined_constant r s = match r with
-  | ConstRef _ -> 
-      add_anonymous_leaf (in_ml_extraction (r,s))
-  | _ -> 
-      errorlabstrm "extract_constant"
-	[< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >]
-
-let _ = 
-  vinterp_add "EXTRACT_INLINED_CONSTANT"
-    (function 
-       | [id; s] -> 
-	   (fun () -> 
-	      extract_inlined_constant 
-		(reference_of_varg id) 
-		(string_of_varg s))
-       | _ -> assert false)
-
-(*s \verb!Extract Inductive qualid => string [ string ... string ]! *)
-
-let extract_inductive r (id2,l2) = match r with
-  | IndRef ((sp,i) as ip) ->
-      let mib = Global.lookup_mind sp in
-      let n = Array.length mib.mind_packets.(i).mind_consnames in
-      if n <> List.length l2 then
-	error "not the right number of constructors";
-      add_anonymous_leaf (in_ml_extraction (r,id2));
-      list_iter_i
-	(fun j s -> 
-	   add_anonymous_leaf 
-	     (in_ml_extraction (ConstructRef (ip,succ j),s))) l2
-  | _ -> 
-      errorlabstrm "extract_inductive"
-	[< Printer.pr_global r; 'sPC; 'sTR "is not an inductive type" >]
-
-let _ = 
-  vinterp_add "EXTRACT_INDUCTIVE"
-    (function 
-       | [q1; VARG_VARGLIST (id2 :: l2)] ->
-	   (fun () -> 
-	      extract_inductive (reference_of_varg q1) 
-		(string_of_varg id2, List.map string_of_varg l2))
-       | _ -> assert false)
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 6f7168ed07..27608c46fe 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -50,30 +50,17 @@ val subst_glob_ast : global_reference -> ml_ast -> ml_ast -> ml_ast
 val normalize : ml_ast -> ml_ast
 val normalize_decl : ml_decl -> ml_decl
 
-(*s Extraction parameters *)
-
-module Refset : Set.S with type elt = global_reference
-
-type extraction_params = {
-  modular : bool;       (* modular extraction *)
-  module_name : string; (* module name if [modular] *)
-  optimization : bool;  (* we need optimization *)
-  to_keep : Refset.t;   (* globals to keep *)
-  to_expand : Refset.t; (* globals to expand *)
-}
-
 (*s Optimization. *)
 
-val optimize : extraction_params -> ml_decl list -> ml_decl list
-
-(*s Table for direct extractions to ML values. *)
-
-val is_ml_extraction : global_reference -> bool
-val find_ml_extraction : global_reference -> string
+type extraction_params =  
+  { strict : bool; 
+    modular : bool; 
+    module_name : string; 
+    to_appear : global_reference list }
 
-val ml_extractions : unit -> Refset.t
+val add_ml_decls : 
+  extraction_params -> ml_decl list -> ml_decl list
 
-(* List of Extract Constant directives *)
+val optimize : 
+  extraction_params -> ml_decl list -> ml_decl list
 
-val ml_cst_extractions : 
-  unit -> global_reference list * string list
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 81d77741b0..e50b087442 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -15,6 +15,7 @@ open Util
 open Names
 open Term
 open Miniml
+open Table
 open Mlutil
 open Options
 
@@ -92,8 +93,10 @@ let module_option r =
   else (String.capitalize (string_of_id m)) ^ "."
 
 let check_ml r d = 
-  try find_ml_extraction r
-  with Not_found -> d
+  if to_inline r then d else 
+    try 
+      find_ml_extraction r 
+    with Not_found -> d
 
 (*s de Bruijn environments for programs *)
 
@@ -233,9 +236,9 @@ let rec pp_expr par env args =
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args
-    | MLexn id -> 
-	[< open_par par; 'sTR "failwith"; 'sPC; 
-	   'qS (string_of_id id); close_par par >]
+    | MLexn str -> 
+	[< open_par par; 'sTR "assert false"; 'sPC; 
+	   'sTR ("(* "^str^" *)"); close_par par >]
     | MLprop ->
 	string "prop"
     | MLarity ->
@@ -258,10 +261,7 @@ and pp_pat env pv =
 	     end;
 	     'sTR " ->"; 'sPC; pp_expr par env' [] t >]
   in 
-  if pv = [||] then
-    [< 'sTR "_ -> assert false (* empty inductive *)" >]
-  else
-    [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) pp_one_pat pv >]
+  [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) pp_one_pat pv >]
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)
@@ -367,6 +367,9 @@ let pp_decl = function
   | Dglob (r, a) ->
       hOV 0 [< 'sTR "let "; 
 	       pp_function (empty_env ()) (pp_global r) a; 'fNL >]
+  | Dcustom (r,s) -> 
+      hOV 0 [< 'sTR "let "; 'sTR (string_of_r r); 
+	       'sTR " ="; 'sPC; 'sTR s; 'fNL >]
 
 let pp_type = pp_type false
 
@@ -461,23 +464,11 @@ let ocaml_preamble () =
      'sTR "type arity = unit"; 'fNL;
      'sTR "let arity = ()"; 'fNL; 'fNL >]
 
-
-let ocaml_header ft b ml_decls =
-  let l,l' = ml_cst_extractions () in
-  List.iter2 
-    (fun r s -> 
-       if (not b) or (Some (module_of_r r) = !current_module)  then 
-       pP_with ft (hV 0  
-	 [< 'sTR "let "; 'sTR (string_of_r r); 'sTR " ="; 'sPC; 'sTR s; 'fNL ; 'fNL >]))
-    ((List.rev l) @ ml_decls)
-    ((List.rev l') @ (List.map find_ml_extraction ml_decls))
-
-let extract_to_file f prm decls ml_decls =
+let extract_to_file f prm decls =
   let pp_decl = if prm.modular then ModularPp.pp_decl else MonoPp.pp_decl in
   let cout = open_out f in
   let ft = Pp_control.with_output_to cout in
   pP_with ft (hV 0 (ocaml_preamble ()));
-  ocaml_header ft prm.modular ml_decls;
   begin 
     try
       List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index e1325d4814..58ee9b662f 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -43,6 +43,6 @@ module Make : functor(P : Mlpp_param) -> Mlpp
 
 val current_module : Names.identifier option ref
 val extract_to_file : 
-  string -> extraction_params -> ml_decl list -> global_reference list -> unit
+  string -> extraction_params -> ml_decl list -> unit
 
 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
new file mode 100644
index 0000000000..85f1887e2a
--- /dev/null
+++ b/contrib/extraction/table.ml
@@ -0,0 +1,203 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Summary
+open Goptions
+open Vernacinterp
+open Names
+open Util
+open Pp
+open Libobject
+open Term
+open Declarations
+open Lib
+
+(*s Set and Map over global reference *)
+
+module Refset = 
+  Set.Make(struct type t = global_reference let compare = compare end)
+
+module Refmap = 
+  Map.Make(struct type t = global_reference let compare = compare end)
+
+(*s Auxiliary functions *) 
+
+let check_constant r = match r with 
+  | ConstRef sp -> r 
+  | _ -> errorlabstrm "extract_constant"
+	[< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >] 
+
+let string_of_varg = function
+  | VARG_IDENTIFIER id -> string_of_id id
+  | VARG_STRING s -> s
+  | _ -> assert false
+
+let no_such_reference q =
+  errorlabstrm "reference_of_varg" 
+    [< Nametab.pr_qualid q; 'sTR ": no such reference" >]
+
+let reference_of_varg = function
+  | VARG_QUALID q -> 
+      (try Nametab.locate q with Not_found -> no_such_reference q)
+  | _ -> assert false
+
+let refs_of_vargl = List.map reference_of_varg
+
+
+(*s AutoInline parameter *)
+
+let auto_inline_params = 
+  {optsyncname = "Extraction AutoInline";
+   optsynckey = SecondaryTable ("Extraction", "AutoInline");
+   optsyncdefault = true}
+
+let auto_inline = declare_sync_bool_option auto_inline_params
+
+(*s Optimize parameter *)
+
+let optim_params = 
+  {optsyncname = "Extraction Optimize";
+   optsynckey = SecondaryTable ("Extraction", "Optimize");
+   optsyncdefault = true}
+
+let optim = declare_sync_bool_option optim_params
+
+
+(*s Table for custom inlining *)
+
+let empty_inline_table = (Refset.empty,Refset.empty)
+
+let inline_table = ref empty_inline_table
+
+let to_inline r = Refset.mem r (fst !inline_table)
+
+let to_keep r = Refset.mem r (snd !inline_table)
+
+let add_inline_entries b l = 
+  let f b = if b then Refset.add else Refset.remove in 
+  let i,k = !inline_table in 
+  inline_table := 
+     (List.fold_right (f b) l i), 
+     (List.fold_right (f (not b)) l k)
+
+
+(*s Registration of operations for rollback. *)
+
+let (inline_extraction,_) = 
+  declare_object ("Extraction Inline",
+		  { cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
+		    load_function = (fun (_,(b,l)) -> add_inline_entries b l);
+		    open_function = (fun _ -> ());
+		    export_function = (fun x -> Some x) })
+
+let _ = declare_summary "Extraction Inline"
+	  { freeze_function = (fun () -> !inline_table);
+	    unfreeze_function = ((:=) inline_table);
+	    init_function = (fun () -> inline_table := empty_inline_table);
+	    survive_section = true }
+
+(*s Grammar entries. *)
+
+let _ = 
+  vinterp_add "ExtractionInline"
+    (fun vl () -> 
+       let refs = List.map check_constant (refs_of_vargl vl) in 
+       add_anonymous_leaf (inline_extraction (true,refs)))
+
+let _ = 
+  vinterp_add "ExtractionNoInline"
+    (fun vl () -> 
+       let refs = List.map check_constant (refs_of_vargl vl) in 
+       add_anonymous_leaf (inline_extraction (false,refs)))
+
+
+(*s Table for direct ML extractions. *)
+
+let empty_extractions = (Refmap.empty, Refset.empty, [])
+
+let extractions = ref empty_extractions
+
+let ml_extractions () = let (_,set,_) =  !extractions in set 
+
+let sorted_ml_extractions () = let (_,_,l) = !extractions in l
+
+let add_ml_extraction r s = 
+  let (map,set,list) = !extractions in
+  extractions := (Refmap.add r s map, Refset.add r set, (r,s)::list)
+
+let is_ml_extraction r = 
+  let (_,set,_) = !extractions in Refset.mem r set
+
+let find_ml_extraction r = 
+  let (map,_,_) = !extractions in Refmap.find r map
+
+(*s Registration of operations for rollback. *)
+
+let (in_ml_extraction,_) = 
+  declare_object ("ML extractions",
+		  { cache_function = (fun (_,(r,s)) -> add_ml_extraction r s);
+		    load_function = (fun (_,(r,s)) -> add_ml_extraction r s);
+		    open_function = (fun _ -> ());
+		    export_function = (fun x -> Some x) })
+
+let _ = declare_summary "ML extractions"
+	  { freeze_function = (fun () -> !extractions);
+	    unfreeze_function = ((:=) extractions);
+	    init_function = (fun () -> extractions := empty_extractions);
+	    survive_section = true }
+
+
+(*s Grammar entries. *)
+
+let _ = 
+  vinterp_add "ExtractConstant"
+    (function 
+       | [id; vs] -> 
+	   (fun () -> 
+	      let r = check_constant (reference_of_varg id) in 
+	      let s = string_of_varg vs in 
+	      add_anonymous_leaf (in_ml_extraction (r,s)))
+       | _ -> assert false)
+
+let _ = 
+  vinterp_add "ExtractInlinedConstant"
+    (function 
+       | [id; vs] -> 
+	   (fun () -> 
+	      let r = check_constant (reference_of_varg id) in 
+	      let s = string_of_varg vs in 
+	      add_anonymous_leaf (inline_extraction (true,[r]));
+	      add_anonymous_leaf (in_ml_extraction (r,s)))
+       | _ -> assert false)
+
+
+let extract_inductive r (id2,l2) = match r with
+  | IndRef ((sp,i) as ip) ->
+      let mib = Global.lookup_mind sp in
+      let n = Array.length mib.mind_packets.(i).mind_consnames in
+      if n <> List.length l2 then
+	error "not the right number of constructors";
+      add_anonymous_leaf (in_ml_extraction (r,id2));
+      list_iter_i
+	(fun j s -> 
+	   add_anonymous_leaf 
+	     (in_ml_extraction (ConstructRef (ip,succ j),s))) l2
+  | _ -> 
+      errorlabstrm "extract_inductive"
+	[< Printer.pr_global r; 'sPC; 'sTR "is not an inductive type" >]
+
+let _ = 
+  vinterp_add "ExtarctInductive"
+    (function 
+       | [q1; VARG_VARGLIST (id2 :: l2)] ->
+	   (fun () -> 
+	      extract_inductive (reference_of_varg q1) 
+		(string_of_varg id2, List.map string_of_varg l2))
+       | _ -> assert false)
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
new file mode 100644
index 0000000000..7efbc0faaa
--- /dev/null
+++ b/contrib/extraction/table.mli
@@ -0,0 +1,49 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Summary
+open Goptions
+open Vernacinterp
+open Names
+
+(*s Set and Map over global reference *) 
+
+module Refset : Set.S with type elt = global_reference
+
+(*s Auxiliary functions *) 
+		      
+val check_constant : global_reference -> global_reference
+
+val refs_of_vargl : vernac_arg list -> global_reference list
+
+(*s AutoInline parameter *) 
+
+val auto_inline : unit -> bool
+
+(*s Optimize parameter *) 
+
+val optim :  unit -> bool
+
+(* Table for custom inlining *) 
+
+val to_inline : global_reference -> bool
+
+val to_keep : global_reference -> bool
+
+(*s Table for direct ML extractions. *)
+
+val is_ml_extraction : global_reference -> bool
+
+val find_ml_extraction : global_reference -> string
+
+val ml_extractions : unit -> Refset.t
+
+val sorted_ml_extractions : unit -> (global_reference * string) list
+
diff --git a/contrib/extraction/test/addReals b/contrib/extraction/test/addReals
index 86e9a79947..601592091a 100644
--- a/contrib/extraction/test/addReals
+++ b/contrib/extraction/test/addReals
@@ -22,4 +22,4 @@ let rec int_to_Z i =
 	else 
 	  Fast_integer.NEG (int_to_positive (-i))
 
-let my_ceil x = int_to_Z (int_of_float (ceil x))
+let my_ceil x = int_to_Z (succ (int_of_float (floor x)))