Major reorganisation of the extraction "backend".

Initial Idea: getting rid of nasty renaming issues in modules, in
 particular bugs #820 (part d) #1340 #1526 #1654

Final effect: lots of changes, simplifications, cleanups, unrelated
 fixes and ehancements, and also probably some regressions (time will 
 tell). 

A few details:

* no more experimental "Toplevel" language. 
* no more functors Make in Ocaml/Haskell/Scheme. The spirit of these
  functors and Mlpp_params was already not followed much, and this 
  framework was more a nuisance that anything else. 
* instead, some records language_descr regrouping the specific 
  features of the different output languages. 
* Common now comes before Ocaml/Haskell/Scheme, these ones are now 
  independant from each others. print_structure_to_file is now 
  in Extract_env. 
* A nice detail: no more duplications of warnings concerning axioms. 
* In modular extraction, the clashes due to the opened modules 
  are now computed once and for all thanks to record_contents_fstlev, 
  instead of re-asking Coq each time about these opened modules and 
  using Extraction.constant_kind 
* some utilities about modules_path added and/or moved from Modutil 
  to Table. 
* using a .v file as a module, e.g. in a functor application should 
  now works in modular extraction. 

Now concerning renaming issues themselves: 

* printing is done twice, the first time toward /dev/null, in order
  to encounter the naming issues unsolvable by a simple qualification. 
  On the second run, we create artificial modules Coq__123 for 
  allowing qualification of these hidden objects. 
* names are now fully separated into their syntaxic categories: 
  terms/types/constructors/modules
* Only one last unsupported situation (but at least detected and 
  signaled by an error): an object M.t from an external file-module
  M.v can't be printed when a local module M is in the way. 
  This situation is really unlikely (in Coq you must use _long_
  file-module name, e.g. Init.Datatypes.nat). It could be solved
  by inserting "module Coq_123 = M" at the beginning of the file, 
  but then the signature of Coq_123 (that is, the one of M) should 
  be written explicitely in the .mli, which is _really_ not nice. 





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

18 files changed, 1179 insertions, 1092 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 6db146b1e..855990d25 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -17,42 +17,218 @@ open Nameops
 open Libnames
 open Table
 open Miniml
+open Mlutil
 open Modutil
-open Ocaml
+open Mod_subst
 
-(*S Renamings. *)
+(*s Some pretty-print utility functions. *)
+
+let pp_par par st = if par then str "(" ++ st ++ str ")" else st
+
+let pp_apply st par args = match args with
+  | [] -> st
+  | _  -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
+
+let pr_binding = function
+  | [] -> mt ()
+  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
+
+let fnl2 () = fnl () ++ fnl () 
+
+let space_if = function true -> str " " | false -> mt ()
+
+let sec_space_if = function true -> spc () | false -> mt ()
+
+let is_digit = function 
+  | '0'..'9' -> true
+  | _ -> false
+
+let begins_with_CoqXX s = 
+  let n = String.length s in 
+  n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' &&
+  let i = ref 3 in 
+  try while !i < n do
+    if s.[!i] = '_' then i:=n (*Stop*)
+    else if is_digit s.[!i] then incr i 
+    else raise Not_found
+  done; true
+  with Not_found -> false
+  
+let unquote s = 
+  if lang () <> Scheme then s 
+  else 
+    let s = String.copy s in 
+    for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
+    s
+      
+let rec dottify = function 
+  | [] -> assert false 
+  | [s] -> unquote s 
+  | s::[""] -> unquote s 
+  | s::l -> (dottify l)^"."^(unquote s)
+
+(*s Uppercase/lowercase renamings. *) 
+
+let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
+let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
+
+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))
+
+(* [pr_upper_id id] makes 2 String.copy lesser than [pr_id (uppercase_id id)] *)
+let pr_upper_id id = str (String.capitalize (string_of_id id))
+
+
+(*s de Bruijn environments for programs *)
+
+type env = identifier list * Idset.t
+
+(*s Generic renaming issues for local variable names. *)
+
+let rec rename_id id avoid = 
+  if Idset.mem id avoid then rename_id (lift_ident id) avoid else id
+
+let rec rename_vars avoid = function
+  | [] -> 
+      [], avoid
+  | id :: idl when id == dummy_name ->
+      (* we don't rename dummy binders *)
+      let (idl', avoid') = rename_vars avoid idl in
+      (id :: idl', avoid')
+  | id :: idl ->
+      let (idl, avoid) = rename_vars avoid idl in
+      let id = rename_id (lowercase_id id) avoid in
+      (id :: idl, Idset.add id avoid)
+
+let rename_tvars avoid l = 
+  let rec rename avoid = function 
+    | [] -> [],avoid 
+    | id :: idl -> 
+	let id = rename_id (lowercase_id id) avoid in 
+	let idl, avoid = rename (Idset.add id avoid) idl in 
+	(id :: idl, avoid) in
+  fst (rename avoid l)
+
+let push_vars ids (db,avoid) =
+  let ids',avoid' = rename_vars avoid ids in
+  ids', (ids' @ db, avoid')
+
+let get_db_name n (db,_) = 
+  let id = List.nth db (pred n) in 
+  if id = dummy_name then id_of_string "__" else id
+
+
+(*S Renamings of global objects. *)
 
 (*s Tables of global renamings *)
 
 let keywords = ref Idset.empty
+let set_keywords kws = keywords := kws
+
 let global_ids = ref Idset.empty
-let modular = ref false
+let add_global_ids s = global_ids := Idset.add s !global_ids
+let global_ids_list () = Idset.elements !global_ids
+
+let empty_env () = [], !global_ids
+
+let mktable () = 
+  let h = Hashtbl.create 97 in 
+  (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
+
+let mkset () = 
+  let h = Hashtbl.create 97 in 
+  (fun x -> Hashtbl.add h x ()), (Hashtbl.mem h), (fun () -> Hashtbl.clear h)
+
+let mktriset () = 
+  let h = Hashtbl.create 97 in
+  (fun x y z -> Hashtbl.add h (x,y,z) ()), 
+  (fun x y z -> Hashtbl.mem h (x,y,z)), 
+  (fun () -> Hashtbl.clear h)
 
 (* For each [global_reference], this table will contain the different parts 
-   of its renamings, in [string list] form. *)
-let renamings = Hashtbl.create 97
-let rename r l = Hashtbl.add renamings r l
-let get_renamings r = Hashtbl.find renamings r 
+   of its renaming, in [string list] form. *)
+let add_renaming, get_renaming, clear_renaming = mktable ()
 
 (* Idem for [module_path]. *)
-let mp_renamings = Hashtbl.create 97
-let mp_rename mp l = Hashtbl.add mp_renamings mp l
-let mp_get_renamings mp = Hashtbl.find mp_renamings mp 
+let add_mp_renaming, get_mp_renaming, clear_mp_renaming = mktable ()
 
-let modvisited = ref MPset.empty
-let modcontents = ref Gset.empty
-let add_module_contents mp s = modcontents := Gset.add (mp,s) !modcontents
-let module_contents mp s = Gset.mem (mp,s) !modcontents
+(* A table for function modfstlev_rename *)
+let add_modfstlev, get_modfstlev, clear_modfstlev = mktable ()
 
-let to_qualify = ref Refset.empty
+(* A set of all external objects that will have to be fully qualified *)
+let add_static_clash, static_clash, clear_static_clash = mkset ()
 
-let mod_1st_level = ref Idmap.empty
+(* Two tables of triplets [kind * module_path * string]. The first one 
+   will record the first level of all MPfile, not only the current one. 
+   The second table will contains local renamings. *)
 
-(*s Uppercase/lowercase renamings. *) 
+type kind = Term | Type | Cons | Mod
 
-let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
+let add_ext_mpmem, ext_mpmem, clear_ext_mpmem = mktriset ()
+let add_loc_mpmem, loc_mpmem, clear_loc_mpmem = mktriset ()
 
-let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
+(* The list of external modules that will be opened initially *)
+let add_mpfiles, mem_mpfiles, list_mpfiles, clear_mpfiles = 
+  let m = ref MPset.empty in 
+  (fun mp -> m:= MPset.add mp !m), 
+  (fun mp -> MPset.mem mp !m),
+  (fun () -> MPset.elements !m),
+  (fun () -> m:= MPset.empty)
+
+(*s table containing the visible horizon at a precise moment *)
+
+let visible = ref ([] : module_path list)
+let pop_visible () = visible := List.tl !visible
+let push_visible mp = visible := mp :: !visible
+let top_visible_mp () = List.hd !visible
+
+(*s substitutions for printing signatures *)
+
+let substs = ref empty_subst
+let add_subst msid mp = substs := add_msid msid mp !substs
+let subst_mp mp = subst_mp !substs mp
+let subst_kn kn = subst_kn !substs kn
+let subst_con c = fst (subst_con !substs c)
+let subst_ref = function 
+  | ConstRef con -> ConstRef (subst_con con)
+  | IndRef (kn,i) -> IndRef (subst_kn kn,i)
+  | ConstructRef ((kn,i),j) -> ConstructRef ((subst_kn kn,i),j)
+  | _ -> assert false
+
+
+let duplicate_index = ref 0
+let to_duplicate = ref Gmap.empty
+let add_duplicate mp l = 
+  incr duplicate_index; 
+  let ren = "Coq__" ^ string_of_int (!duplicate_index) in 
+  to_duplicate := Gmap.add (mp,l) ren !to_duplicate
+let check_duplicate mp l = 
+  let mp' = subst_mp mp in 
+  Gmap.find (mp',l) !to_duplicate
+
+type reset_kind = OnlyLocal | AllButExternal | Everything
+
+let reset_allbutext () = 
+  clear_loc_mpmem (); 
+  global_ids := !keywords; 
+  clear_renaming (); 
+  clear_mp_renaming (); 
+  clear_modfstlev (); 
+  clear_static_clash (); 
+  clear_mpfiles (); 
+  duplicate_index := 0; 
+  to_duplicate := Gmap.empty; 
+  visible := []; 
+  substs := empty_subst
+ 
+let reset_everything () = reset_allbutext (); clear_ext_mpmem ()
+
+let reset_renaming_tables = function 
+  | OnlyLocal -> clear_loc_mpmem ()
+  | AllButExternal -> reset_allbutext ()
+  | Everything -> reset_everything ()
+
+(*S Renaming functions *)
 
 (* This function creates from [id] a correct uppercase/lowercase identifier. 
    This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes 
@@ -69,389 +245,237 @@ let modular_rename up id =
   then prefix ^ s
   else s
 
-let rename_module = modular_rename true 
-
-(* [clash mp0 l s mpl] checks if [mp0-l-s] can be printed as [l-s] when 
-   [mpl] is the context of visible modules. More precisely, we check if 
-   there exists a mp1, module (sub-)path of an element of [mpl], such as 
-   module [mp1-l] contains [s]. 
-   The verification stops if we encounter [mp1=mp0]. *)
-
-exception Stop 
-
-let clash mp0 l s mpl = 
-  let rec clash_one mp = match mp with
-    | _ when mp = mp0 -> raise Stop
-    | MPdot (mp',_) -> 
-	(module_contents (add_labels_mp mp l) s) || (clash_one mp') 
-    | mp when is_toplevel mp -> false
-    | _ -> module_contents (add_labels_mp mp l) s
+(*s [record_contents_fstlev] finds the names of the first-level objects 
+  exported by the ground-level modules in [struc]. *)
+
+let rec record_contents_fstlev struc = 
+  let upper_type = (lang () = Haskell) in 
+  let addtyp mp id = add_ext_mpmem Type mp (modular_rename upper_type id) in
+  let addcons mp id = add_ext_mpmem Cons mp (modular_rename true id) in
+  let addterm mp id = add_ext_mpmem Term mp (modular_rename false id) in
+  let addmod mp id = add_ext_mpmem Mod mp (modular_rename true id) in 
+  let addfix mp r = 
+    add_ext_mpmem Term mp (modular_rename false (id_of_global r))
   in
-  let rec clash_list = function 
-    | [] -> false
-    | mp :: mpl -> (clash_one mp) || (clash_list mpl) 
-  in try clash_list mpl with Stop -> false
-
-(*s [contents_first_level mp] finds the names of the first-level objects 
-  exported by module [mp]. Nota: it might fail if [mp] isn't a directly 
-  visible module. Ex: [MPself] under functor, [MPbound], etc ... *)
-
-let contents_first_level mp = 
-  if not (MPset.mem mp !modvisited) then begin 
-    modvisited := MPset.add mp !modvisited; 
-    match (Global.lookup_module mp).mod_type with 
-      | MTBsig (msid,msb) -> 
-	  let add b id = add_module_contents mp (modular_rename b id) in 
-	  let upper_type = (lang () = Haskell) in
-	  List.iter 
-	    (function 
-	       | (l, SPBconst cb) -> 
-		   (match Extraction.constant_kind (Global.env ()) cb with 
-		      | Extraction.Logical -> () 
-		      | Extraction.Type -> add upper_type (id_of_label l)
-		      | Extraction.Term -> add false (id_of_label l))
-	       | (_, SPBmind mib) ->
-		   Array.iter 
-		     (fun mip -> if snd (Inductive.mind_arity mip) <> InProp
-		      then begin
-			add upper_type mip.mind_typename; 
-			Array.iter (add true) mip.mind_consnames
-		      end)
-		     mib.mind_packets
-	       | _ -> ())
-	    (Modops.subst_signature_msid msid mp msb)
-      | _ -> ()
-  end
+  let f mp = function 
+    | (l,SEdecl (Dind (_,ind))) -> 
+	Array.iter 
+	  (fun ip -> 
+	     addtyp mp ip.ip_typename; Array.iter (addcons mp) ip.ip_consnames)
+	  ind.ind_packets
+    | (l,SEdecl (Dtype _)) -> addtyp mp (id_of_label l)
+    | (l,SEdecl (Dterm _)) -> addterm mp (id_of_label l)
+    | (l,SEdecl (Dfix  (rv,_,_))) -> Array.iter (addfix mp) rv
+    | (l,SEmodule _) -> addmod mp (id_of_label l)
+    | (l,SEmodtype _) -> addmod mp (id_of_label l)
+  in
+  List.iter (fun (mp,sel) -> List.iter (f mp) sel) struc
 
-(*s Initial renamings creation, for modular extraction. *) 
+(*s For monolithic extraction, first-level modules might have to be renamed 
+    with unique numbers *)
+
+let modfstlev_rename l =
+  let coqid = id_of_string "Coq" in 
+  let id = id_of_label l in 
+  try 
+    let coqset = get_modfstlev id in 
+    let nextcoq = next_ident_away coqid coqset in 
+    add_modfstlev id (nextcoq::coqset); 
+    (string_of_id nextcoq)^"_"^(string_of_id id) 
+  with Not_found -> 
+    let s = string_of_id id in 
+    if is_lower s || begins_with_CoqXX s then
+      (add_modfstlev id [coqid]; "Coq_"^s)
+    else
+      (add_modfstlev id []; s)
+
+(*s Creating renaming for a [module_path] *)
 
-let rec mp_create_modular_renamings mp = 
-  try mp_get_renamings mp 
+let rec mp_create_renaming mp = 
+  try get_mp_renaming mp 
   with Not_found -> 
     let ren = match mp with 
+      | _ when not (modular ()) && at_toplevel mp -> [""]
       | MPdot (mp,l) -> 
-	  (rename_module (id_of_label l)) :: (mp_create_modular_renamings mp)
-      | MPself msid -> [rename_module (id_of_msid msid)]
-      | MPbound mbid -> [rename_module (id_of_mbid mbid)]
-      | MPfile f -> [String.capitalize (string_of_id (List.hd (repr_dirpath f)))]
-    in mp_rename mp ren; ren
+	  let lmp = mp_create_renaming mp in 
+	  if lmp = [""] then (modfstlev_rename l)::lmp
+	  else (modular_rename true (id_of_label l))::lmp
+      | MPself msid -> [modular_rename true (id_of_msid msid)]
+      | MPbound mbid -> [modular_rename true (id_of_mbid mbid)]
+      | MPfile _ when not (modular ()) -> assert false
+      | MPfile _ -> [string_of_modfile mp]
+    in add_mp_renaming mp ren; ren
+
+(* [clash mp0 s mpl] checks if [mp0-s] can be printed as [s] when 
+   [mpl] is the context of visible modules. More precisely, we check if 
+   there exists a [mp] in [mpl] that contains [s]. 
+   The verification stops if we encounter [mp=mp0]. *)
 
+let rec clash mem mp0 s = function 
+  | [] -> false
+  | mp :: _ when mp = mp0 -> false
+  | mp :: mpl -> mem mp s || clash mem mp0 s mpl
+    
+(*s Initial renamings creation, for modular extraction. *) 
 
 let create_modular_renamings struc = 
   let current_module = fst (List.hd struc) in 
-  let modfiles = ref MPset.empty in 
-  let { up = u ; down = d } = struct_get_references_set struc 
+  let { typ = ty ; trm = tr ; cons = co } = struct_get_references_set struc 
   in 
   (* 1) creates renamings of objects *)
   let add upper r = 
     let mp = modpath_of_r r in 
-    let l = mp_create_modular_renamings mp in 
+    let l = mp_create_renaming mp in 
     let s = modular_rename upper (id_of_global r) in 
-    global_ids := Idset.add (id_of_string s) !global_ids;    
-    rename r (s::l); 
+    add_global_ids (id_of_string s);
+    add_renaming r (s::l); 
     begin try 
-      let mp = modfile_of_mp mp in 
-      if mp <> current_module then modfiles := MPset.add mp !modfiles
+      let mp = modfile_of_mp mp in if mp <> current_module then add_mpfiles mp
     with Not_found -> () 
     end; 
   in
-  Refset.iter (add true) u; 
-  Refset.iter (add false) d; 
+  Refset.iter (add (lang () = Haskell)) ty; 
+  Refset.iter (add true) co;
+  Refset.iter (add false) tr;
   
   (* 2) determines the opened libraries. *)
-  let used_modules = MPset.elements !modfiles in 
-
-  (* [s] will contain all first-level sub-modules of [cur_mp] *)
-  let s = ref Stringset.empty in 
-  begin 
-    let add l = s := Stringset.add (rename_module (id_of_label l)) !s in 
-    match (Global.lookup_module current_module).mod_type with 
-      | MTBsig (_,msb) ->
-	  List.iter (function (l,SPBmodule _) -> add l | _ -> ()) msb
-      | _ -> ()
-  end;
-  (* We now compare [s] with the modules coming from [used_modules]. *)
-  List.iter 
-    (function 
-       | MPfile d -> 
-	   let s_mp = 
-	     String.capitalize (string_of_id (List.hd (repr_dirpath d))) in 
-	   if Stringset.mem s_mp !s then error_module_clash s_mp 
-	   else s:= Stringset.add s_mp !s 
-       | _ -> assert false)
-    used_modules;
+  let used_modules = list_mpfiles () in 
+  let used_modules' = List.rev used_modules in 
+  let str_list = List.map string_of_modfile used_modules' 
+  in
+  let rec check_elsewhere mpl sl = match mpl, sl with
+    | [], [] -> []
+    | mp::mpl, _::sl -> 
+	if List.exists (ext_mpmem Mod mp) sl then
+	  check_elsewhere mpl sl
+	else mp :: (check_elsewhere mpl sl)
+    | _ -> assert false
+  in 
+  let opened_modules = check_elsewhere used_modules' str_list in 
+  clear_mpfiles (); 
+  List.iter add_mpfiles opened_modules; 
 
   (* 3) determines the potential clashes *)
-  List.iter contents_first_level used_modules; 
-  let used_modules' = List.rev used_modules in 
-  let needs_qualify r = 
+  let needs_qualify k r = 
     let mp = modpath_of_r r in 
     if (is_modfile mp) && mp <> current_module && 
-      (clash mp [] (List.hd (get_renamings r)) used_modules')
-    then to_qualify := Refset.add r !to_qualify
+      (clash (ext_mpmem k) mp (List.hd (get_renaming r)) opened_modules)
+    then add_static_clash r
   in
-  Refset.iter needs_qualify u;
-  Refset.iter needs_qualify d; 
-  used_modules
+  Refset.iter (needs_qualify Type) ty;
+  Refset.iter (needs_qualify Term) tr;
+  Refset.iter (needs_qualify Cons) co;
+  List.rev opened_modules
 
 (*s Initial renamings creation, for monolithic extraction. *)
 
-let begins_with_CoqXX s = 
-  (String.length s >= 4) && 
-  (String.sub s 0 3 = "Coq") &&
-  (try 
-     for i = 4 to (String.index s '_')-1 do 
-       match s.[i] with 
-	 | '0'..'9' -> () 
-	 | _ -> raise Not_found
-     done; 
-     true
-   with Not_found -> false)
-
-let mod_1st_level_rename l =
-  let coqid = id_of_string "Coq" in 
-  let id = id_of_label l in 
-  try 
-    let coqset = Idmap.find id !mod_1st_level in 
-    let nextcoq = next_ident_away coqid coqset in 
-    mod_1st_level := Idmap.add id (nextcoq::coqset) !mod_1st_level; 
-    (string_of_id nextcoq)^"_"^(string_of_id id) 
-  with Not_found -> 
-    let s = string_of_id id in 
-    if is_lower s || begins_with_CoqXX s then
-      (mod_1st_level := Idmap.add id [coqid] !mod_1st_level; "Coq_"^s)
-    else
-      (mod_1st_level := Idmap.add id [] !mod_1st_level; s)
-
-let rec mp_create_mono_renamings mp = 
-  try mp_get_renamings mp 
-  with Not_found -> 
-    let ren = match mp with 
-       | _ when (at_toplevel mp) -> [""]
-       | MPdot (mp,l) -> 
-	   let lmp = mp_create_mono_renamings mp in
-	   if lmp = [""] then (mod_1st_level_rename l)::lmp
-	   else (rename_module (id_of_label l))::lmp
-       | MPself msid -> [rename_module (id_of_msid msid)]
-       | MPbound mbid -> [rename_module (id_of_mbid mbid)]
-       | _ -> assert false
-    in mp_rename mp ren; ren
-
 let create_mono_renamings struc = 
-  let { up = u ; down = d } = struct_get_references_list struc in 
+  let { typ = ty ; trm = tr ; cons = co } = struct_get_references_list struc in
   let add upper r = 
     let mp = modpath_of_r r in 
-    let l = mp_create_mono_renamings mp in
+    let l = mp_create_renaming mp in
     let mycase = if upper then uppercase_id else lowercase_id in 
     let id = 
       if l = [""] then 
-	next_ident_away (mycase (id_of_global r)) (Idset.elements !global_ids)
+	next_ident_away (mycase (id_of_global r)) (global_ids_list ())
       else id_of_string (modular_rename upper (id_of_global r))
     in 
-    global_ids := Idset.add id !global_ids;    
-    rename r ((string_of_id id)::l) 
+    add_global_ids id; 
+    add_renaming r ((string_of_id id)::l) 
   in
-  List.iter (add true) (List.rev u); 
-  List.iter (add false) (List.rev d)
-		    
-(*s Renaming issues at toplevel *)
-
-module TopParams = struct
-  let globals () = Idset.empty
-  let pp_global _ r = pr_id (id_of_global r)
-  let pp_module _ mp = str (string_of_mp mp)
-end
-
-(*s Renaming issues for a monolithic or modular extraction. *)
-
-module StdParams = struct
-
-  let globals () = !global_ids
-
-  let unquote s = 
-    if lang () <> Scheme then s 
-    else 
-      let s = String.copy s in 
-      for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
-      s
-
-  let rec dottify = function 
-    | [] -> assert false 
-    | [s] -> unquote s 
-    | s::[""] -> unquote s 
-    | s::l -> (dottify l)^"."^(unquote s)
-
-  let pp_global mpl r = 
-    let ls = get_renamings r in 
-    let s = List.hd ls in 
-    let mp = modpath_of_r r in 
-    let ls = 
-      if mp = List.hd mpl then [s] (* simpliest situation *)
-      else match lang () with 
-	| Scheme -> [s] (* no modular Scheme extraction... *)
-	| Toplevel -> [s] (* idem *)
-	| Haskell -> 
-	    if !modular then 
-	      ls (* for the moment we always qualify in modular Haskell *)
-	    else [s]
-	| Ocaml -> 
-	    try (* has [mp] something in common with one of those in [mpl] ? *)
-	      let pref = common_prefix_from_list mp mpl in 
-	      (*i TODO: possibilité de clash i*)
-	      list_firstn ((mp_length mp)-(mp_length pref)+1) ls
-	    with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
-	      let base = base_mp mp in 
-	      if !modular &&  
-		(at_toplevel mp) && 
-		not (Refset.mem r !to_qualify) && 
-		not (clash base [] s mpl) 
-	      then snd (list_sep_last ls)
-	      else ls
-    in 
-    add_module_contents mp s; (* update the visible environment *)
-    str (dottify ls)
-
-  (* The next function is used only in Ocaml extraction...*)
-  let pp_module mpl mp = 
-    let ls = 
-      if !modular 
-      then mp_create_modular_renamings mp 
-      else mp_create_mono_renamings mp 
-    in 
-    let ls = 
-      try (* has [mp] something in common with one of those in [mpl] ? *)
-	let pref = common_prefix_from_list mp mpl in 
-	(*i TODO: clash possible i*)
-	list_firstn ((mp_length mp)-(mp_length pref)) ls
-      with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
-	if !modular && (at_toplevel mp) 
-	then snd (list_sep_last ls)
-	else ls
-    in str (dottify ls) 
-
-end
-
-module ToplevelPp = Ocaml.Make(TopParams)
-module OcamlPp = Ocaml.Make(StdParams)
-module HaskellPp = Haskell.Make(StdParams)
-module SchemePp = Scheme.Make(StdParams)
-
-let pp_decl mp d = match lang () with 
-  | Ocaml -> OcamlPp.pp_decl mp d 
-  | Haskell -> HaskellPp.pp_decl mp d
-  | Scheme -> SchemePp.pp_decl mp d 
-  | Toplevel -> ToplevelPp.pp_decl mp d 
-
-let pp_struct s = match lang () with 
-  | Ocaml -> OcamlPp.pp_struct s 
-  | Haskell -> HaskellPp.pp_struct s
-  | Scheme -> SchemePp.pp_struct s
-  | Toplevel -> ToplevelPp.pp_struct s
-
-let pp_signature s = match lang () with 
-  | Ocaml -> OcamlPp.pp_signature s 
-  | Haskell -> HaskellPp.pp_signature s
-  | _ -> assert false
-
-let set_keywords () =
-  (match lang () with 
-    | Ocaml -> keywords := Ocaml.keywords
-    | Haskell -> keywords := Haskell.keywords
-    | Scheme -> keywords := Scheme.keywords
-    | Toplevel -> keywords := Idset.empty);
-  global_ids := !keywords; 
-  to_qualify := Refset.empty
+  List.iter (add (lang () = Haskell)) (List.rev ty); 
+  List.iter (add false) (List.rev tr);
+  List.iter (add true) (List.rev co);
+  []
+
+let create_renamings struc = 
+  if modular () then create_modular_renamings struc
+  else create_mono_renamings struc
     
-let preamble prm = match lang () with 
-  | Ocaml -> Ocaml.preamble prm   
-  | Haskell -> Haskell.preamble prm
-  | Scheme -> Scheme.preamble prm
-  | Toplevel -> (fun _ _ _ -> mt ())
-
-let preamble_sig prm = match lang () with 
-  | Ocaml -> Ocaml.preamble_sig prm   
-  | _ -> assert false
-
-(*S Extraction of one decl to stdout. *)
-
-let print_one_decl struc mp decl = 
-  set_keywords (); 
-  modular := false; 
-  create_mono_renamings struc;
-  msgnl (pp_decl [mp] decl)
-
-(*S Extraction to a file. *)
-
-let info f = 
-  Options.if_verbose msgnl 
-    (str ("The file "^f^" has been created by extraction."))
-
-let print_structure_to_file f prm struc =
-  Hashtbl.clear renamings;
-  mod_1st_level := Idmap.empty; 
-  modcontents := Gset.empty;
-  modvisited := MPset.empty; 
-  set_keywords ();
-  modular := prm.modular; 
-  let used_modules =
-    if lang () = Toplevel then []
-    else if prm.modular then create_modular_renamings struc
-    else (create_mono_renamings struc; [])
-  in 
-  let print_dummys =
-    (struct_ast_search ((=) MLdummy) struc, 
-     struct_type_search Mlutil.isDummy struc, 
-     struct_type_search ((=) Tunknown) struc)
-  in 
-  let print_magic = 
-    if lang () <> Haskell then false 
-    else struct_ast_search (function MLmagic _ -> true | _ -> false) struc
-  in
-  (* print the implementation *)
-  let cout = option_map (fun (f,_) -> open_out f) f in 
-  let ft = match cout with 
-    | None -> !Pp_control.std_ft
-    | Some cout -> Pp_control.with_output_to cout in 
-  begin try 
-    msg_with ft (preamble prm used_modules print_dummys print_magic);
-    msg_with ft (pp_struct struc);
-    option_iter close_out cout; 
-  with e -> 
-    option_iter close_out cout; raise e
-  end;
-  option_iter (fun (f,_) -> info f) f;
-  (* print the signature *)
-  match f with 
-    | Some (_,f) when lang () = Ocaml -> 
-	let cout = open_out f in
-	let ft = Pp_control.with_output_to cout in
-	begin try 
-	  msg_with ft (preamble_sig prm used_modules print_dummys);
-	  msg_with ft (pp_signature (signature_of_structure struc));
-	  close_out cout;
-	with e -> 
-	  close_out cout; raise e 
-	end; 
-	info f 
-    | _ -> ()
-	  
-
-(*i 
-  (* DO NOT REMOVE: used when making names resolution *)
-  let cout = open_out (f^".ren") in 
-  let ft = Pp_control.with_output_to cout in
-  Hashtbl.iter 
-    (fun r id -> 
-       if short_module r = !current_module then 
-	 msgnl_with ft (pr_id id ++ str " " ++ pr_sp (sp_of_r r)))
-    renamings;
-  pp_flush_with ft ();
-  close_out cout;
-i*)    
-
-
-
-
-
-
+		    
+(*s On-the-fly qualification issues for both monolithic or modular extraction. *)
+
+let pp_global k r = 
+  let ls = get_renaming r in 
+  assert (List.length ls > 1); 
+  let s = List.hd ls in 
+  let mp = modpath_of_r r in 
+  if mp = top_visible_mp () then 
+    (* simpliest situation: definition of r (or use in the same context) *)
+    (* we update the visible environment *)
+    (add_loc_mpmem k mp s; unquote s)
+  else match lang () with 
+    | Scheme -> unquote s (* no modular Scheme extraction... *)
+    | Haskell -> 
+	(* for the moment we always qualify in modular Haskell *)
+	if modular () then dottify ls else s
+    | Ocaml -> 
+	try (* has [mp] something in common with one of [!visible] ? *)
+	  let prefix = common_prefix_from_list mp !visible in 
+	  let delta = mp_length mp - mp_length prefix in 
+	  let ls = list_firstn (delta+1) ls in 
+	  (* Difficulty: in ocaml we cannot qualify more than [ls], 
+             but this (not-so-long) name can in fact be hidden. Solution: 
+	     duplication of the _definition_ of r in a Coq__XXX module *)
+	  let s,ls' = list_sep_last ls in 
+	  let k' = if ls' = [] then k else Mod in 
+	  if clash (loc_mpmem k') prefix s !visible then 
+	    let front = if ls' = [] then [s] else ls' in 
+	    let l = get_nth_label delta r in 
+	    try dottify (front @ [check_duplicate prefix l])
+	    with Not_found -> add_duplicate prefix l; dottify ls
+	  else dottify ls 
+	with Not_found -> 
+	  (* [mp] belongs to a closed module, not one of [!visible]. *)
+	  let base = base_mp mp in 
+	  let base_s,ls1 = list_sep_last ls in 
+	  let s,ls2 = list_sep_last ls1 in  
+	  let k' = if ls2 = [] then k else Mod in 
+	  if modular () && (mem_mpfiles base) && 
+	    not (static_clash r) && 
+	    (* k' = Mod can't clash in an opened module, see earlier check *)
+	    not (clash (loc_mpmem k') base s !visible)
+	  then (* Standard situation of an object in another file: *)
+	    (* Thanks to the "open" of this file we remove its name *) 
+	    dottify ls1
+	  else if clash (loc_mpmem Mod) base base_s !visible then 
+	    error_module_clash base_s
+	  else dottify ls 
+	    
+(* The next function is used only in Ocaml extraction...*)
+let pp_module mp = 
+  let ls = mp_create_renaming mp in
+  if List.length ls = 1 then dottify ls 
+  else match mp with 
+    | MPdot (mp0,_) when mp0 = top_visible_mp () -> 
+	(* simpliest situation: definition of mp (or use in the same context) *)
+	(* we update the visible environment *)
+	let s = List.hd ls in 
+	add_loc_mpmem Mod mp0 s; s
+    | _ ->
+	try (* has [mp] something in common with one of those in [!visible] ? *)
+	  let prefix = common_prefix_from_list mp !visible in 
+	  assert (mp <> prefix); (* no use of mp as whole module from itself *)
+	  let delta = mp_length mp - mp_length prefix in 
+	  let ls = list_firstn delta ls in
+	  (* Difficulty: in ocaml we cannot qualify more than [ls], 
+	     but this (not-so-long) name can in fact be hidden. Solution: 
+	     duplication of the _definition_ of mp via a Coq__XXX module *)
+	  let s,ls' = list_sep_last ls in 
+	  if clash (loc_mpmem Mod) prefix s !visible then 
+	    let l = get_nth_label_mp delta mp in 
+	    try dottify (ls' @ [check_duplicate prefix l])
+	    with Not_found -> add_duplicate prefix l; dottify ls
+	  else dottify ls
+	with Not_found -> 
+	  (* [mp] belongs to a closed module, not one of [!visible]. *)
+	  let base = base_mp mp in 
+	  let base_s,ls' = list_sep_last ls in 
+	  let s = fst (list_sep_last ls) in 
+	  if modular () && (mem_mpfiles base) &&
+	    not (clash (loc_mpmem Mod) base s !visible)
+	  then dottify ls'
+	  else if clash (loc_mpmem Mod) base base_s !visible then 
+	    error_module_clash base_s
+	  else dottify ls
 
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index f35c0dea5..e17326bc9 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -9,13 +9,53 @@
 (*i $Id$ i*)
 
 open Names
+open Libnames
 open Miniml
 open Mlutil
+open Pp
 
-val print_one_decl :
-  ml_structure -> module_path -> ml_decl -> unit
+val fnl2 : unit -> std_ppcmds
+val space_if : bool -> std_ppcmds
+val sec_space_if : bool -> std_ppcmds
 
-val print_structure_to_file : 
-  (string * string) option -> extraction_params -> ml_structure -> unit
+val pp_par : bool -> std_ppcmds -> std_ppcmds
+val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds 
+val pr_binding : identifier list -> std_ppcmds
 
+val rename_id : identifier -> Idset.t -> identifier
 
+val lowercase_id : identifier -> identifier
+val uppercase_id : identifier -> identifier
+
+val pr_upper_id : identifier -> std_ppcmds
+
+type env = identifier list * Idset.t
+val empty_env : unit -> env
+
+val rename_vars: Idset.t -> identifier list -> env
+val rename_tvars: Idset.t -> identifier list -> identifier list 
+val push_vars : identifier list -> env -> identifier list * env
+val get_db_name : int -> env -> identifier
+
+val record_contents_fstlev : ml_structure -> unit
+
+val create_renamings : ml_structure -> module_path list
+
+type kind = Term | Type | Cons | Mod
+
+val pp_global : kind -> global_reference -> string
+val pp_module : module_path -> string
+
+val top_visible_mp : unit -> module_path
+val push_visible : module_path -> unit
+val pop_visible : unit -> unit
+
+val add_subst : mod_self_id -> module_path -> unit
+
+val check_duplicate : module_path -> label -> string
+
+type reset_kind = OnlyLocal | AllButExternal | Everything
+
+val reset_renaming_tables : reset_kind -> unit
+
+val set_keywords : Idset.t -> unit
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 0ef993057..953e4930b 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -21,7 +21,9 @@ open Modutil
 open Common
 open Mod_subst
 
-(*s Obtaining Coq environment. *)
+(***************************************)
+(*S Part I: computing Coq environment. *)
+(***************************************)
 
 let toplevel_env () = 
   let seg = Lib.contents_after None in 
@@ -156,22 +158,19 @@ let rec extract_msig env mp = function
 	(l,Spec s) :: (extract_msig env mp msig)
       end
   | (l,SPBmodule {msb_modtype=mtb}) :: msig -> 
-      (l,Smodule (extract_mtb env None mtb)) :: (extract_msig env mp msig)
+      (l,Smodule (extract_mtb env mtb)) :: (extract_msig env mp msig)
   | (l,SPBmodtype mtb) :: msig -> 
-      (l,Smodtype (extract_mtb env None mtb)) :: (extract_msig env mp msig)
+      (l,Smodtype (extract_mtb env mtb)) :: (extract_msig env mp msig)
 
-and extract_mtb env mpo = function 
+and extract_mtb env = function 
   | MTBident kn -> Visit.add_kn kn; MTident kn 
   | MTBfunsig (mbid, mtb, mtb') -> 
       let mp = MPbound mbid in 
       let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in 
-      MTfunsig (mbid, extract_mtb env None mtb, 
-		extract_mtb env' None mtb') 
+      MTfunsig (mbid, extract_mtb env mtb, 
+		extract_mtb env' mtb') 
   | MTBsig (msid, msig) -> 
-      let mp, msig = match mpo with 
-	| None -> MPself msid, msig
-	| Some mp -> mp, Modops.subst_signature_msid msid mp msig
-      in
+      let mp = MPself msid in 
       let env' = Modops.add_signature mp msig env in 
       MTsig (msid, extract_msig env' mp msig) 
 
@@ -216,19 +215,20 @@ let rec extract_msb env mp all = function
       let ms = extract_msb env mp all msb in
       let kn = make_kn mp empty_dirpath l in
       if all || Visit.needed_kn kn then 
-	(l,SEmodtype (extract_mtb env None mtb)) :: ms
+	(l,SEmodtype (extract_mtb env mtb)) :: ms
       else ms
 
 and extract_meb env mpo all = function 
-  | MEBident (MPfile d) -> error_MPfile_as_mod d (* temporary (I hope) *)
-  | MEBident mp -> Visit.add_mp mp; MEident mp 
+  | MEBident mp -> 
+      if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp; 
+      Visit.add_mp mp; MEident mp 
   | MEBapply (meb, meb',_) -> 
       MEapply (extract_meb env None true meb, 
 	       extract_meb env None true meb')
   | MEBfunctor (mbid, mtb, meb) -> 
       let mp = MPbound mbid in 
       let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in 
-      MEfunctor (mbid, extract_mtb env None mtb, 
+      MEfunctor (mbid, extract_mtb env mtb, 
 		 extract_meb env' None true meb)
   | MEBstruct (msid, msb) -> 
       let mp,msb = match mpo with 
@@ -247,7 +247,7 @@ and extract_module env mp all mb =
   (* a msid different from the one of the module. Here is the patch. *)
   let mtb = replicate_msid meb mtb in
   { ml_mod_expr = extract_meb env (Some mp) all meb;
-    ml_mod_type = extract_mtb env None mtb }
+    ml_mod_type = extract_mtb env mtb }
 
 let unpack = function MEstruct (_,sel) -> sel | _ -> assert false 
 
@@ -260,14 +260,118 @@ let mono_environment refs mpl =
   List.rev_map 
     (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) false m)) l
 
-    
+(**************************************)
+(*S Part II : Input/Output primitives *)
+(**************************************)
+
+let descr () = match lang () with 
+  | Ocaml -> Ocaml.ocaml_descr 
+  | Haskell -> Haskell.haskell_descr 
+  | Scheme -> Scheme.scheme_descr
+
+(* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli" 
+   Works similarly for the other languages. *)
+
+let mono_filename f = 
+  let d = descr () in 
+  match f with 
+    | None -> None, None, id_of_string "Main"
+    | Some f -> 
+	let f = 
+	  if Filename.check_suffix f d.file_suffix then 
+	    Filename.chop_suffix f d.file_suffix 
+	  else f
+	in 
+	Some (f^d.file_suffix), option_map ((^) f) d.sig_suffix, id_of_string f
+
+(* Builds a suitable filename from a module id *)
+
+let module_filename m = 
+  let d = descr () in 
+  let f = if d.capital_file then String.capitalize else String.uncapitalize in 
+  let fn = f (string_of_id m) in
+  Some (fn^d.file_suffix), option_map ((^) fn) d.sig_suffix, m
+
+(*s Extraction of one decl to stdout. *)
+
+let print_one_decl struc mp decl =
+  let d = descr () in 
+  reset_renaming_tables AllButExternal; 
+  ignore (create_renamings struc);
+  push_visible mp; 
+  msgnl (d.pp_decl decl); 
+  pop_visible ()
+
+(*s Extraction of a ml struct to a file. *)
+
+let print_structure_to_file (fn,si,mo) struc =
+  let d = descr () in 
+  reset_renaming_tables AllButExternal; 
+  let used_modules = create_renamings struc in 
+  let unsafe_needs = {
+    mldummy = struct_ast_search ((=) MLdummy) struc; 
+    tdummy = struct_type_search Mlutil.isDummy struc; 
+    tunknown = struct_type_search ((=) Tunknown) struc; 
+    magic = 
+      if lang () <> Haskell then false 
+      else struct_ast_search (function MLmagic _ -> true | _ -> false) struc }
+  in
+  (* print the implementation *)
+  let cout = option_map open_out fn in 
+  let ft = match cout with 
+    | None -> !Pp_control.std_ft
+    | Some cout -> Pp_control.with_output_to cout in 
+  let devnull = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in 
+  begin try 
+    msg_with ft (d.preamble mo used_modules unsafe_needs);
+    msg_with devnull (d.pp_struct struc); (* for computing objects to duplicate *)
+    reset_renaming_tables OnlyLocal; 
+    msg_with ft (d.pp_struct struc);
+    option_iter close_out cout; 
+  with e -> 
+    option_iter close_out cout; raise e
+  end;
+  option_iter info_file fn;
+  (* print the signature *)
+  option_iter 
+    (fun si -> 
+       let cout = open_out si in
+       let ft = Pp_control.with_output_to cout in
+       begin try 
+	 msg_with ft (d.sig_preamble mo used_modules unsafe_needs);
+	 reset_renaming_tables OnlyLocal;
+	 msg_with ft (d.pp_sig (signature_of_structure struc));
+	 close_out cout;
+       with e -> 
+	 close_out cout; raise e 
+       end; 
+       info_file si)
+    si
+
+
+(*********************************************)
+(*s Part III: the actual extraction commands *)
+(*********************************************)
+
+
+let reset () =  
+  Visit.reset (); reset_tables (); reset_renaming_tables Everything
+
+let init modular = 
+  check_inside_section (); check_inside_module ();
+  set_keywords (descr ()).keywords;
+  set_modular modular;
+  reset ();
+  if modular && lang () = Scheme then error_scheme ()
+
+
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
-    \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
-    to get the saturated environment to extract. *)
+    \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when 
+    extracting to a file with the command: 
+    \verb!Extraction "file"! [qualid1] ... [qualidn]. *)
 
-let mono_extraction (f,m) qualids = 
-  check_inside_section (); 
-  check_inside_module ();
+let full_extraction f qualids = 
+  init false; 
   let rec find = function 
     | [] -> [],[]
     | q::l -> 
@@ -276,116 +380,44 @@ let mono_extraction (f,m) qualids =
 	  let mp = Nametab.locate_module (snd (qualid_of_reference q))
 	  in refs,(mp::mps)
 	with Not_found -> (Nametab.global q)::refs, mps 
-  in 	    
+  in  
   let refs,mps = find qualids in
-  let prm = {modular=false; mod_name = m; to_appear= refs} in
-  let struc = optimize_struct prm None (mono_environment refs mps) in 
-  print_structure_to_file f prm struc; 
-  Visit.reset ();
-  reset_tables ()
+  let struc = optimize_struct refs (mono_environment refs mps) in 
+  warning_axioms (); 
+  print_structure_to_file (mono_filename f) struc; 
+  reset ()
 
-let extraction_rec = mono_extraction (None,id_of_string "Main")
 
-(*s Extraction in the Coq toplevel. We display the extracted term in
-    Ocaml syntax and we use the Coq printers for globals. The
-    vernacular command is \verb!Extraction! [qualid]. *)
+(*s Simple extraction in the Coq toplevel. The vernacular command 
+    is \verb!Extraction! [qualid]. *)
 
-let extraction qid = 
-  check_inside_section (); 
-  check_inside_module ();
+let simple_extraction qid = 
+  init false; 
   try 
     let _ = Nametab.locate_module (snd (qualid_of_reference qid)) in 
-    extraction_rec [qid]
+    full_extraction None [qid]
   with Not_found -> 
     let r = Nametab.global qid in 
     if is_custom r then
       msgnl (str "User defined extraction:" ++ spc () ++ 
 	       str (find_custom r) ++ fnl ()) 
     else
-      let prm = 
-	{ modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
-      let struc = optimize_struct prm None (mono_environment [r] []) in 
+      let struc = optimize_struct [r] (mono_environment [r] []) in
       let d = get_decl_in_structure r struc in 
+      warning_axioms (); 
       print_one_decl struc (modpath_of_r r) d;
-      Visit.reset (); 
-      reset_tables () 
-
-(*s Extraction to a file (necessarily recursive). 
-    The vernacular command is 
-    \verb!Extraction "file"! [qualid1] ... [qualidn].*)
-
-let lang_suffix () = match lang () with 
-  | Ocaml -> ".ml",".mli"
-  | Haskell -> ".hs",".hi"
-  | Scheme -> ".scm",".scm"
-  | Toplevel -> assert false
-
-let filename f = 
-  let s,s' = lang_suffix () in
-  if Filename.check_suffix f s then 
-    let f' = Filename.chop_suffix f s in 
-    Some (f,f'^s'),id_of_string f' 
-  else Some (f^s,f^s'),id_of_string f
-
-let extraction_file f vl =
-  if lang () = Toplevel then error_toplevel () 
-  else mono_extraction (filename f) vl
-
-(*s Extraction of a module at the toplevel. *)
-
-let extraction_module m = 
-  check_inside_section (); 
-  check_inside_module ();
-  begin match lang () with 
-    | Toplevel -> error_toplevel ()
-    | Scheme -> error_scheme ()
-    | _ -> ()
-  end; 
-  let q = snd (qualid_of_reference m) in 
-  let mp = 
-    try Nametab.locate_module q with Not_found -> error_unknown_module q
-  in 
-  let b = is_modfile mp in 
-  let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in
-  Visit.reset ();
-  Visit.add_mp mp; 
-  let env = Global.env () in 
-  let l = List.rev (environment_until None) in 
-  let struc = 
-    List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) b m)) l
-  in
-  let struc = optimize_struct prm None struc in 
-  let struc = 
-    let bmp = base_mp mp in 
-    try [bmp, List.assoc bmp struc] with Not_found -> assert false
-  in
-  print_structure_to_file None prm struc; 
-  Visit.reset (); 
-  reset_tables ()
+      reset ()
 
 
 (*s (Recursive) Extraction of a library. The vernacular command is 
   \verb!(Recursive) Extraction Library! [M]. *) 
 
-let module_file_name m = match lang () with 
-  | Ocaml -> let f = String.uncapitalize (string_of_id m) in  f^".ml", f^".mli"
-  | Haskell -> let f = String.capitalize (string_of_id m) in f^".hs", f^".hi"
-  | _ -> assert false
-
-let dir_module_of_id m = 
-  let q = make_short_qualid m in 
-  try Nametab.full_name_module q with Not_found -> error_unknown_module q
-
 let extraction_library is_rec m =
-  check_inside_section (); 
-  check_inside_module ();  
-  begin match lang () with 
-    | Toplevel -> error_toplevel ()
-    | Scheme -> error_scheme ()
-    | _ -> () 
-  end; 
-  let dir_m = dir_module_of_id m in 
-  Visit.reset (); 
+  init true; 
+  let dir_m = 
+    let q = make_short_qualid m in 
+    try Nametab.full_name_module q with Not_found -> error_unknown_module q
+  in 
   Visit.add_mp (MPfile dir_m); 
   let env = Global.env () in	
   let l = List.rev (environment_until (Some dir_m)) in 
@@ -395,22 +427,20 @@ let extraction_library is_rec m =
     else l
   in 
   let struc = List.fold_left select [] l in 
-  let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
-  let struc = optimize_struct dummy_prm None struc in 
+  let struc = optimize_struct [] struc in 
+  warning_axioms (); 
+  record_contents_fstlev struc; 
   let rec print = function 
     | [] -> () 
     | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l 
     | (MPfile dir, sel) as e :: l -> 
 	let short_m = snd (split_dirpath dir) in
-	let f = module_file_name short_m in 
-	let prm = {modular=true;mod_name=short_m;to_appear=[]} in
-	print_structure_to_file (Some f) prm [e]; 
+	print_structure_to_file (module_filename short_m) [e]; 
 	print l 
     | _ -> assert false
   in 
   print struc; 
-  Visit.reset ();
-  reset_tables ()
+  reset ()
 
 
 
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index 18b106da2..baf79573f 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -13,8 +13,6 @@
 open Names
 open Libnames
 
-val extraction : reference -> unit
-val extraction_rec : reference list -> unit
-val extraction_file : string -> reference list -> unit
-val extraction_module : reference -> unit
+val simple_extraction : reference -> unit
+val full_extraction : string option -> reference list -> unit
 val extraction_library : bool -> identifier -> unit
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 3fa318e7e..77067b2b4 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -337,7 +337,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
       {ind_info = Standard; 
        ind_nparams = npar; 
        ind_packets = packets; 
-       ind_equiv = mib.mind_equiv };
+       ind_equiv = match mib.mind_equiv with 
+         | None -> NoEquiv 
+	 | Some kn -> Equiv kn
+      };
     (* Second pass: we extract constructors *)
     for i = 0 to mib.mind_ntypes - 1 do
       let p = packets.(i) in 
@@ -421,7 +424,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     let i = {ind_info = ind_info; 
 	     ind_nparams = npar; 
 	     ind_packets = packets; 
-	     ind_equiv = mib.mind_equiv}
+	     ind_equiv = match mib.mind_equiv with 
+	       | None -> NoEquiv
+	       | Some kn -> Equiv kn }
     in
     add_ind kn mib i; 
     i
@@ -828,18 +833,18 @@ let extract_constant env kn cb =
     | None -> (* A logical axiom is risky, an informative one is fatal. *) 
         (match flag_of_type env typ with
 	   | (Info,TypeScheme) -> 
-	       if not (is_custom r) then warning_info_ax r; 
+	       if not (is_custom r) then add_info_axiom r; 
 	       let n = type_scheme_nb_args env typ in 
 	       let ids = iterate (fun l -> anonymous::l) n [] in 
 	       Dtype (r, ids, Taxiom) 
            | (Info,Default) -> 
-	       if not (is_custom r) then warning_info_ax r; 
+	       if not (is_custom r) then add_info_axiom r; 
 	       let t = snd (record_constant_type env kn (Some typ)) in 
 	       Dterm (r, MLaxiom, type_expunge env t) 
            | (Logic,TypeScheme) -> 
-	       warning_log_ax r; Dtype (r, [], Tdummy Ktype)
+	       add_log_axiom r; Dtype (r, [], Tdummy Ktype)
 	   | (Logic,Default) -> 
-	       warning_log_ax r; Dterm (r, MLdummy, Tdummy Kother))
+	       add_log_axiom r; Dterm (r, MLdummy, Tdummy Kother))
     | Some body ->
 	(match flag_of_type env typ with
 	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother)
@@ -880,24 +885,6 @@ let extract_inductive env kn =
       ind.ind_packets
   in { ind with ind_packets = packets }
 
-(*s From a global reference to a ML declaration. *)
-
-let extract_declaration env r = match r with
-  | ConstRef kn -> extract_constant env kn (Environ.lookup_constant kn env)
-  | IndRef (kn,_) -> Dind (kn, extract_inductive env kn)
-  | ConstructRef ((kn,_),_) -> Dind (kn, extract_inductive env kn)
-  | VarRef kn -> assert false
-
-(*s Without doing complete extraction, just guess what a constant would be. *) 
-
-type kind = Logical | Term | Type 
-    
-let constant_kind env cb = 
-  match flag_of_type env (Typeops.type_of_constant_type env cb.const_type) with 
-    | (Logic,_) -> Logical
-    | (Info,TypeScheme) -> Type
-    | (Info,Default) -> Term
-
 (*s Is a [ml_decl] logical ? *) 
 
 let logical_decl = function 
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index b26a577e2..cb0600d05 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -26,16 +26,6 @@ val extract_fixpoint :
 
 val extract_inductive : env -> kernel_name -> ml_ind
 
-(*s ML declaration corresponding to a Coq reference. *)
-
-val extract_declaration : env -> global_reference -> ml_decl
-
-(*s Without doing complete extraction, just guess what a constant would be. *) 
-
-type kind = Logical | Term | Type 
-
-val constant_kind : env -> constant_body -> kind
-
 (*s Is a [ml_decl] or a [ml_spec] logical ? *) 
 
 val logical_decl : ml_decl -> bool
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 13b29c7b5..cb95808d6 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -31,19 +31,18 @@ VERNAC ARGUMENT EXTEND language
 | [ "Ocaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
 | [ "Scheme" ] -> [ Scheme ]
-| [ "Toplevel" ] -> [ Toplevel ]
 END
 
 (* Extraction commands *)
 
 VERNAC COMMAND EXTEND Extraction
 (* Extraction in the Coq toplevel *)
-| [ "Extraction" global(x) ] -> [ extraction x ]
-| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ extraction_rec l ]
+| [ "Extraction" global(x) ] -> [ simple_extraction x ]
+| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ]
 
 (* Monolithic extraction to a file *)
 | [ "Extraction" string(f) ne_global_list(l) ] 
-  -> [ extraction_file f l ]
+  -> [ full_extraction (Some f) l ]
 END
 
 (* Modular extraction (one Coq library = one ML module) *)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 1e26f6c75..f55bc6feb 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -18,7 +18,7 @@ open Libnames
 open Table
 open Miniml
 open Mlutil
-open Ocaml
+open Common
 
 (*s Haskell renaming issues. *)
 
@@ -30,22 +30,22 @@ let keywords =
     "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
   Idset.empty
 
-let preamble prm used_modules (mldummy,tdummy,tunknown) magic =
+let preamble mod_name used_modules usf =
   let pp_mp = function 
     | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
     | _ -> assert false 
   in  
-  (if not magic then mt () 
+  (if not usf.magic then mt () 
    else
      str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++
      str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n")
   ++
-  str "module " ++ pr_upper_id prm.mod_name ++ str " where" ++ fnl () 
+  str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl () 
   ++ fnl() ++ 
   str "import qualified Prelude" ++ fnl() ++
   prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules
   ++ fnl () ++
-  (if not magic then mt () 
+  (if not usf.magic then mt () 
    else str "\
 #ifdef __GLASGOW_HASKELL__
 import qualified GHC.Base
@@ -58,13 +58,11 @@ unsafeCoerce = IOExts.unsafeCoerce
   ++
   fnl() ++ fnl() 
   ++
-  (if not mldummy then mt () 
+  (if not usf.mldummy then mt () 
    else
      str "__ = Prelude.error \"Logical or arity value used\"" 
      ++ fnl () ++ fnl())
 
-let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO" 
-
 let pp_abst = function
   | [] -> (mt ())
   | l  -> (str "\\" ++
@@ -73,17 +71,11 @@ let pp_abst = function
 
 let pr_lower_id id = pr_id (lowercase_id id)
 
-(*s The pretty-printing functor. *)
-
-module Make = functor(P : Mlpp_param) -> struct
-
-let local_mpl = ref ([] : module_path list)
+(*s The pretty-printer for haskell syntax *)
 
-let pp_global r = 
+let pp_global k r = 
   if is_inline_custom r then str (find_custom r) 
-  else P.pp_global !local_mpl r
-
-let empty_env () = [], P.globals()
+  else str (Common.pp_global k r)
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
@@ -96,13 +88,14 @@ let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ -> assert false 
     | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
-    | Tglob (r,[]) -> pp_global r	
+    | Tglob (r,[]) -> pp_global Type r	
     | Tglob (r,l) -> 
 	if r = IndRef (kn_sig,0) then 
 	  pp_type true vl (List.hd l)
 	else 
 	  pp_par par 
-	    (pp_global r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l)
+	    (pp_global Type r ++ spc () ++ 
+	     prlist_with_sep spc (pp_type true vl) l)
     | Tarr (t1,t2) ->
 	pp_par par 
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
@@ -151,15 +144,15 @@ let rec pp_expr par env args =
 		    spc () ++ str "in") ++
 		 spc () ++ hov 0 pp_a2)))
     | MLglob r -> 
-	apply (pp_global r)
+	apply (pp_global Term r)
     | MLcons (_,r,[]) ->
-	assert (args=[]); pp_global r
+	assert (args=[]); pp_global Cons r
     | MLcons (_,r,[a]) ->
 	assert (args=[]);
-	pp_par par (pp_global r ++ spc () ++ pp_expr true env [] a)
+	pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a)
     | MLcons (_,r,args') ->
 	assert (args=[]);
-	pp_par par (pp_global r ++ spc () ++ 
+	pp_par par (pp_global Cons r ++ spc () ++ 
 		    prlist_with_sep spc (pp_expr true env []) args')
     | MLcase ((_,factors),t, pv) ->
       	apply (pp_par par' 
@@ -181,7 +174,7 @@ and pp_pat env factors pv =
   let pp_one_pat (name,ids,t) =
     let ids,env' = push_vars (List.rev ids) env in
     let par = expr_needs_par t in
-    hov 2 (pp_global name ++
+    hov 2 (pp_global Cons name ++
 	   (match ids with 
 	      | [] -> mt ()
 	      | _  -> (str " " ++ 
@@ -234,7 +227,7 @@ let pp_logical_ind packet =
 let pp_singleton kn packet = 
   let l = rename_tvars keywords packet.ip_vars in 
   let l' = List.rev l in 
-  hov 2 (str "type " ++ pp_global (IndRef (kn,0)) ++ spc () ++ 
+  hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++ 
 	 prlist_with_sep spc pr_id l ++
 	 (if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++
 	 pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
@@ -244,7 +237,7 @@ let pp_singleton kn packet =
 let pp_one_ind ip pl cv =
   let pl = rename_tvars keywords pl in
   let pp_constructor (r,l) =
-    (pp_global r ++
+    (pp_global Cons r ++
      match l with
        | [] -> (mt ()) 
        | _  -> (str " " ++
@@ -252,7 +245,7 @@ let pp_one_ind ip pl cv =
 		  (fun () -> (str " ")) (pp_type true pl) l))
   in
   str (if Array.length cv = 0 then "type " else "data ") ++ 
-  pp_global (IndRef ip) ++ str " " ++
+  pp_global Type (IndRef ip) ++ str " " ++
   prlist_with_sep (fun () -> str " ") pr_lower_id pl ++
   (if pl = [] then mt () else str " ") ++
   if Array.length cv = 0 then str "= () -- empty inductive"
@@ -280,9 +273,7 @@ let rec pp_ind first kn i ind =
 
 let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
 
-let pp_decl mpl = 
-  local_mpl := mpl;
-  function
+let pp_decl = function
   | Dind (kn,i) when i.ind_info = Singleton -> 
       pp_singleton kn i.ind_packets.(0) ++ fnl ()
   | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i)
@@ -299,38 +290,49 @@ let pp_decl mpl =
 	    if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
 	    else str "=" ++ spc () ++ pp_type false l t
 	in 
-	hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl ()
+	hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 ()
   | Dfix (rv, defs, typs) ->
       let max = Array.length rv in 
       let rec iter i = 
 	if i = max then mt () 
 	else
-	  let e = pp_global rv.(i) in 
+	  let e = pp_global Term rv.(i) in 
 	  e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () 
-	  ++ pp_function (empty_env ()) e defs.(i) ++ fnl () ++ fnl () 
+	  ++ pp_function (empty_env ()) e defs.(i) ++ fnl2 ()
 	  ++ iter (i+1)
       in iter 0
   | Dterm (r, a, t) ->
       if is_inline_custom r then mt () 
       else 
-	let e = pp_global r in 
+	let e = pp_global Term r in 
 	e ++ str " :: " ++ pp_type false [] t ++ fnl () ++
 	  if is_custom r then 	
-	    hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl() ++ fnl ())
+	    hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ())
 	  else 
-	    hov 0 (pp_function (empty_env ()) e a ++ fnl () ++ fnl ())
+	    hov 0 (pp_function (empty_env ()) e a ++ fnl2 ())
 
-let pp_structure_elem mpl = function 
-  | (l,SEdecl d) -> pp_decl mpl d
+let pp_structure_elem = function 
+  | (l,SEdecl d) -> pp_decl d
   | (l,SEmodule m) -> 
       failwith "TODO: Haskell extraction of modules not implemented yet"
   | (l,SEmodtype m) -> 
       failwith "TODO: Haskell extraction of modules not implemented yet"
 
 let pp_struct = 
-  prlist (fun (mp,sel) -> prlist (pp_structure_elem [mp]) sel)
-
-let pp_signature s = failwith "TODO"
-
-end
-
+  let pp_sel (mp,sel) = 
+    push_visible mp; let p = prlist pp_structure_elem sel in pop_visible (); p
+  in 
+  prlist pp_sel 
+
+
+let haskell_descr = {
+  keywords = keywords;  
+  file_suffix = ".hs"; 
+  capital_file = true;  
+  preamble = preamble; 
+  pp_struct = pp_struct; 
+  sig_suffix = None;
+  sig_preamble = (fun _ _ _ -> mt ()); 
+  pp_sig = (fun _ -> mt ());
+  pp_decl = pp_decl; 
+}
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 430ec1fce..1b5dbc711 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -8,13 +8,5 @@
 
 (*i $Id$ i*)
 
-open Pp
-open Names
-open Miniml
+val haskell_descr : Miniml.language_descr
 
-val keywords : Idset.t
-
-val preamble : 
-  extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
-
-module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index d728a8a14..ef963cc90 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -78,11 +78,16 @@ type ml_ind_packet = {
 
 (* [ip_nparams] contains the number of parameters. *)
 
+type equiv = 
+  | NoEquiv
+  | Equiv of kernel_name 
+  | RenEquiv of string
+
 type ml_ind = {
   ind_info : inductive_info;
   ind_nparams : int; 	       
   ind_packets : ml_ind_packet array;
-  ind_equiv : kernel_name option
+  ind_equiv : equiv
 }
 
 (*s ML terms. *)
@@ -151,24 +156,28 @@ type ml_structure = (module_path * ml_module_structure) list
 
 type ml_signature = (module_path * ml_module_sig) list
 
-(*s Pretty-printing of MiniML in a given concrete syntax is parameterized
-    by a function [pp_global] that pretty-prints global references. 
-    The resulting pretty-printer is a module of type [Mlpp] providing
-    functions to print types, terms and declarations. *)
-
-module type Mlpp_param = sig
-  val globals : unit -> Idset.t
-  val pp_global : module_path list -> global_reference -> std_ppcmds
-  val pp_module : module_path list -> module_path -> std_ppcmds
-end
-
-module type Mlpp = sig
-  val pp_decl : module_path list -> ml_decl -> std_ppcmds
-  val pp_struct : ml_structure -> std_ppcmds
-  val pp_signature : ml_signature -> std_ppcmds
-end
-
-type extraction_params =  
-  { modular : bool; 
-    mod_name : identifier; 
-    to_appear : global_reference list }
+type unsafe_needs = {
+  mldummy : bool; 
+  tdummy : bool; 
+  tunknown : bool; 
+  magic : bool
+}
+
+type language_descr = {
+  keywords : Idset.t; 
+
+  (* Concerning the source file *)
+  file_suffix : string;  
+  capital_file : bool; (* should we capitalize filenames ? *)
+  preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; 
+  pp_struct : ml_structure -> std_ppcmds; 
+
+  (* Concerning a possible interface file *)
+  sig_suffix : string option; 
+  sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
+  pp_sig : ml_signature -> std_ppcmds; 
+
+  (* for an isolated declaration print *)
+  pp_decl : ml_decl -> std_ppcmds; 
+
+}  
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 87713e4d5..760f76c9a 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -86,56 +86,6 @@ let rec replicate_msid meb mtb = match meb,mtb with
       if msig' == msig then MTBsig (msid, msig) else MTBsig (msid, msig')
   | _ -> mtb
 
-
-(*S More functions concerning [module_path]. *)
-
-let rec mp_length = function
-  | MPdot (mp, _) -> 1 + (mp_length mp)
-  | _ -> 1
-
-let rec prefixes_mp mp = match mp with 
-  | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
-  | _ -> MPset.singleton mp 
-
-let rec common_prefix prefixes_mp1 mp2 = 
-  if MPset.mem mp2 prefixes_mp1 then mp2 
-  else match mp2 with 
-    | MPdot (mp,_) -> common_prefix prefixes_mp1 mp 
-    | _ -> raise Not_found
-
-let common_prefix_from_list mp0 mpl = 
-  let prefixes_mp0 = prefixes_mp mp0 in 
-  let rec f = function 
-    | [] -> raise Not_found
-    | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l
-  in f mpl
-
-let rec modfile_of_mp mp = match mp with 
-  | MPfile _ -> mp
-  | MPdot (mp,_) -> modfile_of_mp mp 
-  | _ -> raise Not_found
-
-let rec parse_labels ll = function 
-  | MPdot (mp,l) -> parse_labels (l::ll) mp 
-  | mp -> mp,ll
-
-let labels_of_mp mp = parse_labels [] mp 
-
-let labels_of_ref r = 
- let mp,_,l =
-  match r with
-     ConstRef con -> repr_con con
-   | IndRef (kn,_)
-   | ConstructRef ((kn,_),_) -> repr_kn kn
-   | VarRef _ -> assert false
- in
-  parse_labels [l] mp
-
-let rec add_labels_mp mp = function 
-  | [] -> mp 
-  | l :: ll -> add_labels_mp (MPdot (mp,l)) ll
-
-
 (*S Functions upon ML modules. *)
 
 (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a 
@@ -200,7 +150,9 @@ let ind_iter_references do_term do_cons do_type kn ind =
   let packet_iter ip p = 
     do_type (IndRef ip); 
     if lang () = Ocaml then 
-      option_iter (fun kne -> do_type (IndRef (kne,snd ip))) ind.ind_equiv; 
+      (match ind.ind_equiv with 
+	 | Equiv kne -> do_type (IndRef (kne, snd ip)); 
+	 | _ -> ()); 
     Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types 
   in
   if lang () = Ocaml then record_iter_references do_term ind.ind_info; 
@@ -228,13 +180,13 @@ let struct_iter_references do_term do_cons do_type =
 
 (*s Get all references used in one [ml_structure], either in [list] or [set]. *)
 
-type 'a updown = { mutable up : 'a ; mutable down : 'a }
+type 'a kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a }
 
 let struct_get_references empty add struc = 
-  let o = { up = empty ; down = empty } in 
-  let do_term r = o.down <- add r o.down in
-  let do_cons r = o.up <- add r o.up in 
-  let do_type = if lang () = Haskell then do_cons else do_term in 
+  let o = { typ = empty ; trm = empty ; cons = empty } in 
+  let do_type r = o.typ <- add r o.typ in 
+  let do_term r = o.trm <- add r o.trm in
+  let do_cons r = o.cons <- add r o.cons in 
   struct_iter_references do_term do_cons do_type struc; o
 
 let struct_get_references_set = struct_get_references Refset.empty Refset.add
@@ -251,7 +203,9 @@ end
 
 let struct_get_references_list struc = 
   let o = struct_get_references Orefset.empty Orefset.add struc in 
-  { up = Orefset.list o.up; down = Orefset.list o.down }
+  { typ = Orefset.list o.typ; 
+    trm = Orefset.list o.trm; 
+    cons = Orefset.list o.cons }
 
 
 (*s Searching occurrences of a particular term (no lifting done). *)
@@ -363,38 +317,40 @@ let dfix_to_mlfix rv av i =
   let c = Array.map (subst 0) av 
   in MLfix(i, ids, c)
 
-let rec optim prm s = function
+let rec optim to_appear s = function
   | [] -> []
   | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l ->
-      if List.mem r prm.to_appear then d :: (optim prm s l) else optim prm s l
+      if List.mem r to_appear 
+      then d :: (optim to_appear s l) 
+      else optim to_appear s l
   | Dterm (r,t,typ) :: l ->
       let t = normalize (ast_glob_subst !s t) in 
       let i = inline r t in 
       if i then s := Refmap.add r t !s; 
-      if not i || prm.modular || List.mem r prm.to_appear 
+      if not i || modular () || List.mem r to_appear 
       then 
 	let d = match optimize_fix t with 
 	  | MLfix (0, _, [|c|]) -> 
 	      Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|])
 	  | t -> Dterm (r, t, typ)
-	in d :: (optim prm s l)
-      else optim prm s l
-  | d :: l -> d :: (optim prm s l)
+	in d :: (optim to_appear s l)
+      else optim to_appear s l
+  | d :: l -> d :: (optim to_appear s l)
 
-let rec optim_se top prm s = function 
+let rec optim_se top to_appear s = function 
   | [] -> [] 
   | (l,SEdecl (Dterm (r,a,t))) :: lse -> 
       let a = normalize (ast_glob_subst !s a) in 
       let i = inline r a in 
       if i then s := Refmap.add r a !s; 
-      if top && i && not prm.modular && not (List.mem r prm.to_appear)
-      then optim_se top prm s lse
+      if top && i && not (modular ()) && not (List.mem r to_appear)
+      then optim_se top to_appear s lse
       else 
 	let d = match optimize_fix a with 
 	  | MLfix (0, _, [|c|]) -> 
 	      Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|])
 	  | a -> Dterm (r, a, t)
-	in (l,SEdecl d) :: (optim_se top prm s lse)
+	in (l,SEdecl d) :: (optim_se top to_appear s lse)
   | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> 
       let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in 
       let all = ref true in 
@@ -405,22 +361,22 @@ let rec optim_se top prm s = function
 	then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s
 	else all := false
       done; 
-      if !all && top && not prm.modular 
-	&& (array_for_all (fun r -> not (List.mem r prm.to_appear)) rv)  
-      then optim_se top prm s lse
-      else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top prm s lse)
+      if !all && top && not (modular ())
+	&& (array_for_all (fun r -> not (List.mem r to_appear)) rv)  
+      then optim_se top to_appear s lse
+      else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
   | (l,SEmodule m) :: lse -> 
-      let m = { m with ml_mod_expr = optim_me prm s m.ml_mod_expr}
-      in (l,SEmodule m) :: (optim_se top prm s lse)
-  | se :: lse -> se :: (optim_se top prm s lse) 
+      let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr}
+      in (l,SEmodule m) :: (optim_se top to_appear s lse)
+  | se :: lse -> se :: (optim_se top to_appear s lse) 
 
-and optim_me prm s = function 
-  | MEstruct (msid, lse) -> MEstruct (msid, optim_se false prm s lse)
+and optim_me to_appear s = function 
+  | MEstruct (msid, lse) -> MEstruct (msid, optim_se false to_appear s lse)
   | MEident mp as me -> me
-  | MEapply (me, me') -> MEapply (optim_me prm s me, optim_me prm s me')
-  | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me prm s me)
+  | MEapply (me, me') -> 
+      MEapply (optim_me to_appear s me, optim_me to_appear s me')
+  | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me)
 
-let optimize_struct prm before struc = 
+let optimize_struct to_appear struc = 
   let subst = ref (Refmap.empty : ml_ast Refmap.t) in 
-  option_iter (fun l -> ignore (optim prm subst l)) before; 
-  List.map (fun (mp,lse) -> (mp, optim_se true prm subst lse)) struc
+  List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index 46c7dbc3f..c89590daa 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -33,14 +33,6 @@ val subst_msb : substitution -> module_structure_body -> module_structure_body
 
 val replicate_msid : module_expr_body -> module_type_body -> module_type_body
 
-(*s More utilities concerning [module_path]. *)
-
-val mp_length : module_path -> int
-val prefixes_mp : module_path -> MPset.t
-val modfile_of_mp : module_path -> module_path
-val common_prefix_from_list : module_path -> module_path list -> module_path
-val add_labels_mp : module_path -> label list -> module_path
-
 (*s Functions upon ML modules. *)
 
 val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
@@ -52,10 +44,10 @@ val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit
 val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit
 val struct_iter_references : do_ref -> do_ref -> do_ref -> ml_structure -> unit
 
-type 'a updown = { mutable up : 'a ; mutable down : 'a }
+type 'a kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a }
 
-val struct_get_references_set : ml_structure -> Refset.t updown
-val struct_get_references_list : ml_structure -> global_reference list updown
+val struct_get_references_set : ml_structure -> Refset.t kinds
+val struct_get_references_list : ml_structure -> global_reference list kinds
 
 val signature_of_structure : ml_structure -> ml_signature
 
@@ -65,7 +57,7 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
    all beta redexes (when the argument does not occur, it is just
    thrown away; when it occurs exactly once it is substituted; otherwise
    a let-in redex is created for clarity) and iota redexes, plus some other
-   optimizations. *)
+   optimizations. The first argument is the list of objects we want to appear.
+*)
 
-val optimize_struct : 
-  extraction_params -> ml_decl list option -> ml_structure -> ml_structure
+val optimize_struct : global_reference list -> ml_structure -> ml_structure
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 600e6ebca..7548c1487 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -19,10 +19,7 @@ open Table
 open Miniml
 open Mlutil
 open Modutil
-
-(*s Some utility functions. *)
-
-let pp_par par st = if par then str "(" ++ st ++ str ")" else st
+open Common
 
 let pp_tvar id = 
   let s = string_of_id id in 
@@ -52,70 +49,12 @@ let pp_abst = function
       str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++ 
       str " ->" ++ spc ()
 
-let pp_apply st par args = match args with
-  | [] -> st
-  | _  -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
-
-let pr_binding = function
-  | [] -> mt ()
-  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
-
-let space_if = function true -> str " " | false -> mt ()
-
-let sec_space_if = function true -> spc () | false -> mt ()
-
-let fnl2 () = fnl () ++ fnl () 
-
 let pp_parameters l = 
   (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
 
 let pp_string_parameters l = 
   (pp_boxed_tuple str l ++ space_if (l<>[])) 
 
-(*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 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))
-
-(* [pr_upper_id id] makes 2 String.copy lesser than [pr_id (uppercase_id id)] *)
-let pr_upper_id id = str (String.capitalize (string_of_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 == dummy_name ->
-      (* we don't rename dummy binders *)
-      let (idl', avoid') = rename_vars avoid idl in
-      (id :: idl', avoid')
-  | id :: idl ->
-      let (idl, avoid) = rename_vars avoid idl in
-      let id = rename_id (lowercase_id id) avoid in
-      (id :: idl, Idset.add id avoid)
-
-let rename_tvars avoid l = 
-  let rec rename avoid = function 
-    | [] -> [],avoid 
-    | id :: idl -> 
-	let id = rename_id (lowercase_id id) avoid in 
-	let idl, avoid = rename (Idset.add id avoid) idl in 
-	(id :: idl, avoid) in
-  fst (rename avoid l)
-
-let push_vars ids (db,avoid) =
-  let ids',avoid' = rename_vars avoid ids in
-  ids', (ids' @ db, avoid')
-
-let get_db_name n (db,_) = 
-  let id = List.nth db (pred n) in 
-  if id = dummy_name then id_of_string "__" else id
-
 (*s Ocaml renaming issues. *)
 
 let keywords =     
@@ -130,7 +69,7 @@ let keywords =
     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] 
   Idset.empty
 
-let preamble _ used_modules (mldummy,tdummy,tunknown) _ = 
+let preamble _ used_modules usf = 
   let pp_mp = function 
     | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
     | _ -> assert false 
@@ -139,15 +78,15 @@ let preamble _ used_modules (mldummy,tdummy,tunknown) _ =
   ++ 
   (if used_modules = [] then mt () else fnl ())
   ++
-  (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() else mt()) 
+  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl() else mt())
   ++
-  (if mldummy then 
+  (if usf.mldummy then 
      str "let __ = let rec f _ = Obj.repr f in Obj.repr f" ++ fnl ()
    else mt ()) 
   ++ 
-  (if tdummy || tunknown || mldummy then fnl () else mt ())
+  (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ())
 
-let preamble_sig _ used_modules (_,tdummy,tunknown) = 
+let sig_preamble _ used_modules usf =
   let pp_mp = function 
     | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
     | _ -> assert false 
@@ -156,18 +95,16 @@ let preamble_sig _ used_modules (_,tdummy,tunknown) =
   ++ 
   (if used_modules = [] then mt () else fnl ())
   ++
-  (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() ++ fnl () 
+  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl() ++ fnl () 
    else mt()) 
 
-(*s The pretty-printing functor. *)
-
-module Make = functor(P : Mlpp_param) -> struct
+(*s The pretty-printer for Ocaml syntax*)
 
-let local_mpl = ref ([] : module_path list)
-
-let pp_global r = 
+let pp_global k r = 
   if is_inline_custom r then str (find_custom r) 
-  else P.pp_global !local_mpl  r
+  else str (Common.pp_global k r)
+
+let pp_modname mp = str (Common.pp_module mp)
 
 let is_infix r = 
   is_inline_custom r && 
@@ -177,8 +114,6 @@ let get_infix r =
   let s = find_custom r in 
   String.sub s 1 (String.length s - 2)
 
-let empty_env () = [], P.globals ()
-
 exception NoRecord
 
 let find_projections = function Record l -> l | _ -> raise NoRecord
@@ -199,12 +134,12 @@ let rec pp_type par vl t =
 	pp_par par 
 	  (pp_rec true a1 ++ spc () ++ str (get_infix r) ++ spc () ++ 
 	   pp_rec true a2)
-    | Tglob (r,[]) -> pp_global r
+    | Tglob (r,[]) -> pp_global Type r
     | Tglob (r,l) -> 
 	if r = IndRef (kn_sig,0) then 
 	  pp_tuple_light pp_rec l
 	else 
-	  pp_tuple_light pp_rec l ++ spc () ++ pp_global r
+	  pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
     | Tarr (t1,t2) ->
 	pp_par par 
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
@@ -256,18 +191,18 @@ let rec pp_expr par env args =
 	(try 
 	   let args = list_skipn (projection_arity r) args in 
 	   let record = List.hd args in 
-	   pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
-	 with _ -> apply (pp_global r))
+	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
+	 with _ -> apply (pp_global Term r))
     | MLcons (Coinductive,r,[]) ->
 	assert (args=[]);
-	pp_par par (str "lazy " ++ pp_global r)
+	pp_par par (str "lazy " ++ pp_global Cons r)
     | MLcons (Coinductive,r,args') -> 
 	assert (args=[]);
 	let tuple = pp_tuple (pp_expr true env []) args' in 
-	pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")")
+	pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")")
     | MLcons (_,r,[]) -> 
 	assert (args=[]);
-	pp_global r
+	pp_global Cons r
     | MLcons (Record projs, r, args') -> 
 	assert (args=[]); 
 	pp_record_pat (projs, List.map (pp_expr true env []) args')
@@ -279,7 +214,7 @@ let rec pp_expr par env args =
     | MLcons (_,r,args') -> 
 	assert (args=[]);
 	let tuple = pp_tuple (pp_expr true env []) args' in 
-	pp_par par (pp_global r ++ spc () ++ tuple)
+	pp_par par (pp_global Cons r ++ spc () ++ tuple)
     | MLcase ((i,factors), t, pv) ->
 	let expr = if i = Coinductive then 
 	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
@@ -293,7 +228,7 @@ let rec pp_expr par env args =
 	   match c with 
 	     | MLrel i when i <= n -> 
 		 apply (pp_par par' (pp_expr true env [] t ++ str "." ++ 
-				     pp_global (List.nth projs (n-i)))) 
+				     pp_global Term (List.nth projs (n-i))))
 	     | MLapp (MLrel i, a) when i <= n -> 
 		 if List.exists (ast_occurs_itvl 1 n) a 
 		 then raise NoRecord
@@ -301,7 +236,7 @@ let rec pp_expr par env args =
 		   let ids,env' = push_vars (List.rev ids) env in
 		   (pp_apply 
 		      (pp_expr true env [] t ++ str "." ++ 
-		       pp_global (List.nth projs (n-i)))
+		       pp_global Term (List.nth projs (n-i)))
 		      par ((List.map (pp_expr true env' []) a) @ args))
 	     | _ -> raise NoRecord
 	 with NoRecord -> 
@@ -336,7 +271,7 @@ let rec pp_expr par env args =
 and pp_record_pat (projs, args) =
    str "{ " ++
    prlist_with_sep (fun () -> str ";" ++ spc ()) 
-     (fun (r,a) -> pp_global r ++ str " =" ++ spc () ++ a)
+     (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a)
      (List.combine projs args) ++
    str " }"
 
@@ -350,8 +285,8 @@ and pp_one_pat env i (r,ids,t) =
     (match List.rev ids with 
       | [i1;i2] when is_infix r -> 
 	  pr_id i1 ++ str " " ++ str (get_infix r) ++ str " " ++ pr_id i2
-      | [] -> pp_global r
-      | ids -> pp_global r ++ str " " ++ pp_boxed_tuple pr_id ids), 
+      | [] -> pp_global Cons r
+      | ids -> pp_global Cons r ++ str " " ++ pp_boxed_tuple pr_id ids), 
     expr
   
 and pp_pat env (info,factors) pv = 
@@ -369,23 +304,23 @@ and pp_pat env (info,factors) pv =
 	 let t = ast_lift (-List.length ids) t in 
 	 hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t)
 
-and pp_function env f t =
+and pp_function env t =
   let bl,t' = collect_lams t in
   let bl,env' = push_vars bl env in
   match t' with 
     | MLcase(i,MLrel 1,pv) when fst i=Standard -> 
 	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then 
-	  (f ++ pr_binding (List.rev (List.tl bl)) ++
-       	     str " = function" ++ fnl () ++
-	     v 0 (str "  | " ++ pp_pat env' i pv))
+	  pr_binding (List.rev (List.tl bl)) ++
+       	  str " = function" ++ fnl () ++
+	  v 0 (str "  | " ++ pp_pat env' i pv)
 	else
-          (f ++ pr_binding (List.rev bl) ++ 
-             str " = match " ++
-	     pr_id (List.hd bl) ++ str " with" ++ fnl () ++
-	     v 0 (str "  | " ++ pp_pat env' i pv))
-    | _ -> (f ++ pr_binding (List.rev bl) ++
-	      str " =" ++ fnl () ++ str "  " ++
-	      hov 2 (pp_expr false env' [] t'))
+          pr_binding (List.rev bl) ++ 
+          str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
+	  v 0 (str "  | " ++ pp_pat env' i pv)
+    | _ -> 
+          pr_binding (List.rev bl) ++
+	  str " =" ++ fnl () ++ str "  " ++
+	  hov 2 (pp_expr false env' [] t')
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)
@@ -395,54 +330,57 @@ and pp_fix par env i (ids,bl) args =
     (v 0 (str "let rec " ++
 	  prvect_with_sep
       	    (fun () -> fnl () ++ str "and ")
-	    (fun (fi,ti) -> pp_function env (pr_id fi) ti)
+	    (fun (fi,ti) -> pr_id fi ++ pp_function env ti)
 	    (array_map2 (fun id b -> (id,b)) ids bl) ++
 	  fnl () ++
 	  hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
 
 let pp_val e typ = 
-  str "(** val " ++ e ++ str " : " ++ pp_type false [] typ ++ 
-  str " **)"  ++ fnl2 ()
+  hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++ 
+  str " **)")  ++ fnl2 ()
 
 (*s Pretty-printing of [Dfix] *)
 
-let rec pp_Dfix init i ((rv,c,t) as fix) = 
-  if i >= Array.length rv then mt () 
-  else 
-    if is_inline_custom rv.(i) then pp_Dfix init (i+1) fix
+let pp_Dfix (rv,c,t) = 
+  let names = Array.map 
+    (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv
+  in 
+  let rec pp sep letand i = 
+    if i >= Array.length rv then mt ()
+    else if is_inline_custom rv.(i) then pp sep letand (i+1)
     else 
-      let e = pp_global rv.(i) in
-      (if init then mt () else fnl2 ()) ++
-      pp_val e t.(i) ++
-      str (if init then "let rec " else "and ") ++
-      (if is_custom rv.(i) then e ++ str " = " ++ str (find_custom rv.(i))
-       else pp_function (empty_env ()) e c.(i)) ++
-      pp_Dfix false (i+1) fix 
-	
+      let def = 
+	if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
+	else pp_function (empty_env ()) c.(i)
+      in 
+      sep () ++ pp_val names.(i) t.(i) ++ 
+      str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1) 
+  in pp mt "let rec " 0
+
 (*s Pretty-printing of inductive types declaration. *)
 
-let pp_equiv param_list = function 
-  | None -> mt ()
-  | Some ip_equiv -> 
-      str " = " ++ pp_parameters param_list ++ pp_global (IndRef ip_equiv)
+let pp_equiv param_list name = function 
+  | NoEquiv, _ -> mt ()
+  | Equiv kn, i -> 
+      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (kn,i))
+  | RenEquiv ren, _  ->
+      str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
 
 let pp_comment s = str "(* " ++ s ++ str " *)"
 
-let pp_one_ind prefix ip ip_equiv pl cv =
+let pp_one_ind prefix ip_equiv pl name cnames ctyps =
   let pl = rename_tvars keywords pl in
-  let pp_constructor (r,l) =
-    hov 2 (str "  | " ++ pp_global r ++
-	   match l with
-	     | [] -> mt () 
-	     | _  -> (str " of " ++ 
-		      prlist_with_sep 
-			(fun () -> spc () ++ str "* ") (pp_type true pl) l))
+  let pp_constructor i typs =
+    (if i=0 then mt () else fnl ()) ++ 
+    hov 5 (str "  | " ++ cnames.(i) ++
+	   (if typs = [] then mt () else str " of ") ++
+	   prlist_with_sep 
+	    (fun () -> spc () ++ str "* ") (pp_type true pl) typs)
   in
-  pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++
-  pp_equiv pl ip_equiv ++ str " =" ++
-  if Array.length cv = 0 then str " unit (* empty inductive *)" 
-  else fnl () ++ v 0 (prvect_with_sep fnl pp_constructor
-			(Array.mapi (fun i c -> ConstructRef (ip,i+1), c) cv))
+  pp_parameters pl ++ str prefix ++ name ++
+  pp_equiv pl name ip_equiv ++ str " =" ++
+  if Array.length ctyps = 0 then str " unit (* empty inductive *)" 
+  else fnl () ++ v 0 (prvecti pp_constructor ctyps)
 
 let pp_logical_ind packet = 
   pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ 
@@ -452,38 +390,51 @@ let pp_logical_ind packet =
   fnl ()
 
 let pp_singleton kn packet = 
+  let name = pp_global Type (IndRef (kn,0)) in 
   let l = rename_tvars keywords packet.ip_vars in 
-  hov 2 (str "type " ++ pp_parameters l ++
-	 pp_global (IndRef (kn,0)) ++ str " =" ++ spc () ++
+  hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
 	 pp_comment (str "singleton inductive, whose constructor was " ++ 
 		     pr_id packet.ip_consnames.(0)))
 
 let pp_record kn projs ip_equiv packet = 
-  let l = List.combine projs packet.ip_types.(0) in 
+  let name = pp_global Type (IndRef (kn,0)) in
+  let projnames = List.map (pp_global Term) projs in 
+  let l = List.combine projnames packet.ip_types.(0) in 
   let pl = rename_tvars keywords packet.ip_vars in 
-  str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ 
-  pp_equiv pl ip_equiv ++ str " = { "++
+  str "type " ++ pp_parameters pl ++ name ++ 
+  pp_equiv pl name ip_equiv ++ str " = { "++
   hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) 
-	   (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l) 
+	   (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l) 
   ++ str " }"
 
-let pp_coind ip pl = 
-  let r = IndRef ip in 
+let pp_coind pl name = 
   let pl = rename_tvars keywords pl in
-  pp_parameters pl ++ pp_global r ++ str " = " ++ 
-  pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t" ++ 
+  pp_parameters pl ++ name ++ str " = " ++ 
+  pp_parameters pl ++ str "__" ++ name ++ str " Lazy.t" ++ 
   fnl() ++ str "and "
 
 let pp_ind co kn ind =
   let prefix = if co then "__" else "" in 
   let some = ref false in 
   let init= ref (str "type ") in 
+  let names = 
+    Array.mapi (fun i p -> if p.ip_logical then mt () else 
+		  pp_global Type (IndRef (kn,i)))
+      ind.ind_packets
+  in 
+  let cnames = 
+    Array.mapi 
+      (fun i p -> if p.ip_logical then [||] else 
+	 Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1)))
+	   p.ip_types)
+      ind.ind_packets
+  in 
   let rec pp i =  
     if i >= Array.length ind.ind_packets then mt () 
     else 
       let ip = (kn,i) in 
-      let ip_equiv = option_map (fun kn -> (kn,i)) ind.ind_equiv in 
+      let ip_equiv = ind.ind_equiv, 0 in 
       let p = ind.ind_packets.(i) in 
       if is_custom (IndRef ip) then pp (i+1)
       else begin 
@@ -494,8 +445,9 @@ let pp_ind co kn ind =
 	  begin 
 	    init := (fnl () ++ str "and "); 
 	    s ++
-	    (if co then pp_coind ip p.ip_vars else mt ())
-	    ++ pp_one_ind prefix ip ip_equiv p.ip_vars p.ip_types ++
+	    (if co then pp_coind p.ip_vars names.(i) else mt ()) ++
+	    pp_one_ind 
+	      prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++
 	    pp (i+1)
 	  end
       end
@@ -510,159 +462,215 @@ let pp_mind kn i =
     | Singleton -> pp_singleton kn i.ind_packets.(0)
     | Coinductive -> pp_ind true kn i
     | Record projs -> 
-	let ip_equiv = option_map (fun kn -> (kn,0)) i.ind_equiv in 
-	pp_record kn projs ip_equiv i.ind_packets.(0)
+	pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0)
     | Standard -> pp_ind false kn i
 
-let pp_decl mpl = 
-  local_mpl := mpl; 
-  function
+let pp_decl = function
+    | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
+    | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase"
     | Dind (kn,i) -> pp_mind kn i
-    | Dtype (r, l, t) ->
-	if is_inline_custom r then failwith "empty phrase"
-	else 
-          let pp_r = pp_global r in 
-	  let l = rename_tvars keywords l in 
-          let ids, def = try 
+    | Dtype (r, l, t) -> 
+        let name = pp_global Type r in 
+	let l = rename_tvars keywords l in 
+        let ids, def = 
+	  try 
 	    let ids,s = find_type_custom r in 
 	    pp_string_parameters ids, str "=" ++ spc () ++ str s 
-	  with not_found -> 
+	  with Not_found -> 
 	    pp_parameters l, 
 	    if t = Taxiom then str "(* AXIOM TO BE REALIZED *)"
 	    else str "=" ++ spc () ++ pp_type false l t
-	  in 
-	  hov 2 (str "type" ++ spc () ++ ids ++ pp_r ++ 
-		 spc () ++ def)
+	in 
+	hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
     | Dterm (r, a, t) -> 
-	if is_inline_custom r then failwith "empty phrase"
-	else 
-	  let e = pp_global r in 
-	  pp_val e t ++
-	  hov 0 
-	    (str "let " ++ 
-	     if is_custom r then 
-	       e ++ str " = " ++ str (find_custom r)
-	     else if is_projection r then 
-	       let s = prvecti (fun _ -> str) 
-			 (Array.make (projection_arity r) " _") in 
-	       e ++ s ++ str " x = x." ++ e
-	     else pp_function (empty_env ()) e a)
+	let def = 
+	  if is_custom r then str (" = " ^ find_custom r)
+	  else if is_projection r then 
+	    (prvect str (Array.make (projection_arity r) " _")) ++ 
+	    str " x = x."
+	  else pp_function (empty_env ()) a
+	in 
+	let name = pp_global Term r in 
+	let postdef = if is_projection r then name else mt () in 
+	pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef)
     | Dfix (rv,defs,typs) ->
-	pp_Dfix true 0 (rv,defs,typs)
-
-let pp_spec mpl = 
-  local_mpl := mpl; 
-  function 
-    | Sind (kn,i) -> pp_mind kn i
-    | Sval (r,t) -> 
-	if is_inline_custom r then failwith "empty phrase"
-	else 
-	  hov 2 (str "val" ++ spc () ++ pp_global r ++ str " :" ++ spc () ++
-		 pp_type false [] t)
-    | Stype (r,vl,ot) -> 
-	if is_inline_custom r then failwith "empty phrase"
-	else 
-	  let l = rename_tvars keywords vl in 
-	  let ids, def = 
-	    try 
-	      let ids, s = find_type_custom r in 
-	      pp_string_parameters ids,  str "= " ++ str s 
-	    with not_found -> 
-	      let ids = pp_parameters l in 
-	      match ot with 
-		| None -> ids, mt ()
-		| Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" 
-		| Some t -> ids, str "=" ++ spc () ++ pp_type false l t 
-	  in 
-	  hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ spc () ++ def)
-
-let rec pp_specif mpl = function 
-  | (_,Spec s) -> pp_spec mpl s 
+	pp_Dfix (rv,defs,typs)
+
+let pp_alias_decl ren = function 
+  | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
+  | Dtype (r, l, _) -> 
+      let name = pp_global Type r in 
+      let l = rename_tvars keywords l in 
+      let ids = pp_parameters l in 
+      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ 
+	     str (ren^".") ++ name)
+  | Dterm (r, a, t) -> 
+      let name = pp_global Term r in
+      hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name)
+  | Dfix (rv, _, _) ->
+      prvecti (fun i r -> if is_inline_custom r then mt () else 
+		 let name = pp_global Term r in 
+		 hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++
+		 fnl ()) 
+	rv
+
+let pp_spec = function 
+  | Sval (r,_) when is_inline_custom r -> failwith "empty phrase"
+  | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
+  | Sind (kn,i) -> pp_mind kn i
+  | Sval (r,t) -> 
+      let def = pp_type false [] t in 
+      let name = pp_global Term r in 
+      hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
+  | Stype (r,vl,ot) -> 
+      let name = pp_global Type r in
+      let l = rename_tvars keywords vl in 
+      let ids, def = 
+	try 
+	  let ids, s = find_type_custom r in 
+	  pp_string_parameters ids,  str "= " ++ str s 
+	with Not_found -> 
+	  let ids = pp_parameters l in 
+	  match ot with 
+	    | None -> ids, mt ()
+	    | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" 
+	    | Some t -> ids, str "=" ++ spc () ++ pp_type false l t 
+      in 
+      hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
+
+let pp_alias_spec ren = function 
+  | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
+  | Stype (r,l,_) ->       
+      let name = pp_global Type r in 
+      let l = rename_tvars keywords l in 
+      let ids = pp_parameters l in 
+      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ 
+	     str (ren^".") ++ name)
+  | Sval _ -> assert false
+	  
+let rec pp_specif = function 
+  | (_,Spec (Sval _ as s)) -> pp_spec s
+  | (l,Spec s) -> 
+      (try 
+	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
+	 hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++
+	 fnl () ++ str "end" ++ fnl () ++
+	 pp_alias_spec ren s
+       with Not_found -> pp_spec s)
   | (l,Smodule mt) -> 
-      hov 1 
-	(str "module " ++ 
-	 P.pp_module mpl (MPdot (List.hd mpl, l)) ++
-	 str " : " ++ fnl () ++ pp_module_type mpl None (* (Some l) *) mt)
+      let def = pp_module_type (Some l) mt in 
+      let def' = pp_module_type (Some l) mt in 
+      let name = pp_modname (MPdot (top_visible_mp (), l)) in 
+      hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++
+      (try 
+	 let ren = Common.check_duplicate (top_visible_mp ()) l in
+	 fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def')
+       with Not_found -> Pp.mt ())
   | (l,Smodtype mt) -> 
-      hov 1
-	(str "module type " ++
-	 P.pp_module mpl (MPdot (List.hd mpl, l)) ++
-	 str " = " ++ fnl () ++ pp_module_type mpl None mt)
-
-and pp_module_type mpl ol = function 
+      let def = pp_module_type None mt in 
+      let name = pp_modname (MPdot (top_visible_mp (), l)) in
+      hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
+      (try 
+	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
+	 fnl () ++ str ("module type "^ren^" = ") ++ name
+       with Not_found -> Pp.mt ())
+
+and pp_module_type ol = function 
   | MTident kn -> 
-      let mp,_,l = repr_kn kn in P.pp_module mpl (MPdot (mp,l)) 
+      let mp,_,l = repr_kn kn in pp_modname (MPdot (mp,l))
   | MTfunsig (mbid, mt, mt') -> 
-      str "functor (" ++ 
-      P.pp_module mpl (MPbound mbid) ++
-      str ":" ++
-      pp_module_type mpl None mt ++
-      str ") ->" ++ fnl () ++
-      pp_module_type mpl None mt'
+      let name = pp_modname (MPbound mbid) in 
+      let typ = pp_module_type None mt in 
+      let def = pp_module_type None mt' in 
+      str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MTsig (msid, sign) ->
-      let mpl = match ol, mpl with 
-	| None, _ -> (MPself msid) :: mpl
-	| Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl
-	| _ -> assert false 
-      in
-      let l = map_succeed (pp_specif mpl) sign in 
+      let tvm = top_visible_mp () in 
+      option_iter (fun l -> add_subst msid (MPdot (tvm, l))) ol; 
+      let mp = MPself msid in
+      push_visible mp; 
+      let l = map_succeed pp_specif sign in 
+      pop_visible (); 
       str "sig " ++ fnl () ++ 
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
       fnl () ++ str "end"
 
 let is_short = function MEident _ | MEapply _ -> true | _ -> false
 
-let rec pp_structure_elem mpl = function 
-  | (_,SEdecl d) -> pp_decl mpl d
+let rec pp_structure_elem = function 
+  | (l,SEdecl d) -> 
+       (try 
+	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
+	 hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++
+	 fnl () ++ str "end" ++ fnl () ++
+	 pp_alias_decl ren d 
+	with Not_found -> pp_decl d)
   | (l,SEmodule m) ->
+      let def = pp_module_expr (Some l) m.ml_mod_expr in 
+      let name = pp_modname (MPdot (top_visible_mp (), l)) in 
       hov 1 
-	(str "module " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ 
-	 (*i if you want signatures everywhere: i*)
-	 (*i str " :" ++ fnl () ++ i*)
-	 (*i pp_module_type mpl None m.ml_mod_type ++ fnl () ++ i*)
-	 str " = " ++
-	 (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++
-	 pp_module_expr mpl (Some l) m.ml_mod_expr)
+	(str "module " ++ name ++ str " = " ++ 
+	 (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++ 
+      (try 
+	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
+	 fnl () ++ str ("module "^ren^" = ") ++ name
+       with Not_found -> mt ())
   | (l,SEmodtype m) -> 
-      hov 1 
-	(str "module type " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++
-	 str " = " ++ fnl () ++ pp_module_type mpl None m)
-
-and pp_module_expr mpl ol = function 
-  | MEident mp' -> P.pp_module mpl mp'
+      let def = pp_module_type None m in 
+      let name = pp_modname (MPdot (top_visible_mp (), l)) in 
+      hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++
+      (try 
+	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
+         fnl () ++ str ("module type "^ren^" = ") ++ name
+       with Not_found -> mt ())
+
+and pp_module_expr ol = function 
+  | MEident mp' -> pp_modname mp'
   | MEfunctor (mbid, mt, me) -> 
-      str "functor (" ++ 
-      P.pp_module mpl (MPbound mbid) ++
-      str ":" ++
-      pp_module_type mpl None mt ++
-      str ") ->" ++ fnl () ++
-      pp_module_expr mpl None me
+      let name = pp_modname (MPbound mbid) in
+      let typ = pp_module_type None mt in 
+      let def = pp_module_expr None me in 
+      str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MEapply (me, me') -> 
-      pp_module_expr mpl None me ++ str "(" ++ 
-      pp_module_expr mpl None me' ++ str ")"
+      pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")"
   | MEstruct (msid, sel) -> 
-      let mpl = match ol, mpl with 
-	| None, _ -> (MPself msid) :: mpl
-	| Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl
-	| _ -> assert false
-      in
-      let l = map_succeed (pp_structure_elem mpl) sel in 
+      let tvm = top_visible_mp () in 
+      let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
+      push_visible mp; 
+      let l = map_succeed pp_structure_elem sel in 
+      pop_visible (); 
       str "struct " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ 
       fnl () ++ str "end" 
 
 let pp_struct s =
-  let pp mp s = pp_structure_elem [mp] s ++ fnl2 () in 
+  let pp mp s = 
+    push_visible mp; 
+    let p = pp_structure_elem s ++ fnl2 () in 
+    pop_visible (); p
+  in
   prlist (fun (mp,sel) -> prlist identity (map_succeed (pp mp) sel)) s
 
 let pp_signature s = 
-  let pp mp s = pp_specif [mp] s ++ fnl2 () in 
+  let pp mp s = 
+    push_visible mp; 
+    let p = pp_specif s ++ fnl2 () in 
+    pop_visible (); p
+  in 
   prlist (fun (mp,sign) -> prlist identity (map_succeed (pp mp) sign)) s
 
-let pp_decl mpl d = 
-  try pp_decl mpl d with Failure "empty phrase" -> mt () 
-
-end
-
+let pp_decl d = 
+  try pp_decl d with Failure "empty phrase" -> mt ()
+
+let ocaml_descr = {
+  keywords = keywords;  
+  file_suffix = ".ml"; 
+  capital_file = false;  
+  preamble = preamble; 
+  pp_struct = pp_struct; 
+  sig_suffix = Some ".mli";  
+  sig_preamble = sig_preamble; 
+  pp_sig = pp_signature;
+  pp_decl = pp_decl; 
+}
 
 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 7a13590e2..c127fc1d1 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -8,47 +8,5 @@
 
 (*i $Id$ i*)
 
-(*s Some utility functions to be reused in module [Haskell]. *)
-
-open Pp
-open Names
-open Libnames
-open Miniml
-
-val pp_par : bool -> std_ppcmds -> std_ppcmds
-val pp_abst : identifier list -> std_ppcmds
-val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds 
-val pr_binding : identifier list -> std_ppcmds
-
-val rename_id : identifier -> Idset.t -> identifier
-
-val lowercase_id : identifier -> identifier
-val uppercase_id : identifier -> identifier
-
-val pr_upper_id : identifier -> std_ppcmds
-
-type env = identifier list * Idset.t
-
-val rename_vars: Idset.t -> identifier list -> env
-val rename_tvars: Idset.t -> identifier list -> identifier list 
-val push_vars : identifier list -> env -> identifier list * env
-val get_db_name : int -> env -> identifier
-
-val keywords : Idset.t
-
-val preamble : 
-  extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
-
-val preamble_sig : 
-  extraction_params -> module_path list -> bool*bool*bool -> 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. *)
-
-module Make : functor(P : Mlpp_param) -> Mlpp
-
-
-
-
+val ocaml_descr : Miniml.language_descr 
 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 0b358f77d..5048002d0 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -18,7 +18,7 @@ open Libnames
 open Miniml
 open Mlutil
 open Table
-open Ocaml
+open Common
 
 (*s Scheme renaming issues. *)
 
@@ -29,14 +29,14 @@ let keywords =
       "error"; "delay"; "force"; "_"; "__"] 
     Idset.empty
 
-let preamble _ _ (mldummy,_,_) _ = 
+let preamble _ _ usf = 
   str ";; This extracted scheme code relies on some additional macros" ++ 
   fnl () ++
   str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme" ++
   fnl () ++
   str "(load \"macros_extr.scm\")" ++
   fnl () ++ fnl () ++
-  (if mldummy then 
+  (if usf.mldummy then 
      str "(define __ (lambda (_) __))" 
      ++ fnl () ++ fnl()
    else mt ())
@@ -62,12 +62,9 @@ let pp_apply st _ = function
   | args -> hov 2 (paren (str "@ " ++ st ++ 
 			  (prlist (fun x -> spc () ++ x) args))) 
 
-(*s The pretty-printing functor. *)
+(*s The pretty-printer for Scheme syntax *)
 
-module Make = functor(P : Mlpp_param) -> struct
-
-let pp_global r = P.pp_global [initial_path] r
-let empty_env () = [], P.globals()
+let pp_global k r = str (Common.pp_global k r)
 
 (*s Pretty-printing of expressions.  *)
 
@@ -95,12 +92,12 @@ let rec pp_expr env args =
 			 (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) 
 		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
     | MLglob r -> 
-	apply (pp_global r)
+	apply (pp_global Term r)
     | MLcons (i,r,args') ->
 	assert (args=[]);
 	let st = 
 	  str "`" ++ 
-	  paren (pp_global r ++ 
+	  paren (pp_global Cons r ++ 
 		 (if args' = [] then mt () else spc ()) ++
 		 prlist_with_sep spc (pp_cons_args env) args')
 	in 
@@ -125,7 +122,7 @@ let rec pp_expr env args =
 
 and pp_cons_args env = function 
   | MLcons (i,r,args) when i<>Coinductive -> 
-      paren (pp_global r ++ 
+      paren (pp_global Cons r ++ 
 	     (if args = [] then mt () else spc ()) ++
 	     prlist_with_sep spc (pp_cons_args env) args)
   | e -> str "," ++ pp_expr env [] e
@@ -137,7 +134,7 @@ and pp_one_pat env (r,ids,t) =
     if ids = [] then mt () 
     else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
   in 
-  (pp_global r ++ args), (pp_expr env' [] t)
+  (pp_global Cons r ++ args), (pp_expr env' [] t)
   
 and pp_pat env pv = 
   prvect_with_sep fnl  
@@ -160,11 +157,11 @@ and pp_fix env j (ids,bl) args =
 
 (*s Pretty-printing of a declaration. *)
 
-let pp_decl _ = function
+let pp_decl = function
   | Dind _ -> mt ()
   | Dtype _ -> mt () 
   | Dfix (rv, defs,_) ->
-      let ppv = Array.map pp_global rv in 
+      let ppv = Array.map (pp_global Term) rv in 
       prvect_with_sep fnl 
 	(fun (pi,ti) -> 
 	   hov 2 
@@ -177,23 +174,33 @@ let pp_decl _ = function
       if is_inline_custom r then mt () 
       else 
 	if is_custom r then 
-	  hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ 
+	  hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ 
 			  str (find_custom r))) ++ fnl () ++ fnl () 
 	else 
-	  hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
+	  hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
 			  pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
 
-let pp_structure_elem mp = function 
-  | (l,SEdecl d) -> pp_decl mp d
+let pp_structure_elem = function 
+  | (l,SEdecl d) -> pp_decl d
   | (l,SEmodule m) -> 
       failwith "TODO: Scheme extraction of modules not implemented yet"
   | (l,SEmodtype m) -> 
       failwith "TODO: Scheme extraction of modules not implemented yet"
 
 let pp_struct = 
-  prlist (fun (mp,sel) -> prlist (pp_structure_elem mp) sel)
-
-let pp_signature s = assert false
-
-end
-
+  let pp_sel (mp,sel) = 
+    push_visible mp; let p = prlist pp_structure_elem sel in pop_visible (); p
+  in
+  prlist pp_sel
+
+let scheme_descr = {
+  keywords = keywords;  
+  file_suffix = ".scm"; 
+  capital_file = false;  
+  preamble = preamble; 
+  pp_struct = pp_struct; 
+  sig_suffix = None;
+  sig_preamble = (fun _ _ _ -> mt ()); 
+  pp_sig = (fun _ -> mt ()); 
+  pp_decl = pp_decl; 
+}
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index bded1a8a8..573bb9cef 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -8,20 +8,4 @@
 
 (*i $Id$ i*)
 
-(*s Some utility functions to be reused in module [Haskell]. *)
-
-open Pp
-open Miniml
-open Names
-
-val keywords : Idset.t
-
-val preamble : 
-  extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
-
-module Make : functor(P : Mlpp_param) -> Mlpp
-
-
-
-
-
+val scheme_descr : Miniml.language_descr 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 204319099..7a8ff95ed 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -20,37 +20,49 @@ open Util
 open Pp
 open Miniml
 
-(*S Utilities concerning [module_path] and [kernel_names] *)
+(*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
 
-let occur_kn_in_ref kn =
- function
+let occur_kn_in_ref kn = function
   | IndRef (kn',_)
   | ConstructRef ((kn',_),_) -> kn = kn'
   | ConstRef _ -> false
   | VarRef _ -> assert false
-
-let modpath_of_r r = match r with 
-    | ConstRef kn -> con_modpath kn
-    | IndRef (kn,_)
-    | ConstructRef ((kn,_),_) -> modpath kn
-    | VarRef _ -> assert false
-
-let label_of_r r = match r with 
-    | ConstRef kn -> con_label kn
-    | IndRef (kn,_)
-    | ConstructRef ((kn,_),_) -> label kn
-    | VarRef _ -> assert false
-
-let current_toplevel () = fst (Lib.current_prefix ())
+      
+let modpath_of_r = function 
+  | ConstRef kn -> con_modpath kn
+  | IndRef (kn,_)
+  | ConstructRef ((kn,_),_) -> modpath kn
+  | VarRef _ -> assert false
+      
+let label_of_r = function 
+  | ConstRef kn -> con_label kn
+  | IndRef (kn,_)
+  | ConstructRef ((kn,_),_) -> label kn
+  | VarRef _ -> assert false
 
 let rec base_mp = function 
   | MPdot (mp,l) -> base_mp mp 
   | mp -> mp 
 
+let rec mp_length = function
+  | MPdot (mp, _) -> 1 + (mp_length mp)
+  | _ -> 1
+
 let is_modfile = function 
   | MPfile _ -> true 
   | _ -> false
 
+let string_of_modfile = function 
+  | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
+  | _ -> assert false
+
+let rec modfile_of_mp = function 
+  | (MPfile _) as mp -> mp
+  | MPdot (mp,_) -> modfile_of_mp mp 
+  | _ -> raise Not_found
+
+let current_toplevel () = fst (Lib.current_prefix ())
+
 let is_toplevel mp = 
   mp = initial_path || mp = current_toplevel ()
 
@@ -60,8 +72,56 @@ let at_toplevel mp =
 let visible_kn kn = at_toplevel (base_mp (modpath kn))
 let visible_con kn = at_toplevel (base_mp (con_modpath kn))
 
+let rec prefixes_mp mp = match mp with 
+  | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
+  | _ -> MPset.singleton mp 
+
+let rec get_nth_label_mp n mp = match mp with 
+  | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp 
+  | _ -> failwith "get_nth_label: not enough MPdot"
+
+let get_nth_label n r = 
+  if n=0 then label_of_r r else get_nth_label_mp n (modpath_of_r r)
+
+let rec common_prefix prefixes_mp1 mp2 = 
+  if MPset.mem mp2 prefixes_mp1 then mp2 
+  else match mp2 with 
+    | MPdot (mp,_) -> common_prefix prefixes_mp1 mp 
+    | _ -> raise Not_found
+
+let common_prefix_from_list mp0 mpl = 
+  let prefixes_mp0 = prefixes_mp mp0 in 
+  let rec f = function 
+    | [] -> raise Not_found
+    | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l
+  in f mpl
+
+let rec parse_labels ll = function 
+  | MPdot (mp,l) -> parse_labels (l::ll) mp 
+  | mp -> mp,ll
+
+let labels_of_mp mp = parse_labels [] mp 
+
+let labels_of_ref r = 
+ let mp,_,l =
+  match r with
+     ConstRef con -> repr_con con
+   | IndRef (kn,_)
+   | ConstructRef ((kn,_),_) -> repr_kn kn
+   | VarRef _ -> assert false
+ in
+  parse_labels [l] mp
+
+let rec add_labels_mp mp = function 
+  | [] -> mp 
+  | l :: ll -> add_labels_mp (MPdot (mp,l)) ll
+
+
 (*S The main tables: constants, inductives, records, ... *)
 
+(* Theses tables are not registered within coq save/undo mechanism 
+   since we reset their contents at each run of Extraction *)
+
 (*s Constants tables. *) 
 
 let terms = ref (Cmap.empty : ml_decl Cmap.t)
@@ -109,11 +169,26 @@ let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
 let is_projection r = Refmap.mem r !projs
 let projection_arity r = Refmap.find r !projs
 
+(*s Table of used axioms *)
+
+let info_axioms = ref Refset.empty
+let log_axioms = ref Refset.empty
+let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty
+let add_info_axiom r = info_axioms := Refset.add r !info_axioms
+let add_log_axiom r = log_axioms := Refset.add r !log_axioms
+
+(*s Extraction mode: modular or monolithic *)
+
+let modular_ref = ref false
+
+let set_modular b = modular_ref := b
+let modular () = !modular_ref
+
 (*s Tables synchronization. *)
 
 let reset_tables () = 
   init_terms (); init_types (); init_inductives (); init_recursors (); 
-  init_projs ()
+  init_projs (); init_axioms ()
 
 (*s Printing. *)
 
@@ -146,21 +221,34 @@ let pr_long_global r =
 
 let err s = errorlabstrm "Extraction" s
 
+let warning_axioms () = 
+  let info_axioms = Refset.elements !info_axioms in 
+  if info_axioms = [] then () 
+  else begin
+    let s = if List.length info_axioms = 1 then "axiom" else "axioms" in 
+    msg_warning 
+      (str ("The following "^s^" must be realized in the extracted code:")
+       ++ hov 1 (spc () ++ prlist_with_sep spc pr_global info_axioms) 
+       ++ str "." ++ fnl ())
+  end;
+  let log_axioms = Refset.elements !log_axioms in 
+  if log_axioms = [] then ()
+  else begin
+    let s = if List.length log_axioms = 1 then "axiom was" else "axioms were" 
+    in 
+    msg_warning
+      (str ("The following logical "^s^" encountered:") ++
+       hov 1 (spc () ++ prlist_with_sep spc pr_global log_axioms ++ str ".\n") ++
+       str "Having invalid logical axiom in the environment when extracting" ++
+       spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
+       fnl ())
+  end
+
 let error_axiom_scheme r i = 
   err (str "The type scheme axiom " ++ spc () ++
        pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ 
        str " type variable(s).") 
 
-let warning_info_ax r =
-  msg_warning (str "You must realize axiom " ++
-		  pr_global r ++ str " in the extracted code.")
-
-let warning_log_ax r = 
-  msg_warning (str "This extraction depends on logical axiom" ++ spc () ++ 
-		  pr_global r ++ str "." ++ spc() ++ 
-		  str "Having false logical axiom in the environment when extracting" ++ 
-		  spc () ++ str "may lead to incorrect or non-terminating ML terms.")
-
 let check_inside_module () = 
   if Lib.is_modtype () then 
     err (str "You can't do that within a Module Type." ++ fnl () ++
@@ -186,15 +274,11 @@ let error_nb_cons () =
 
 let error_module_clash s = 
   err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++ 
-       str "This is not allowed in ML. Please do some renaming first.")
+       str "This is not supported yet. Please do some renaming first.") 
 
 let error_unknown_module m = 
   err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") 
 
-let error_toplevel () = 
-  err (str "Toplevel pseudo-ML language can be used only at Coq toplevel.\n" ++
-       str "You should use Extraction Language Ocaml or Haskell before.") 
-
 let error_scheme () = 
   err (str "No Scheme modular extraction available yet.")
 
@@ -203,9 +287,11 @@ let error_not_visible r =
        str "For example, it may be inside an applied functor." ++
        str "Use Recursive Extraction to get the whole environment.")
 
-let error_MPfile_as_mod d = 
-  err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^
-	    "Extraction cannot currently deal with this situation.\n"))
+let error_MPfile_as_mod mp = 
+  err (str ("The whole file "^(string_of_modfile mp)^
+	    ".v is used somewhere as a module.\n"^
+	    "Monolithic Extraction cannot deal with this situation.\n"^
+	    "Please use (Recursive) Extraction Library instead.\n"))
 
 let error_record r = 
   err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++
@@ -216,8 +302,16 @@ let check_loaded_modfile mp = match base_mp mp with
       err (str ("Please load library "^(string_of_dirpath dp^" first.")))
   | _ -> ()
 
+let info_file f =   
+  Options.if_verbose message 
+    ("The file "^f^" has been created by extraction.")
+
+
 (*S The Extraction auxiliary commands *)
 
+(* The objects defined below should survive an arbitrary time, 
+   so we register them to coq save/undo mechanism. *)
+
 (*s Extraction AutoInline *)
 
 let auto_inline_ref = ref true
@@ -305,7 +399,7 @@ let _ = declare_int_option
 
 (*s Extraction Lang *)
 
-type lang = Ocaml | Haskell | Scheme | Toplevel
+type lang = Ocaml | Haskell | Scheme
 
 let lang_ref = ref Ocaml
 
@@ -327,7 +421,6 @@ let _ = declare_summary "Extraction Lang"
 	  
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
-
 (*s Extraction Inline/NoInline *)
 
 let empty_inline_table = (Refset.empty,Refset.empty)
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 55402d94a..304e374b5 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -14,39 +14,49 @@ open Miniml
 open Declarations
 
 val id_of_global : global_reference -> identifier
+val pr_long_global : global_reference -> Pp.std_ppcmds
+
 
 (*s Warning and Error messages. *)
 
+val warning_axioms : unit -> unit
 val error_axiom_scheme : global_reference -> int -> 'a
-val warning_info_ax : global_reference -> unit
-val warning_log_ax : global_reference -> unit
 val error_constant : global_reference -> 'a
 val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
 val error_module_clash : string -> 'a 
 val error_unknown_module : qualid -> 'a
-val error_toplevel : unit -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
-val error_MPfile_as_mod : dir_path -> 'a
+val error_MPfile_as_mod : module_path -> 'a
 val error_record : global_reference -> 'a 
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
 val check_loaded_modfile : module_path -> unit
 
-(*s utilities concerning [module_path]. *)
+val info_file : string -> unit
+
+(*s utilities about [module_path] and [kernel_names] and [global_reference] *)
 
 val occur_kn_in_ref : kernel_name -> global_reference -> bool
 val modpath_of_r : global_reference -> module_path
 val label_of_r : global_reference -> label
-
 val current_toplevel : unit -> module_path
 val base_mp : module_path -> module_path
-val is_modfile : module_path -> bool 
+val is_modfile : module_path -> bool
+val string_of_modfile : module_path -> string 
 val is_toplevel : module_path -> bool
 val at_toplevel : module_path -> bool 
 val visible_kn : kernel_name -> bool
 val visible_con : constant -> bool
+val mp_length : module_path -> int
+val prefixes_mp : module_path -> MPset.t
+val modfile_of_mp : module_path -> module_path
+val common_prefix_from_list : module_path -> module_path list -> module_path
+val add_labels_mp : module_path -> label list -> module_path
+val get_nth_label_mp : int -> module_path -> label
+val get_nth_label : int -> global_reference -> label
+val labels_of_ref : global_reference -> module_path * label list
 
 (*s Some table-related operations *)
 
@@ -66,6 +76,9 @@ val add_projection : int -> constant -> unit
 val is_projection : global_reference -> bool 
 val projection_arity : global_reference -> int
 
+val add_info_axiom : global_reference -> unit
+val add_log_axiom : global_reference -> unit
+
 val reset_tables : unit -> unit
 
 (*s AutoInline parameter *) 
@@ -95,9 +108,14 @@ val optims :  unit -> opt_flag
 
 (*s Target language. *)
 
-type lang = Ocaml | Haskell | Scheme | Toplevel
+type lang = Ocaml | Haskell | Scheme
 val lang : unit -> lang 
 
+(*s Extraction mode: modular or monolithic *)
+
+val set_modular : bool -> unit
+val modular : unit -> bool 
+
 (*s Table for custom inlining *) 
 
 val to_inline : global_reference -> bool