Fin de mise en place de l'option Optimize. Reorganisation du pretty-print. ETC etc etc

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

17 files changed, 519 insertions, 550 deletions

diff --git a/.depend b/.depend
index 38e8507dab..9bcaf7993d 100644
--- a/.depend
+++ b/.depend
@@ -256,17 +256,18 @@ contrib/correctness/putil.cmi: kernel/names.cmi contrib/correctness/past.cmi \
 contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \
     contrib/correctness/penv.cmi contrib/correctness/prename.cmi \
     kernel/term.cmi 
+contrib/extraction/common.cmi: contrib/extraction/miniml.cmi \
+    contrib/extraction/mlutil.cmi kernel/names.cmi 
 contrib/extraction/extraction.cmi: kernel/environ.cmi \
     contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi 
 contrib/extraction/haskell.cmi: contrib/extraction/miniml.cmi \
-    contrib/extraction/mlutil.cmi kernel/names.cmi 
+    kernel/names.cmi lib/pp.cmi 
 contrib/extraction/miniml.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi 
 contrib/extraction/mlutil.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
     kernel/term.cmi 
-contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi \
-    contrib/extraction/mlutil.cmi kernel/names.cmi lib/pp.cmi kernel/term.cmi 
-contrib/extraction/table.cmi: library/goptions.cmi kernel/names.cmi \
-    library/summary.cmi toplevel/vernacinterp.cmi 
+contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \
+    lib/pp.cmi kernel/term.cmi 
+contrib/extraction/table.cmi: kernel/names.cmi toplevel/vernacinterp.cmi 
 contrib/interface/dad.cmi: contrib/interface/ctast.cmo proofs/proof_type.cmi \
     proofs/tacmach.cmi 
 contrib/interface/debug_tac.cmi: parsing/coqast.cmi proofs/proof_type.cmi \
@@ -1646,21 +1647,31 @@ contrib/correctness/pwp.cmx: kernel/environ.cmx kernel/evd.cmx \
     contrib/correctness/ptype.cmi contrib/correctness/ptyping.cmx \
     contrib/correctness/putil.cmx kernel/reduction.cmx kernel/term.cmx \
     lib/util.cmx contrib/correctness/pwp.cmi 
-contrib/extraction/extract_env.cmo: parsing/astterm.cmi kernel/evd.cmi \
-    contrib/extraction/extraction.cmi library/global.cmi \
-    contrib/extraction/haskell.cmi library/lib.cmi library/libobject.cmi \
-    library/library.cmi contrib/extraction/miniml.cmi \
+contrib/extraction/common.cmo: kernel/environ.cmi library/global.cmi \
+    contrib/extraction/haskell.cmi contrib/extraction/miniml.cmi \
+    contrib/extraction/mlutil.cmi kernel/names.cmi \
+    contrib/extraction/ocaml.cmi lib/pp.cmi lib/pp_control.cmi \
+    parsing/printer.cmi contrib/extraction/table.cmi \
+    contrib/extraction/common.cmi 
+contrib/extraction/common.cmx: kernel/environ.cmx library/global.cmx \
+    contrib/extraction/haskell.cmx contrib/extraction/miniml.cmi \
+    contrib/extraction/mlutil.cmx kernel/names.cmx \
+    contrib/extraction/ocaml.cmx lib/pp.cmx lib/pp_control.cmx \
+    parsing/printer.cmx contrib/extraction/table.cmx \
+    contrib/extraction/common.cmi 
+contrib/extraction/extract_env.cmo: parsing/astterm.cmi \
+    contrib/extraction/common.cmi kernel/evd.cmi \
+    contrib/extraction/extraction.cmi library/global.cmi library/lib.cmi \
+    library/libobject.cmi library/library.cmi contrib/extraction/miniml.cmi \
     contrib/extraction/mlutil.cmi kernel/names.cmi library/nametab.cmi \
-    contrib/extraction/ocaml.cmi lib/pp.cmi parsing/printer.cmi \
-    contrib/extraction/table.cmi kernel/term.cmi lib/util.cmi \
+    lib/pp.cmi contrib/extraction/table.cmi kernel/term.cmi lib/util.cmi \
     toplevel/vernacinterp.cmi contrib/extraction/extract_env.cmi 
-contrib/extraction/extract_env.cmx: parsing/astterm.cmx kernel/evd.cmx \
-    contrib/extraction/extraction.cmx library/global.cmx \
-    contrib/extraction/haskell.cmx library/lib.cmx library/libobject.cmx \
-    library/library.cmx contrib/extraction/miniml.cmi \
+contrib/extraction/extract_env.cmx: parsing/astterm.cmx \
+    contrib/extraction/common.cmx kernel/evd.cmx \
+    contrib/extraction/extraction.cmx library/global.cmx library/lib.cmx \
+    library/libobject.cmx library/library.cmx contrib/extraction/miniml.cmi \
     contrib/extraction/mlutil.cmx kernel/names.cmx library/nametab.cmx \
-    contrib/extraction/ocaml.cmx lib/pp.cmx parsing/printer.cmx \
-    contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
+    lib/pp.cmx contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
     toplevel/vernacinterp.cmx contrib/extraction/extract_env.cmi 
 contrib/extraction/extraction.cmo: kernel/closure.cmi kernel/declarations.cmi \
     kernel/environ.cmi kernel/evd.cmi library/global.cmi lib/gmap.cmi \
@@ -1676,32 +1687,28 @@ contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \
     kernel/reduction.cmx pretyping/retyping.cmx library/summary.cmx \
     contrib/extraction/table.cmx kernel/term.cmx lib/util.cmx \
     contrib/extraction/extraction.cmi 
-contrib/extraction/haskell.cmo: kernel/environ.cmi library/global.cmi \
-    contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
-    kernel/names.cmi contrib/extraction/ocaml.cmi lib/options.cmi lib/pp.cmi \
-    lib/pp_control.cmi kernel/term.cmi lib/util.cmi \
-    contrib/extraction/haskell.cmi 
-contrib/extraction/haskell.cmx: kernel/environ.cmx library/global.cmx \
-    contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
-    kernel/names.cmx contrib/extraction/ocaml.cmx lib/options.cmx lib/pp.cmx \
-    lib/pp_control.cmx kernel/term.cmx lib/util.cmx \
-    contrib/extraction/haskell.cmi 
+contrib/extraction/haskell.cmo: contrib/extraction/miniml.cmi \
+    contrib/extraction/mlutil.cmi kernel/names.cmi \
+    contrib/extraction/ocaml.cmi lib/options.cmi lib/pp.cmi kernel/term.cmi \
+    lib/util.cmi contrib/extraction/haskell.cmi 
+contrib/extraction/haskell.cmx: contrib/extraction/miniml.cmi \
+    contrib/extraction/mlutil.cmx kernel/names.cmx \
+    contrib/extraction/ocaml.cmx lib/options.cmx lib/pp.cmx kernel/term.cmx \
+    lib/util.cmx contrib/extraction/haskell.cmi 
 contrib/extraction/mlutil.cmo: kernel/declarations.cmi \
-    contrib/extraction/miniml.cmi kernel/names.cmi lib/pp.cmi \
+    contrib/extraction/miniml.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
     parsing/printer.cmi contrib/extraction/table.cmi kernel/term.cmi \
     lib/util.cmi contrib/extraction/mlutil.cmi 
 contrib/extraction/mlutil.cmx: kernel/declarations.cmx \
-    contrib/extraction/miniml.cmi kernel/names.cmx lib/pp.cmx \
+    contrib/extraction/miniml.cmi kernel/names.cmx lib/options.cmx lib/pp.cmx \
     parsing/printer.cmx contrib/extraction/table.cmx kernel/term.cmx \
     lib/util.cmx contrib/extraction/mlutil.cmi 
-contrib/extraction/ocaml.cmo: kernel/environ.cmi library/global.cmi \
-    contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \
-    kernel/names.cmi lib/options.cmi lib/pp.cmi lib/pp_control.cmi \
+contrib/extraction/ocaml.cmo: contrib/extraction/miniml.cmi \
+    contrib/extraction/mlutil.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
     parsing/printer.cmi contrib/extraction/table.cmi kernel/term.cmi \
     lib/util.cmi contrib/extraction/ocaml.cmi 
-contrib/extraction/ocaml.cmx: kernel/environ.cmx library/global.cmx \
-    contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \
-    kernel/names.cmx lib/options.cmx lib/pp.cmx lib/pp_control.cmx \
+contrib/extraction/ocaml.cmx: contrib/extraction/miniml.cmi \
+    contrib/extraction/mlutil.cmx kernel/names.cmx lib/options.cmx lib/pp.cmx \
     parsing/printer.cmx contrib/extraction/table.cmx kernel/term.cmx \
     lib/util.cmx contrib/extraction/ocaml.cmi 
 contrib/extraction/table.cmo: kernel/declarations.cmi library/global.cmi \
diff --git a/Makefile b/Makefile
index d6f3a60373..7b8e5ad99f 100644
--- a/Makefile
+++ b/Makefile
@@ -201,6 +201,7 @@ EXTRACTIONCMO=contrib/extraction/table.cmo\
 	      contrib/extraction/mlutil.cmo\
 	      contrib/extraction/ocaml.cmo \
 	      contrib/extraction/haskell.cmo \
+              contrib/extraction/common.cmo \
 	      contrib/extraction/extraction.cmo \
 	      contrib/extraction/extract_env.cmo
 
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 51574bda0d..b8c7eeb9a0 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -39,6 +39,15 @@ Grammar vernac vernac : ast :=
      [ "Extraction" "NoInline" ne_qualidarg_list($l) "." ] 
   -> [ (ExtractionNoInline ($LIST $l)) ]
 
+| print_inline_constant 
+     [ "Print" "Extraction" "Inline" "."]
+  -> [ (PrintExtractionInline) ]
+
+| reset_inline_constant 
+     [ "Reset" "Extraction" "Inline" "."]
+  -> [ (ResetExtractionInline) ]
+
+
 (* Overriding of a Coq object by an ML one *)
 | extract_constant 
      [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ]
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
new file mode 100644
index 0000000000..35dfd4d042
--- /dev/null
+++ b/contrib/extraction/common.ml
@@ -0,0 +1,198 @@
+(***********************************************************************)
+(*  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 Pp
+open Names
+open Miniml
+open Table
+open Mlutil
+open Ocaml
+open Nametab
+
+
+(*s Modules considerations *)
+
+let current_module = ref None
+
+let module_of_r r = 
+  string_of_id (snd (split_dirpath (dirpath (sp_of_r r))))
+
+let module_option r = 
+  let m = module_of_r r in
+  if Some m = !current_module then ""
+  else (String.capitalize m) ^ "."
+
+let check_ml r d = 
+  if to_inline r then 
+    try 
+      find_ml_extraction r 
+    with Not_found -> d
+  else d
+
+
+(*s tables of global renamings *)
+
+let keywords = ref Idset.empty
+let global_ids = ref Idset.empty
+
+let renamings = Hashtbl.create 97
+
+let cache r f =  
+  try Hashtbl.find renamings r 
+  with Not_found -> let id = f r in Hashtbl.add renamings r id; id 
+    
+(*s Renaming issues at toplevel *)
+
+module ToplevelParams = struct
+  let globals () = Idset.empty
+  let rename_global r = Names.id_of_string (Global.string_of_global r)
+  let pp_type_global = Printer.pr_global
+  let pp_global = Printer.pr_global
+  let cofix_warning = false
+end
+
+(*s Renaming issues for a monolithic extraction. *)
+
+module MonoParams = struct
+  
+  let globals () = ! global_ids
+		     
+  let cache r f = f r
+		    
+  let rename_global_id id = 
+    let id' = rename_id id !global_ids in
+    global_ids := Idset.add id' !global_ids; 
+    id'
+
+  let rename_type_global r =  
+    cache r
+      (fun r -> 
+	 let id = Environ.id_of_global (Global.env()) r in
+	 rename_global_id (lowercase_id id))
+      
+  let rename_global r = 
+    cache r
+      (fun r -> 
+	 let id = Environ.id_of_global (Global.env()) r in
+	 match r with
+	   | ConstructRef _ -> rename_global_id (uppercase_id id)
+	   | _ -> rename_global_id (lowercase_id id))
+      
+  let pp_type_global r = 
+    string (check_ml r (string_of_id (rename_type_global r)))
+      
+  let pp_global r = 
+    string (check_ml r (string_of_id (rename_global r)))
+      
+  let cofix_warning = true
+
+end
+
+
+(*s Renaming issues in a modular extraction. *)
+
+module ModularParams = struct
+
+  let globals () = !global_ids 
+
+  let clash r id = 
+    try 
+      let _ = locate (make_qualid (dirpath (sp_of_r r)) id)
+      in true
+    with _ -> false
+
+  let rename_global_id r id id' prefix =
+    let id' = 
+      if (Idset.mem id' !keywords) || (id <> id' && clash r id') then 
+	id_of_string (prefix^(string_of_id id))
+      else id'
+    in global_ids := Idset.add id' !global_ids; id'
+
+  let rename_type_global r = 
+    cache r 
+      (fun r ->     
+	 let id = Environ.id_of_global (Global.env()) r in 
+	 rename_global_id r id (lowercase_id id) "coq_")
+
+  let rename_global r =
+    cache r 
+      (fun r -> 
+	 let id = Environ.id_of_global (Global.env()) r in 
+	 match r with
+	   | ConstructRef _ -> rename_global_id r id (uppercase_id id) "Coq_"
+	   | _ -> rename_global_id r id (lowercase_id id) "coq_")
+
+  let pp_type_global r = 
+    string 
+      (check_ml r ((module_option r)^(string_of_id (rename_type_global r))))
+
+  let pp_global r = 
+    string 
+      (check_ml r ((module_option r)^(string_of_id (rename_global r))))
+
+  let cofix_warning = true
+end
+
+
+module ToplevelPp = Ocaml.Make(ToplevelParams)
+
+module OcamlMonoPp = Ocaml.Make(MonoParams)
+module OcamlModularPp = Ocaml.Make(ModularParams)
+
+module HaskellMonoPp = Haskell.Make(MonoParams)
+module HaskellModularPp = Haskell.Make(ModularParams)
+
+
+
+(*s Extraction to a file. *)
+
+let init_global_ids lang = 
+  keywords := 
+  Idset.add (id_of_string "prop") 
+    (Idset.add (id_of_string "arity") 
+       (match lang with 
+	  | "ocaml" -> Ocaml.keywords
+	  | "haskell" -> Haskell.keywords
+	  | _ -> assert false));
+  global_ids := !keywords
+
+let extract_to_file f prm decls =
+  Hashtbl.clear renamings;
+  init_global_ids prm.lang; 
+  current_module := 
+    if prm.modular then 
+      Some prm.module_name 
+    else None;
+  let preamble = match prm.lang with 
+    | "ocaml" -> Ocaml.preamble
+    | "haskell" -> Haskell.preamble
+    | _ -> assert false
+  in
+  let pp_decl = match prm.lang,prm.modular with 
+    | "ocaml", true -> OcamlModularPp.pp_decl
+    | "ocaml", false -> OcamlMonoPp.pp_decl
+    | "haskell",true -> HaskellModularPp.pp_decl
+    | "haskell",false -> HaskellMonoPp.pp_decl 
+    | _ -> assert false
+  in
+  let cout = open_out f in
+  let ft = Pp_control.with_output_to cout in
+  pP_with ft (hV 0 (preamble prm));
+  begin 
+    try
+      List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
+    with e ->
+      pp_flush_with ft (); close_out cout; raise e
+  end;
+  pp_flush_with ft ();
+  close_out cout
+
+
+
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
new file mode 100644
index 0000000000..00136ef93e
--- /dev/null
+++ b/contrib/extraction/common.mli
@@ -0,0 +1,19 @@
+(***********************************************************************)
+(*  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 Miniml
+open Mlutil
+open Names
+
+module ToplevelPp : Mlpp
+
+val extract_to_file : 
+  string -> extraction_params -> ml_decl list -> unit
+
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 64373877d3..7e8a0c0734 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -18,6 +18,7 @@ open Miniml
 open Table
 open Mlutil
 open Vernacinterp
+open Common
 
 (*s Recursive computation of the global references to extract. 
     We use a set of functions visiting the extracted objects in
@@ -104,15 +105,6 @@ let extract_env rl =
     vernacular command is \verb!Extraction! [term]. Whenever [term] is
     a global, its definition is displayed. *)
 
-module ToplevelParams = struct
-  let rename_global r = Names.id_of_string (Global.string_of_global r)
-  let pp_type_global = Printer.pr_global
-  let pp_global = Printer.pr_global
-  let cofix_warning = false
-end
-
-module Pp = Ocaml.Make(ToplevelParams)
-
 let refs_set_of_list l = List.fold_right Refset.add l Refset.empty 
 
 let decl_of_refs refs =
@@ -120,7 +112,7 @@ let decl_of_refs refs =
 
 let local_optimize refs = 
   let prm = 
-    { strict = true ; modular = false ; 
+    { lang = "ocaml" ; modular = false ; 
       module_name = "" ; to_appear = refs} in
   optimize prm (decl_of_refs refs)
 
@@ -131,7 +123,7 @@ let extract_reference r =
   if is_ml_extraction r then
     print_user_extract r 
   else
-    mSGNL (Pp.pp_decl (list_last (local_optimize [r])))
+    mSGNL (ToplevelPp.pp_decl (list_last (local_optimize [r])))
 
 let _ = 
   vinterp_add "Extraction"
@@ -147,8 +139,8 @@ let _ =
 		(* Otherwise, output the ML type or expression *)
 		| _ ->
 		    match extract_constr (Global.env()) [] c with
-		      | Emltype (t,_,_) -> mSGNL (Pp.pp_type t)
-		      | Emlterm a -> mSGNL (Pp.pp_ast (normalize a)))
+		      | Emltype (t,_,_) -> mSGNL (ToplevelPp.pp_type t)
+		      | Emlterm a -> mSGNL (ToplevelPp.pp_ast (normalize a)))
        | _ -> assert false)
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
@@ -163,38 +155,26 @@ let _ =
        let rl = List.filter (fun x -> not (is_ml_extraction x)) rl in 
        let dl = decl_of_refs rl in
        List.iter print_user_extract ml_rl ;
-       List.iter (fun d -> mSGNL (Pp.pp_decl d)) dl)
-
-(*s Extraction parameters. *)
-
-let strict_language = function
-  | "ocaml" -> true
-  | "haskell" -> false
-  | _ -> assert false
+       List.iter (fun d -> mSGNL (ToplevelPp.pp_decl d)) dl)
 
 (*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. *)
 
-let extract_to_file = function
-  | "ocaml" -> Ocaml.extract_to_file 
-  | "haskell" -> Haskell.extract_to_file
-  | _ -> assert false
-
 let _ = 
   vinterp_add "ExtractionFile"
     (function 
        | VARG_STRING lang :: VARG_STRING f :: vl ->
 	   (fun () -> 
 	      let refs = refs_of_vargl vl in
-	      let prm = {strict=strict_language lang;
+	      let prm = {lang=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
-	      extract_to_file lang f prm decls)
+	      extract_to_file f prm decls)
        | _ -> assert false)
 
 (*s Extraction of a module. The vernacular command is \verb!Extraction Module!
@@ -232,16 +212,15 @@ let _ =
     (function 
        | [VARG_STRING lang; VARG_IDENTIFIER m] ->
 	   (fun () -> 
-	      Ocaml.current_module := Some m;
 	      let ms = Names.string_of_id m in
 	      let f = (String.uncapitalize ms) ^ (file_suffix lang) in
-	      let prm = {strict=strict_language lang;
+	      let prm = {lang=lang;
 			 modular=true;
-			 module_name= Names.string_of_id m;
+			 module_name= ms;
 			 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 f prm decls)
        | _ -> assert false)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 9549829862..3282880a71 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -19,17 +19,9 @@ open Mlutil
 open Options
 open Ocaml
 
-let rec collapse_type_app = function
-  | (Tapp l1) :: l2 -> collapse_type_app (l1 @ l2)
-  | l -> l
-
-let space_if = function true -> [< 'sTR " " >] | false -> [< >]
-
-let sec_space_if = function true -> [< 'sPC >] | false -> [< >]
-
 (*s Haskell renaming issues. *)
 
-let haskell_keywords =     
+let keywords =     
   List.fold_right (fun s -> Idset.add (id_of_string s))
   [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; 
@@ -37,67 +29,13 @@ let haskell_keywords =
     "as"; "qualified"; "hiding" ]
   Idset.empty
 
-let current_ids = ref haskell_keywords
-
-let rec rename_id id avoid = 
-  if Idset.mem id avoid then rename_id (lift_ident id) avoid else id
-
-let rename_global id = 
-  let id' = rename_id id !current_ids in
-  current_ids := Idset.add id' !current_ids; 
-  id'
-
-let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
-let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
-
-let rename_lower_global id = rename_global (lowercase_id id)
-let rename_upper_global id = rename_global (uppercase_id id)
-
-let pr_lower_id id = pr_id (lowercase_id id)
-
-(*s de Bruijn environments for programs *)
-
-type env = identifier list * Idset.t
-
-let rec rename_vars avoid = function
-  | [] -> 
-      [], avoid
-  | id :: idl when id == prop_name ->
-      (* we don't rename propositions binders *)
-      let (idl', avoid') = rename_vars avoid idl in
-      (id :: idl', avoid')
-  | id :: idl ->
-      let id' = rename_id (lowercase_id id) avoid in
-      let (idl', avoid') = rename_vars (Idset.add id' avoid) idl in
-      (id' :: idl', avoid')
-
-let push_vars ids (db,avoid) =
-  let ids',avoid' = rename_vars avoid ids in
-  ids', (ids' @ db, avoid')
-
-let empty_env () = ([], !current_ids)
-
-let get_db_name n (db,_) = List.nth db (pred n)
-
-(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
-    the list [id1;...;idn] and the term [t]. *)
-
-let collect_lambda = 
-  let rec collect acc = function
-    | MLlam(id,t) -> collect (id::acc) t
-    | x           -> acc,x
-  in 
-  collect []
-
-let abst = function
-  | [] -> [< >]
-  | l  -> [< 'sTR "\\ ";
-             prlist_with_sep (fun  ()-> [< 'sTR " " >]) pr_id l;
-             'sTR " ->"; 'sPC >]
-
-let pr_binding = function
-  | [] -> [< >]
-  | l  -> [< 'sTR " "; prlist_with_sep (fun () -> [< 'sTR " " >]) pr_id l >]
+let preamble prm =
+  let m = if prm.modular then String.capitalize prm.module_name else "Main" in
+  [< 'sTR "module "; 'sTR m; 'sTR " where"; 'fNL; 'fNL;
+     'sTR "type Prop = ()"; 'fNL;
+     'sTR "prop = ()"; 'fNL; 'fNL;
+     'sTR "type Arity = ()"; 'fNL;
+     'sTR "arity = ()"; 'fNL; 'fNL >]
 
 (*s The pretty-printing functor. *)
 
@@ -105,14 +43,18 @@ module Make = functor(P : Mlpp_param) -> struct
 
 let pp_type_global = P.pp_type_global
 let pp_global = P.pp_global
+let rename_global = P.rename_global
+
+let pr_lower_id id = pr_id (lowercase_id id)
+
+let empty_env () = [], P.globals()
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
 let rec pp_type par t =
   let rec pp_rec par = function
-    | Tvar id -> 
-	pr_id (lowercase_id id) (* TODO: possible clash with Haskell kw *)
+    | Tvar id -> pr_lower_id id (* TODO: possible clash with Haskell kw *)
     | Tapp l ->
 	(match collapse_type_app l with
 	   | [] -> assert false
@@ -160,7 +102,7 @@ let rec pp_expr par env args =
     | MLlam _ as a -> 
       	let fl,a' = collect_lambda a in
 	let fl,env' = push_vars fl env in
-	let st = [< abst (List.rev fl); pp_expr false env' [] a' >] in
+	let st = [< pp_abst (List.rev fl); pp_expr false env' [] a' >] in
 	if args = [] then
           [< open_par par; st; close_par par >]
         else
@@ -301,7 +243,7 @@ let pp_decl = function
 	   (fun (fi,ti) -> pp_function env' (pr_id fi) ti)
 	   (List.combine (List.rev ids') (Array.to_list defs));
 	 'fNL;
-	 let id = P.rename_global r in
+	 let id = rename_global r in
 	 let idi = List.nth (List.rev ids') i in
 	 if id <> idi then
 	   [< 'fNL; pr_id id; 'sTR " = "; pr_id idi; 'fNL >]
@@ -310,112 +252,10 @@ 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 " ="; 
+      hOV 0  [< pp_global r; 'sTR " ="; 
 		'sPC; 'sTR s; 'fNL  >]
 
 let pp_type = pp_type false
 
 end
 
-(*s Renaming issues for a monolithic extraction. *)
-
-module MonoParams = struct
-
-let renamings = Hashtbl.create 97
-
-let cache r f = 
-  try Hashtbl.find renamings r 
-  with Not_found -> let id = f r in Hashtbl.add renamings r id; id
-
-let rename_type_global r =  
-  cache r
-    (fun r -> 
-       let id = Environ.id_of_global (Global.env()) r in
-       rename_upper_global id)
-
-let rename_global r = 
-  cache r
-    (fun r -> 
-       let id = Environ.id_of_global (Global.env()) r in
-       match r with
-	 | ConstructRef _ -> rename_upper_global id
-	 | _ -> rename_lower_global id)
-
-let pp_type_global r = 
-  string (check_ml r (string_of_id (rename_type_global r)))
-
-let pp_global r = 
-  string (check_ml r (string_of_id (rename_global r)))
-
-let cofix_warning = true
-
-end
-
-module MonoPp = Make(MonoParams)
-
-(*s Renaming issues in a modular extraction. *)
-
-module ModularParams = struct
-
-  let avoid = 
-    Idset.add (id_of_string "prop")
-      (Idset.add (id_of_string "arity") haskell_keywords)
-
-  let rename_lower id = 
-    if Idset.mem id avoid || id <> lowercase_id id then 
-      "coq_" ^ string_of_id id 
-    else 
-      string_of_id id
-
-  let rename_upper id = 
-    if Idset.mem id avoid || id <> uppercase_id id then 
-      "Coq_" ^ string_of_id id 
-    else 
-      string_of_id id
-
- let rename_type_global r = 
-    let id = Environ.id_of_global (Global.env()) r in 
-    rename_lower id
-
-  let rename_global_aux r = 
-    let id = Environ.id_of_global (Global.env()) r in 
-    match r with
-      | ConstructRef _ -> rename_upper id
-      | _ -> rename_lower id
-
-  let rename_global r = id_of_string (rename_global_aux r)
-
-  let pp_type_global r = 
-    string ((module_option r)^(check_ml r (rename_type_global r)))
-
-  let pp_global r = 
-    string ((module_option r)^(check_ml r (rename_global_aux r)))
-
-  let cofix_warning = true
-end
-
-module ModularPp = Make(ModularParams)
-
-(*s Extraction to a file. *)
-
-let haskell_preamble prm =
-  let m = if prm.modular then String.capitalize prm.module_name else "Main" in
-  [< 'sTR "module "; 'sTR m; 'sTR " where"; 'fNL; 'fNL;
-     'sTR "type Prop = ()"; 'fNL;
-     'sTR "prop = ()"; 'fNL; 'fNL;
-     'sTR "type Arity = ()"; 'fNL;
-     'sTR "arity = ()"; 'fNL; 'fNL >]
-
-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));
-  begin 
-    try
-      List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
-    with e ->
-      pp_flush_with ft (); close_out cout; raise e
-  end;
-  pp_flush_with ft ();
-  close_out cout
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index fa10cb1bd9..e1a7f0cd05 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -8,11 +8,12 @@
 
 (*i $Id$ i*)
 
-(*s Production of Haskell syntax. *)
-
-open Miniml
-open Mlutil
+open Pp
 open Names
+open Miniml
+
+val keywords : Idset.t
+
+val preamble : extraction_params -> std_ppcmds
 
-val extract_to_file : 
-  string -> extraction_params -> ml_decl list -> unit
+module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index d8a9597e18..1cbfe3a55f 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -59,8 +59,15 @@ type ml_decl =
     The resulting pretty-printer is a module of type [Mlpp] providing
     functions to print types, terms and declarations. *)
 
+type extraction_params =  
+  { lang : string; 
+    modular : bool; 
+    module_name : string; 
+    to_appear : global_reference list }
+
 module type Mlpp_param = sig
   val cofix_warning : bool
+  val globals : unit -> Idset.t
   val rename_global : global_reference -> identifier
   val pp_type_global : global_reference -> std_ppcmds
   val pp_global : global_reference -> std_ppcmds
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 3e4a0f0659..bb139597b6 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -197,7 +197,7 @@ let nb_occur a =
   count 1 a; !cpt
 
 
-(*s Beta-iota reductions + simplifications*)
+(*s Some Beta-iota reductions + simplifications*)
 
 let constructor_index = function
   | ConstructRef (_,j) -> pred j
@@ -251,72 +251,74 @@ let all_constr br =
   with Impossible -> false
   
 
-let rec betaiota = function
-  | MLapp (f, []) ->
-      betaiota f
-  | MLapp (f, a) ->
-      let f' = betaiota f 
-      and a' = List.map betaiota a in
-      (match f' with
-	 (* beta redex *)
-	 | MLlam (id,t) -> 
-	     (match nb_occur t with
-		| 0 -> betaiota (MLapp (ml_pop t, List.tl a'))
-		| 1 -> betaiota (MLapp (ml_subst (List.hd a') t, List.tl a'))
-		| _ -> 
-		    let a'' = List.map (ml_lift 1) (List.tl a') in
-		    betaiota (MLletin (id, List.hd a', MLapp (t, a''))))
-	 (* application of a let in: we push arguments inside *)
-	 | MLletin (id,e1,e2) ->
-	     MLletin (id, e1, betaiota (MLapp (e2, List.map (ml_lift 1) a')))
-	 (* application of a case: we push arguments inside *)
-	 | MLcase (e,br) ->
-	     let br' = 
-	       Array.map 
+let normalize a = 
+  let o = optim() in 
+  let rec simplify = function
+    | MLapp (f, []) ->
+	simplify f
+    | MLapp (f, a) ->
+	let f' = simplify f 
+	and a' = List.map simplify a in
+	(match f' with
+	     (* beta redex *)
+	   | MLlam (id,t) -> 
+	       (match nb_occur t with
+		  | 0 -> simplify (MLapp (ml_pop t, List.tl a'))
+		  | 1 when o -> 
+		      simplify (MLapp (ml_subst (List.hd a') t, List.tl a'))
+		  | _ -> 
+		      let a'' = List.map (ml_lift 1) (List.tl a') in
+		      simplify (MLletin (id, List.hd a', MLapp (t, a''))))
+	       (* application of a let in: we push arguments inside *)
+	   | MLletin (id,e1,e2) ->
+	       MLletin (id, e1, simplify (MLapp (e2, List.map (ml_lift 1) a')))
+		 (* application of a case: we push arguments inside *)
+	   | MLcase (e,br) ->
+	       let br' = 
+		 Array.map 
       	       	 (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'')))) 
-		 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 (_,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 = List.fold_right 
-				   (fun id t -> MLlam (id,t)) ids c in
-			let c = ml_lift (List.length i) 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 
+      	       	    (n, l, simplify (MLapp (t,a'')))) 
+		   br 
+	       in simplify (MLcase (e,br'))
+	   | _ ->
+	       MLapp (f',a'))
+    | MLcase (e,[||]) ->
+	MLexn "Empty inductive"
+    | MLcase (e,br) ->
+	(match simplify e with
+	     (* 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
+	       simplify (MLapp (c,a))
+	   | MLcase(e',br') when o && (all_constr br') ->
+	       let new_br= 
+		 Array.map 
+		   (function 
+		      | (n, i, 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
+			  let c = ml_lift (List.length i) c in 
+			  (n,i,simplify (MLapp (c,a)))
+		      | _ -> assert false) br'
+	       in MLcase(e', new_br)
+	   | e' -> 
+	       let br' = Array.map (fun (n,l,t) -> (n,l,simplify t)) br in 
+	       if o then
 		 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)
-  | a -> 
-      ast_map betaiota a
-    
-let normalize a = betaiota (merge_app a)
-
-let optional_normalize a = a (* TODO *)
+		   with Impossible -> MLcase (e', br')
+	       else MLcase (e', br'))
+    | MLletin(_,c,e) when (is_atomic c) || (nb_occur e <= 1) -> 
+	(* expansion of a letin in special cases *)
+	simplify (ml_subst c e)
+    | a -> 
+	ast_map simplify a 
+  in simplify (merge_app a)
 
 let normalize_decl = function
  | Dglob (id, a) -> Dglob (id, normalize a)
@@ -475,12 +477,6 @@ let warning_expansion 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
 
@@ -490,6 +486,11 @@ let add_ml_decls prm decls =
   let l = List.map (fun (r,s)-> Dcustom (r,s)) l in 
   (List.rev l @ decls)
 
+let strict_language = function
+  | "ocaml" -> true
+  | "haskell" -> false
+  | _ -> assert false
+
 let rec optimize prm = function
   | [] -> 
       []
@@ -501,8 +502,7 @@ let rec optimize prm = function
       else optimize prm l
   | Dglob (r,t) :: l ->
       let t = normalize t in
-      let t = if optim() then optional_normalize t else t in 
-      let b = expand prm.strict r t in
+      let b = expand (strict_language prm.lang) r t in
       let l = if b then 
 	begin
 	  if_verbose warning_expansion r;
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index 27608c46fe..bc5a137640 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -52,12 +52,6 @@ val normalize_decl : ml_decl -> ml_decl
 
 (*s Optimization. *)
 
-type extraction_params =  
-  { strict : bool; 
-    modular : bool; 
-    module_name : string; 
-    to_appear : global_reference list }
-
 val add_ml_decls : 
   extraction_params -> ml_decl list -> ml_decl list
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 855db902e8..862821be77 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -23,16 +23,16 @@ let current_module = ref None
 
 (*s Some utility functions. *)
 
+let rec collapse_type_app = function
+  | (Tapp l1) :: l2 -> collapse_type_app (l1 @ l2)
+  | l -> l
+
 let string s = [< 'sTR s >]
 
 let open_par = function true -> string "(" | false -> [< >]
 
 let close_par = function true -> string ")" | false -> [< >]
 
-let rec collapse_type_app = function
-  | (Tapp l1) :: l2 -> collapse_type_app (l1 @ l2)
-  | l -> l
-
 let pp_tuple f = function
   | [] -> [< >]
   | [x] -> f x
@@ -47,58 +47,28 @@ let pp_boxed_tuple f = function
       	    hOV 0 [< prlist_with_sep (fun () -> [< 'sTR ","; 'sPC >]) f l;
 		     'sTR ")" >] >]
 
-let space_if = function true -> [< 'sTR " " >] | false -> [< >]
+let pp_abst = function
+  | [] -> [< >]
+  | l  -> [< 'sTR "fun ";
+             prlist_with_sep (fun () -> [< 'sTR " " >]) pr_id l;
+             'sTR " ->"; 'sPC >]
 
-let sec_space_if = function true -> [< 'sPC >] | false -> [< >]
+let pr_binding = function
+  | [] -> [< >]
+  | l  -> [< 'sTR " "; prlist_with_sep (fun () -> [< 'sTR " " >]) pr_id l >]
 
-(*s Ocaml renaming issues. *)
+let space_if = function true -> [< 'sTR " " >] | false -> [< >]
 
-let ocaml_keywords =     
-  List.fold_right (fun s -> Idset.add (id_of_string s))
-  [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
-    "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
-    "for"; "fun"; "function"; "functor"; "if"; "in"; "include";
-    "inherit"; "initializer"; "lazy"; "let"; "match"; "method";
-    "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
-    "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
-    "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
-    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ] 
-  Idset.empty
+let sec_space_if = function true -> [< 'sPC >] | false -> [< >]
 
-let current_ids = ref ocaml_keywords
+(*s Generic renaming issues. *)
 
 let rec rename_id id avoid = 
   if Idset.mem id avoid then rename_id (lift_ident id) avoid else id
 
-let rename_global id = 
-  let id' = rename_id id !current_ids in
-  current_ids := Idset.add id' !current_ids; 
-  id'
-
 let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
 let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
 
-let rename_lower_global id = rename_global (lowercase_id id)
-let rename_upper_global id = rename_global (uppercase_id id)
-
-(*s Modules considerations *)
-
-let module_of_r r = snd (split_dirpath (dirpath (sp_of_r r)))
-
-let string_of_r r = string_of_id (basename (sp_of_r r))
-
-let module_option r = 
-  let m = module_of_r r in
-  if Some m = !current_module then ""
-  else (String.capitalize (string_of_id m)) ^ "."
-
-let check_ml r d = 
-  if to_inline r then 
-    try 
-      find_ml_extraction r 
-    with Not_found -> d
-  else d
-
 (*s de Bruijn environments for programs *)
 
 type env = identifier list * Idset.t
@@ -119,8 +89,6 @@ let push_vars ids (db,avoid) =
   let ids',avoid' = rename_vars avoid ids in
   ids', (ids' @ db, avoid')
 
-let empty_env () = ([], !current_ids)
-
 let get_db_name n (db,_) = List.nth db (pred n)
 
 (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
@@ -133,22 +101,35 @@ let collect_lambda =
   in 
   collect []
 
-let abst = function
-  | [] -> [< >]
-  | l  -> [< 'sTR "fun ";
-             prlist_with_sep (fun () -> [< 'sTR " " >]) pr_id l;
-             'sTR " ->"; 'sPC >]
+(*s Ocaml renaming issues. *)
 
-let pr_binding = function
-  | [] -> [< >]
-  | l  -> [< 'sTR " "; prlist_with_sep (fun () -> [< 'sTR " " >]) pr_id l >]
+let keywords =     
+  List.fold_right (fun s -> Idset.add (id_of_string s))
+  [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
+    "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
+    "for"; "fun"; "function"; "functor"; "if"; "in"; "include";
+    "inherit"; "initializer"; "lazy"; "let"; "match"; "method";
+    "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
+    "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
+    "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
+    "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ] 
+  Idset.empty
+
+let preamble _ =
+  [< 'sTR "type prop = unit"; 'fNL;
+     'sTR "let prop = ()"; 'fNL; 'fNL;
+     'sTR "type arity = unit"; 'fNL;
+     'sTR "let arity = ()"; 'fNL; 'fNL >]
 
 (*s The pretty-printing functor. *)
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_type_global = P.pp_type_global
+let pp_type_global = P.pp_type_global 
 let pp_global = P.pp_global
+let rename_global = P.rename_global
+
+let empty_env () = [], P.globals()
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
@@ -202,7 +183,7 @@ let rec pp_expr par env args =
     | MLlam _ as a -> 
       	let fl,a' = collect_lambda a in
 	let fl,env' = push_vars fl env in
-	let st = [< abst (List.rev fl); pp_expr false env' [] a' >] in
+	let st = [< pp_abst (List.rev fl); pp_expr false env' [] a' >] in
 	if args = [] then
           [< open_par par; st; close_par par >]
         else
@@ -362,119 +343,17 @@ let pp_decl = function
 	       pp_type_global r; 'sPC; 'sTR "="; 'sPC; 
 	       pp_type false  t; 'fNL >]
   | Dglob (r, MLfix (_,[|_|],[|def|])) ->
-      let id = P.rename_global r in
-      let env' = ([id], !current_ids) in
+      let id = rename_global r in
+      let env' = [id], P.globals() in
       [<  hOV 2 (pp_fix false env' None ([|id|],[|def|]) []) >]
   | 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); 
+      hOV 0 [< 'sTR "let "; pp_global r; 
 	       'sTR " ="; 'sPC; 'sTR s; 'fNL >]
 
 let pp_type = pp_type false
 
 end
 
-(*s Renaming issues for a monolithic extraction. *)
-
-module MonoParams = struct
-
-let renamings = Hashtbl.create 97
-
-let cache r f = 
-  try Hashtbl.find renamings r 
-  with Not_found -> let id = f r in Hashtbl.add renamings r id; id
-
-let rename_type_global r =  
-  cache r
-    (fun r -> 
-       let id = Environ.id_of_global (Global.env()) r in
-       rename_lower_global id)
-
-let rename_global r = 
-  cache r
-    (fun r -> 
-       let id = Environ.id_of_global (Global.env()) r in
-       match r with
-	 | ConstructRef _ -> rename_upper_global id
-	 | _ -> rename_lower_global id)
-
-let pp_type_global r = 
-  string (check_ml r (string_of_id (rename_type_global r)))
-
-let pp_global r = 
-  string (check_ml r (string_of_id (rename_global r)))
-
-let cofix_warning = true
-
-end
-
-module MonoPp = Make(MonoParams)
-
-(*s Renaming issues in a modular extraction. *)
-
-
-
-module ModularParams = struct
-
-  let avoid = 
-    Idset.add (id_of_string "prop")
-      (Idset.add (id_of_string "arity") ocaml_keywords)
-
-  let rename_lower id = 
-    if Idset.mem id avoid || id <> lowercase_id id then 
-      "coq_" ^ string_of_id id 
-    else 
-      string_of_id id
-
-  let rename_upper id = 
-    if Idset.mem id avoid || id <> uppercase_id id then 
-      "Coq_" ^ string_of_id id 
-    else 
-      string_of_id id
-
-  let rename_type_global r = 
-    let id = Environ.id_of_global (Global.env()) r in 
-    rename_lower id
-
-  let rename_global_aux r = 
-    let id = Environ.id_of_global (Global.env()) r in 
-    match r with
-      | ConstructRef _ -> rename_upper id
-      | _ -> rename_lower id
-
-  let rename_global r = id_of_string (rename_global_aux r)
-
-  let pp_type_global r = 
-    string (check_ml r ((module_option r)^(rename_type_global r)))
-
-  let pp_global r = 
-    string (check_ml r ((module_option r)^(rename_global_aux r)))
-
-  let cofix_warning = true
-end
-
-module ModularPp = Make(ModularParams)
-
-(*s Extraction to a file. *)
-
-let ocaml_preamble () =
-  [< 'sTR "type prop = unit"; 'fNL;
-     'sTR "let prop = ()"; 'fNL; 'fNL;
-     'sTR "type arity = unit"; 'fNL;
-     'sTR "let arity = ()"; 'fNL; 'fNL >]
-
-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 ()));
-  begin 
-    try
-      List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls
-    with e ->
-      pp_flush_with ft (); close_out cout; raise e
-  end;
-  pp_flush_with ft ();
-  close_out cout
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 58ee9b662f..2b00192309 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -15,34 +15,39 @@ open Miniml
 open Names
 open Term
 
+val current_module : identifier option ref
+
+val collapse_type_app : ml_type list -> ml_type list
+
 val string : string -> std_ppcmds
 val open_par : bool -> std_ppcmds
 val close_par : bool -> std_ppcmds
+val pp_abst : identifier list -> std_ppcmds
+val pr_binding : identifier list -> std_ppcmds
 
-val collect_lambda : ml_ast -> identifier list * ml_ast
-val push_vars : identifier list -> identifier list * Idset.t ->
-  identifier list * (identifier list * Idset.t)
+val rename_id : identifier -> Idset.t -> identifier
 
-val current_module : identifier option ref
+val lowercase_id : identifier -> identifier
+val uppercase_id : identifier -> identifier
 
-val module_of_r : global_reference -> module_ident
+type env = identifier list * Idset.t
 
-val string_of_r : global_reference -> string
+val rename_vars: Idset.t -> identifier list -> env
+val push_vars : identifier list -> env -> identifier list * env
+val get_db_name : int -> env -> identifier
+val collect_lambda : ml_ast -> identifier list * ml_ast
 
-val check_ml : global_reference -> string -> string
+val keywords : Idset.t
 
-val module_option : global_reference -> string
+val preamble : extraction_params -> std_ppcmds
 
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some 
     declarations to a file. *)
 
-open Mlutil
-
 module Make : functor(P : Mlpp_param) -> Mlpp
 
-val current_module : Names.identifier option ref
-val extract_to_file : 
-  string -> extraction_params -> ml_decl list -> unit
+
+
 
 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 3ad6246d37..6b5abf41c2 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -9,15 +9,35 @@
 (*i $Id$ i*)
 
 open Summary
+open Lib
+open Libobject
 open Goptions
 open Vernacinterp
 open Names
 open Util
 open Pp
-open Libobject
-open Term
+open Term 
 open Declarations
-open Lib
+
+
+(*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 Set and Map over global reference *)
 
@@ -55,24 +75,6 @@ let reference_of_varg = function
 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)
@@ -120,6 +122,36 @@ let _ =
        let refs = List.map check_constant (refs_of_vargl vl) in 
        add_anonymous_leaf (inline_extraction (false,refs)))
 
+(*s Printing part *)
+
+let print_inline () = 
+  let (i,n)= !inline_table in 
+  let i'= Refset.filter is_constant i in 
+  mSG 
+    [< 'sTR "Extraction Inline:"; 'fNL; 
+       Refset.fold
+	 (fun r p -> [< p; 'sTR  "   " ; Printer.pr_global r ; 'fNL >]) i' [<>];
+       'sTR "Extraction NoInline:"; 'fNL; 
+       Refset.fold
+	 (fun r p -> [< p; 'sTR  "   " ; Printer.pr_global r ; 'fNL >]) n [<>]
+    >]
+
+let _ = vinterp_add "PrintExtractionInline" (fun _ -> print_inline)
+
+
+(*s Reset part *)
+
+let (reset_inline,_) = 
+  declare_object
+    ("Reset Extraction Inline", 
+     {  cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
+	load_function = (fun (_,_)-> inline_table :=  empty_inline_table); 
+	open_function = (fun _ -> ());
+	export_function = (fun x -> Some x) })
+	
+let _ = vinterp_add "ResetExtractionInline" 
+	  (fun _ () -> add_anonymous_leaf (reset_inline ()))
+	  
 
 (*s Table for direct ML extractions. *)
 
@@ -167,6 +199,7 @@ let _ =
 	   (fun () -> 
 	      let r = check_constant (reference_of_varg id) in 
 	      let s = string_of_varg vs in 
+	      add_anonymous_leaf (inline_extraction (false,[r]));
 	      add_anonymous_leaf (in_ml_extraction (r,s)))
        | _ -> assert false)
 
@@ -206,3 +239,4 @@ let _ =
 	      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
index 7efbc0faaa..2a0a3092b1 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -8,11 +8,17 @@
 
 (*i $Id$ i*)
 
-open Summary
-open Goptions
 open Vernacinterp
 open Names
 
+(*s AutoInline parameter *) 
+
+val auto_inline : unit -> bool
+
+(*s Optimize parameter *) 
+
+val optim :  unit -> bool
+
 (*s Set and Map over global reference *) 
 
 module Refset : Set.S with type elt = global_reference
@@ -23,15 +29,7 @@ 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 *) 
+(*s Table for custom inlining *) 
 
 val to_inline : global_reference -> bool
 
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index e3e44e0513..787abb32ac 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -31,7 +31,9 @@ CMO:= $(patsubst %.ml,%.cmo,$(ML))
 #	General rules 
 #
 
-all: $(ML) $(CMO) v2ml
+all: ml $(CMO) v2ml
+
+ml: $(ML)
 
 depend: $(ML)
 	rm -f .depend; ocamldep $(INCL) theories/*/*.ml > .depend
diff --git a/contrib/extraction/test/addReals b/contrib/extraction/test/addReals
index 601592091a..fb73d47b5e 100644
--- a/contrib/extraction/test/addReals
+++ b/contrib/extraction/test/addReals
@@ -1,25 +1,21 @@
+open TypeSyntax
+open Fast_integer
+
+
 let total_order_T x y = 
-if x = y then
-        TypeSyntax.Coq_inleftT TypeSyntax.Coq_rightT
-else if x < y then
-        TypeSyntax.Coq_inleftT TypeSyntax.Coq_leftT
-else    TypeSyntax.Coq_inrightT 
+if x = y then InleftT RightT
+else if x < y then InleftT LeftT
+else InrightT 
 
 let rec int_to_positive i = 
-	if i = 1 then 
-	  Fast_integer.Coq_xH
+	if i = 1 then XH
 	else
-	  if (i mod 2) = 0 then 
-	      Fast_integer.Coq_xO (int_to_positive (i/2))
-	  else 
-	      Fast_integer.Coq_xI (int_to_positive (i/2))
+	  if (i mod 2) = 0 then XO (int_to_positive (i/2))
+	  else XI (int_to_positive (i/2))
 
 let rec int_to_Z i = 
-	if i = 0 then 
-	  Fast_integer.ZERO
-	else if i > 0 then 
-	  Fast_integer.POS (int_to_positive i)
-	else 
-	  Fast_integer.NEG (int_to_positive (-i))
+	if i = 0 then ZERO
+	else if i > 0 then POS (int_to_positive i)
+	else NEG (int_to_positive (-i))
 
 let my_ceil x = int_to_Z (succ (int_of_float (floor x)))