Extraction des modules, enfin !

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

20 files changed, 1898 insertions, 1327 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 28f560d96..0f07658fb 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -11,15 +11,16 @@
 open Pp
 open Util
 open Names
+open Term
+open Declarations
 open Nameops
 open Libnames
-open Nametab
 open Table
 open Miniml
 open Mlutil
 open Ocaml
 
-(*s Get all references used in one [ml_decl list]. *)
+(*s Get all references used in one [ml_structure]. *)
 
 module Orefset = struct 
   type t = { set : Refset.t ; list : global_reference list }
@@ -33,51 +34,12 @@ end
 
 type updown = { mutable up : Orefset.t ; mutable down : Orefset.t }
 
-let decl_get_references ld = 
+let struct_get_references struc = 
   let o = { up = Orefset.empty ; down = Orefset.empty } in 
-  let do_term r = o.down <- Orefset.add r o.down in
-  let do_cons r = o.up <- Orefset.add r o.up in 
+  let do_term r = o.down <- Orefset.add (long_r r) o.down in
+  let do_cons r = o.up <- Orefset.add (long_r r) o.up in 
   let do_type = if lang () = Haskell then do_cons else do_term in 
-  List.iter (decl_iter_references do_term do_cons do_type) ld; o
-
-(*S Modules considerations. *)
-
-let long_module r = 
-  match modpath (kn_of_r r) with 
-    | MPfile d -> d
-    | _ -> anomaly "TODO: extraction not ready for true modules"
-
-let short_module r = List.hd (repr_dirpath (long_module r))
-
-(*s [extract_module m] returns all the global reference declared 
-  in a module. This is done by traversing the segment of module [m]. 
-  We just keep constants and inductives. *)
-
-let segment_contents seg = 
-  let get_reference = function
-    | (_,kn), Lib.Leaf o ->
-	(match Libobject.object_tag o with
-	   | "CONSTANT" -> ConstRef kn
-	   | "INDUCTIVE" -> IndRef (kn,0)
-	   | _ -> failwith "caught")
-    | _ -> failwith "caught"
-  in
-  Util.map_succeed get_reference seg
-
-let module_contents m =
-  segment_contents (Declaremods.module_objects (MPfile m))
-
-(*s The next function finds all names common to at least two used modules. *)
-
-let modules_reference_clashes modules = 
-  let id_of_r r = lowercase_id (id_of_global None r) in
-  let map = 
-    Dirset.fold
-      (fun mod_name map -> 
-	 let rl = List.map id_of_r (module_contents mod_name) in 
-	 List.fold_left (fun m id -> Idmap.add id (Idmap.mem id m) m) map rl)
-      modules Idmap.empty 
-  in Idmap.fold (fun i b s -> if b then Idset.add i s else s) map Idset.empty
+  struct_iter_references do_term do_cons do_type struc; o
 
 (*S Renamings. *)
 
@@ -85,80 +47,238 @@ let modules_reference_clashes modules =
 
 let keywords = ref Idset.empty
 let global_ids = ref Idset.empty
+let modular = ref false
 
 let renamings = Hashtbl.create 97
 let rename r s = Hashtbl.add renamings r s
 let get_renamings r = Hashtbl.find renamings r 
 
-let create_mono_renamings decls =  
-  let { up = u ; down = d } = decl_get_references decls in 
-  let add upper r = 
-    try if not (to_inline r) then raise Not_found; 
-      rename r (find_ml_extraction r)  
+let must_qualify = ref Refset.empty
+
+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 modular_rename up id = 
+  let s = string_of_id id in
+  let prefix = if up then "Coq_" else "coq_" in 
+  let check = if up then is_upper else is_lower in 
+  if not (check s) ||
+    (Idset.mem id !keywords) ||
+    (String.length s >= 4 && String.sub s 0 4 = prefix) 
+  then prefix ^ s
+  else s
+
+let rename_module = modular_rename true 
+
+let mp_to_list mp = 
+  let rec f ls = function 
+    | MPfile d -> 
+	String.capitalize (string_of_id (List.hd (repr_dirpath d))) :: ls
+    | MPself msid -> rename_module (id_of_msid msid) :: ls
+    | MPbound mbid -> rename_module (id_of_mbid mbid) :: ls
+    | MPdot (mp,l) -> f (rename_module (id_of_label l) :: ls) mp
+  in f [] mp
+
+let mp_to_list' mp = 
+  let rec f ls = function 
+    | mp when at_toplevel mp -> ls
+    | MPself msid -> rename_module (id_of_msid msid) :: ls
+    | MPbound mbid -> rename_module (id_of_mbid mbid) :: ls
+    | MPdot (mp,l) -> f (rename_module (id_of_label l) :: ls) mp
+    | _ -> assert false
+  in f [] mp
+
+let string_of_modlist l = 
+  List.fold_right (fun s s' -> if s' = "" then s else s ^ "." ^ s') l ""
+
+let string_of_ren l s = 
+  if l = [] then s else (string_of_modlist l)^"."^s
+
+let contents_first_level mp = 
+  let s = ref Stringset.empty in 
+  let add b id = s := Stringset.add (modular_rename b id) !s in 
+  let upper_type = (lang () = Haskell) in
+  let contents_seb = function 
+    | (l, SEBconst cb) -> 
+	let id = id_of_label l in 
+	(match Extraction.constant_kind !cur_env cb with 
+	   | Extraction.Logical -> () 
+	   | Extraction.Type -> add upper_type (id_of_label l)
+	   | Extraction.Term -> add false (id_of_label l))
+    | (_, SEBmind mib) ->
+	Array.iter 
+	  (fun mip -> 
+	     if mip.mind_sort = (Prop Null) then ()
+	     else begin
+	       add upper_type mip.mind_typename; 
+	       Array.iter (add true) mip.mind_consnames
+	     end)
+	  mib.mind_packets
+    | _ -> ()
+  in
+  match (Environ.lookup_module mp !cur_env).mod_expr with 
+    | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; (mp,!s)
+    | _ -> mp,!s
+
+let modules_first_level mp = 
+  let s = ref Stringset.empty in 
+  let add id = s := Stringset.add (rename_module id) !s in 
+  let contents_seb = function 
+    | (l, (SEBmodule _ | SEBmodtype _)) -> add (id_of_label l) 
+    | _ -> ()
+  in
+  match (Environ.lookup_module mp !cur_env).mod_expr with 
+    | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; !s
+    | _ -> !s
+
+let contents_first_level = 
+  let cache = ref MPmap.empty in 
+  fun mp -> 
+    try MPmap.find mp !cache 
     with Not_found -> 
-      let id = id_of_global None r in 
-      let id = if upper then uppercase_id id else lowercase_id id in
-      let id = rename_id id !global_ids in 
-      global_ids := Idset.add id !global_ids; 
-      rename r (string_of_id id)
+      let res = contents_first_level mp in 
+      cache := MPmap.add mp res !cache; 
+      res
+
+let rec clash_in_contents mp0 s = function  
+  | [] -> false
+  | (mp,_) :: _ when mp = mp0 -> false
+  | (mp,ss) :: l -> (Stringset.mem s ss) || (clash_in_contents mp0 s l) 
+
+let create_modular_renamings struc = 
+  let cur_mp = fst (List.hd struc) in
+  let modfiles = ref MPset.empty in 
+  let { up = u ; down = d } = struct_get_references struc 
   in 
-  List.iter (add true) (List.rev (Orefset.list u)); 
-  List.iter (add false) (List.rev (Orefset.list d))
-
-let create_modular_renamings current_module decls = 
-  let { up = u ; down = d } = decl_get_references decls in 
-  let modules = 
-    let f r s = Dirset.add (long_module r) s in 
-    Refset.fold f (Orefset.set u) (Refset.fold f (Orefset.set d) Dirset.empty)
-  in 
-  let modular_clashs = modules_reference_clashes modules 
+  (* 1) create renamings of objects *)
+  let add upper r = 
+    let mp = modpath (kn_of_r r) in 
+    begin try 
+      let mp = modfile_of_mp mp in 
+      if mp <> cur_mp then modfiles := MPset.add mp !modfiles
+    with Not_found -> () 
+    end; 
+    let mplist = mp_to_list (modpath (kn_of_r r)) in 
+    let s = modular_rename upper (id_of_global r) in 
+    global_ids := Idset.add (id_of_string s) !global_ids;    
+    Hashtbl.add renamings r (mplist,s)
+  in
+  Refset.iter (add true) (Orefset.set u); 
+  Refset.iter (add false) (Orefset.set d); 
+  
+  (* 2) determine the opened libraries and the potential clashes *)
+  let used_modules = MPset.elements !modfiles in 
+  let s = ref (modules_first_level cur_mp) in 
+  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 env = List.rev_map contents_first_level used_modules in 
+  let needs_qualify r = 
+    let mp = modpath (kn_of_r r) in 
+    if not (is_modfile mp) || mp = cur_mp then () 
+    else
+      let s = snd (get_renamings r) in 
+      if clash_in_contents mp s env 
+      then must_qualify := Refset.add r !must_qualify
   in 
-  let clash r id = 
-    exists_cci (make_path (dirpath (sp_of_global None r)) id)
+  Refset.iter needs_qualify (Orefset.set u);
+  Refset.iter needs_qualify (Orefset.set d); 
+  used_modules
+
+let create_mono_renamings struc = 
+  let fst_level_modules = ref Idmap.empty in 
+  let { up = u ; down = d } = struct_get_references struc 
   in 
-  let prefix upper r id = 
-    let prefix = if upper then "Coq_" else "coq_" in 
-    let id' = if upper then uppercase_id id else lowercase_id id in
-    if (Idset.mem id' !keywords) || (id <> id' && clash r id') then 
-      id_of_string (prefix^(string_of_id id))
-    else id'
-  in
+  (* 1) create renamings of objects *)
   let add upper r = 
-    try if not (to_inline r) then raise Not_found; 
-      rename r (find_ml_extraction r)  
-    with Not_found -> 
-      let id = id_of_global None r in 
-      let m = short_module r in 
-      let id' = prefix upper r id in 
-      let qualify = 
-	(m <> current_module) && (Idset.mem (lowercase_id id) modular_clashs) 
-      in 
-      if qualify then 
-	let s = String.capitalize (string_of_id m) ^ "." ^ (string_of_id id') in
-	Hashtbl.add renamings r s
-      else begin
-	global_ids := Idset.add id' !global_ids;
-	Hashtbl.add renamings r (string_of_id id')
-      end
+    let mp = modpath (kn_of_r r) in 
+    begin try 
+      let mp,l = fst_level_module_of_mp mp in
+      let id = id_of_label l in 
+      if Idmap.find id !fst_level_modules <> mp then 
+	error_module_clash (string_of_id id) 
+      else fst_level_modules := Idmap.add id mp !fst_level_modules
+    with Not_found -> ()
+    end;
+    let mplist = mp_to_list' (modpath (kn_of_r r)) in 
+    let my_id = if upper then uppercase_id else lowercase_id in
+    let id = 
+      if mplist = [] then 
+	next_ident_away (my_id (id_of_global r)) (Idset.elements !global_ids)
+      else id_of_string (modular_rename upper (id_of_global r)) 
+    in 
+    global_ids := Idset.add id !global_ids;    
+    Hashtbl.add renamings r (mplist,string_of_id id)
   in
   List.iter (add true) (List.rev (Orefset.list u)); 
-  List.iter (add false) (List.rev (Orefset.list d)); 
-  Idset.remove current_module 
-    (Dirset.fold (fun m s -> Idset.add (List.hd (repr_dirpath m)) s) 
-       modules Idset.empty)
+  List.iter (add false) (List.rev (Orefset.list d))
 		    
 (*s Renaming issues at toplevel *)
 
 module ToplevelParams = struct
   let globals () = Idset.empty
-  let pp_global r = Printer.pr_global r
+  let pp_global _ r = pr_global r
+  let pp_long_module mp = str (string_of_mp mp)
+  let pp_short_module id = pr_id id
 end
 
 (*s Renaming issues for a monolithic or modular extraction. *)
 
+let rec remove_common l l' = match l,l' with 
+  | [], _ -> l' 
+  | s::q, s'::q' -> if s = s' then remove_common q q' else l'
+  | _ -> assert false 
+
+let rec length_common_prefix l l' = match l,l' with 
+  | [],_ -> 0
+  | _, [] -> 0 
+  | s::q, s'::q' -> if s <> s' then 0 else 1+(length_common_prefix q q')
+
+let rec decreasing_contents mp = match mp with 
+  | MPdot (mp',_) -> (contents_first_level mp) :: (decreasing_contents mp')
+  | mp when is_toplevel mp -> [] 
+  | _ -> [contents_first_level mp]
+
 module StdParams = struct
+
   let globals () = !global_ids
-  let pp_global r = str (Hashtbl.find renamings r)
+
+  let pp_global cur_mp r = 
+    let cur_mp = long_mp cur_mp in 
+    let cur_l = if !modular then mp_to_list cur_mp else mp_to_list' cur_mp in 
+    let r = long_r r in 
+    let mp = modpath (kn_of_r r) in 
+    let l,s = get_renamings r in 
+    let n = length_common_prefix cur_l l in 
+    if n = 0 && !modular (* [r] is in another module *)
+    then 
+      if (Refset.mem r !must_qualify) || (lang () = Haskell)
+      then str (string_of_ren l s)
+      else 
+	if clash_in_contents mp s (decreasing_contents cur_mp) 
+	then str (string_of_ren l s)
+	else str s
+    else 
+      let nl = List.length l in 
+      if n = nl && nl < List.length cur_l then (* strict prefix *)
+	if clash_in_contents mp s (decreasing_contents cur_mp) 
+	then error_unqualified_name (string_of_ren l s) (string_of_modlist cur_l)
+	else str s
+      else (* [cur_mp] and [mp] are orthogonal *)
+	let l = remove_common cur_l l 
+	in str (string_of_ren l s)
+	     
+  let pp_long_module mp = 
+    str (string_of_modlist (if !modular then mp_to_list mp else mp_to_list' mp))
+
+  let pp_short_module id = str (rename_module id)
 end
 
 module ToplevelPp = Ocaml.Make(ToplevelParams)
@@ -166,11 +286,22 @@ module OcamlPp = Ocaml.Make(StdParams)
 module HaskellPp = Haskell.Make(StdParams)
 module SchemePp = Scheme.Make(StdParams)
 
-let pp_decl () = match lang () with 
-  | Ocaml -> OcamlPp.pp_decl
-  | Haskell -> HaskellPp.pp_decl
-  | Scheme -> SchemePp.pp_decl
-  | Toplevel -> ToplevelPp.pp_decl
+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 
@@ -178,7 +309,8 @@ let set_keywords () =
     | Haskell -> keywords := Haskell.keywords
     | Scheme -> keywords := Scheme.keywords
     | Toplevel -> keywords := Idset.empty);
-  global_ids := !keywords
+  global_ids := !keywords; 
+  must_qualify := Refset.empty
     
 let preamble prm = match lang () with 
   | Ocaml -> Ocaml.preamble prm   
@@ -186,36 +318,59 @@ let preamble prm = match lang () with
   | 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 extract_to_file f prm decls =
+let print_structure_to_file f prm struc =
   cons_cofix := Refset.empty;
   Hashtbl.clear renamings;
   set_keywords ();
-  let used_modules = 
-    if lang () = Toplevel then Idset.empty 
-    else if prm.modular then
-      create_modular_renamings prm.mod_name decls
-    else begin create_mono_renamings decls; Idset.empty end
+  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 pp_decl = pp_decl () in 
-  let cout = match f with 
-    | None -> stdout
-    | Some f -> open_out f in
+  let print_dummys =
+    (struct_ast_search MLdummy struc, 
+     struct_type_search Tdummy struc, 
+     struct_type_search Tunknown struc)
+  in
+  (* print the implementation *)
+  let cout = match f with None -> stdout | Some (f,_) -> open_out f in
   let ft = Pp_control.with_output_to cout in
-  let print_dummys = 
-    (decl_search MLdummy decls, 
-     decl_type_search Tdummy decls, 
-     decl_type_search Tunknown decls) in 
-  pp_with ft (preamble prm used_modules print_dummys);
-  begin try
-    List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
-  with e ->
-    pp_flush_with ft (); if f <> None then close_out cout; raise e
+  begin try 
+    msg_with ft (preamble prm used_modules print_dummys);
+    msg_with ft (pp_struct struc);
+    if f <> None then close_out cout;
+  with e -> 
+    if f <> None then close_out cout; raise e 
   end;
-  pp_flush_with ft ();
-  if f <> None then close_out cout;  
-    
+  (* 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
+    | _ -> () 
+
 (*i 
   (* DO NOT REMOVE: used when making names resolution *)
   let cout = open_out (f^".ren") in 
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index fb2291edf..7dae2ae19 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -14,16 +14,10 @@ open Libnames
 open Miniml
 open Mlutil
 
-val long_module : global_reference -> dir_path
+val print_one_decl :
+  ml_structure -> module_path -> ml_decl -> unit
 
-val create_mono_renamings : ml_decl list -> unit
-val set_keywords : unit -> unit
+val print_structure_to_file : 
+  (string * string) option -> extraction_params -> ml_structure -> unit
 
-val pp_decl : unit -> ml_decl -> std_ppcmds
 
-val segment_contents : Lib.library_segment -> global_reference list
-
-val module_contents : dir_path -> global_reference list 
-
-val extract_to_file : 
-  string option -> extraction_params -> ml_decl list -> unit
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 0e5325a2e..ab798eebf 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -8,22 +8,56 @@
 
 (*i $Id$ i*)
 
-open Pp
-open Util
+open Term
 open Declarations
 open Names
-open Nameops
 open Libnames
+open Pp
+open Util
 open Miniml
 open Table
 open Extraction
 open Mlutil
 open Common
 
-let mp_of_kn kn = 
-  let mp,_,l = repr_kn kn in MPdot (mp,l) 
+(*s Recursive computation of the global references to extract. 
+    We use a set of functions visiting the extracted objects in
+    a depth-first way.
+    We maintain an (imperative) structure [visit'] containing
+    the set of already visited references and the list of 
+    references to extract. The entry point is the function [visit]:
+    it first normalizes the reference, and then check it has already been 
+    visisted; if not, it adds it to the set of visited references, then
+    recursively traverses its extraction and finally adds it to the [result]. *)
+
+(*  Recursive extracted environment for a list of reference: we just
+    iterate [visit] on the list, starting with an empty
+    extracted environment, and we return the reversed list of 
+    declaration in the field [result]. *)
+
+type visit' = { mutable visited : KNset.t; mutable result : ml_decl list }
 
-let toplevel () = 
+let extract_env rl =
+  let knset =  
+    Refset.fold (compose KNset.add kn_of_r) (all_customs ()) KNset.empty in 
+  let v = { visited = knset; result = [] } in 
+  let rec visit r = 
+    let kn = kn_of_r r in 
+    if not (KNset.mem kn v.visited) then begin
+      (* we put [kn] in [visited] first to avoid loops in inductive defs *)
+      v.visited <- KNset.add kn v.visited;
+      let d = extract_declaration !cur_env r in 
+      decl_iter_references visit visit visit d;
+      v.result <- d :: v.result
+    end
+  in 
+  List.iter visit rl;
+  List.rev v.result
+
+
+(*s Obtaining Coq environment. *)
+
+let toplevel_env () = 
   let seg = Lib.contents_after None in 
   let get_reference = function 
     | (_,kn), Lib.Leaf o ->
@@ -37,30 +71,36 @@ let toplevel () =
 	in l,seb
     | _ -> failwith "caught"
   in 
-  MEBstruct (initial_msid, List.rev (map_succeed get_reference seg))
+  match current_toplevel () with 
+    | MPself msid -> MEBstruct (msid, List.rev (map_succeed get_reference seg))
+    | _ -> assert false
 
 let environment_until dir_opt = 
   let rec parse = function 
+    | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()]
     | [] -> [] 
-    | d :: l when dir_opt = Some d -> []
     | d :: l -> 
 	match (Global.lookup_module (MPfile d)).mod_expr with 
-	  | Some meb -> (d, meb) :: (parse l)
+	  | Some meb -> 
+	      if dir_opt = Some d then [MPfile d, meb]
+	      else (MPfile d, meb) :: (parse l)
 	  | _ -> assert false
   in parse (Library.loaded_libraries ())
 
-let std_kn mp l = make_kn mp empty_dirpath l
+(*s Aux. functions *)
 
-let rec sub_modpath mp = match mp with 
-  | MPdot (mp',_) -> MPset.add mp (sub_modpath mp')
-  | _ -> MPset.singleton mp
+let r_of_kn env kn = 
+  try let _ = Environ.lookup_constant kn env in ConstRef kn
+  with Not_found -> 
+    try let _ = Environ.lookup_mind kn env in IndRef (kn,0) 
+    with Not_found -> assert false
 
 (* Add _all_ direct subobjects of a module, not only those exported. 
    Build on the Modops.add_signature model. *)
 
 let add_structure mp msb env = 
   let add_one env (l,elem) = 
-    let kn = std_kn mp l in 
+    let kn = make_kn mp empty_dirpath l in 
     match elem with 
       | SEBconst cb -> Environ.add_constant kn cb env 
       | SEBmind mib -> Environ.add_mind kn mib env 
@@ -70,486 +110,366 @@ let add_structure mp msb env =
 
 let add_functor mbid mtb env = 
   Modops.add_module (MPbound mbid) (Modops.module_body_of_type mtb) env 
-  
-let mp_short = ref initial_path 
-let cur_env = ref (Global.env ()) 
-
-let pr_label l = str (string_of_label l)
-let pr_term t = Printer.prterm_env !cur_env t
-
-let rec print_seb = function 
-  | l, SEBconst {const_body=None; const_type=t} ->
-      msg (str "Cst " ++ pr_label l ++ str " : " ++ 
-      pr_term t ++ fnl ()) 
-  | l, SEBconst {const_body=Some lbody} -> 
-      let body = Declarations.force lbody in 
-      let t = Retyping.get_type_of !cur_env Evd.empty body in 
-      msg (str "Cst " ++ pr_label l ++ str " = " ++ 
-	   pr_term body ++ fnl () ++
-	   str "  : " ++ pr_term t ++ fnl ())
-  | l, SEBmind mind -> 
-      let t = Inductive.type_of_inductive !cur_env ((std_kn !mp_short l),0) in 
-      msg (str "Ind " ++ pr_label l ++ str " : " ++ pr_term t ++ fnl ()) 
-  | l, SEBmodule mb -> print_module l mb 
-  | l, SEBmodtype mtb -> print_modtype l mtb 
-
-and print_msb = function 
-  | [] -> () 
-  | seb :: msb -> print_seb seb; print_msb msb
-
-and print_module l mb = 
-  msg (str "Begin Module " ++ pr_label l ++ fnl ());
-  (match mb.mod_expr with 
-     | None -> ()
-     | Some meb -> print_meb meb);
-  msg (str "End Module " ++ pr_label l ++ fnl ())
-
-and print_meb = function 
+
+(*s First, we parse everything in order to produce 1) an env containing 
+   every internal objects and 2) a table of aliases between short and long 
+   [module_path]. *)
+
+let rec init_env_seb loc abs = function 
+  | l, SEBmodule mb -> 
+      init_env_module loc (option_app (fun mp -> MPdot (mp,l)) abs) mb 
+  | l, SEBmodtype mtb -> init_env_modtype loc mtb 
+  | _ -> () 
+
+and init_env_module loc abs mb = 
+  option_iter (init_env_meb loc abs) mb.mod_expr
+
+and init_env_meb loc abs = function 
   | MEBident mp -> ()
+  | MEBapply (meb, meb',_) -> 
+      init_env_meb loc None meb; init_env_meb loc None meb'
   | MEBfunctor (mbid, mtb, meb) -> 
       cur_env := add_functor mbid mtb !cur_env; 
-      print_meb meb 
+      init_env_modtype loc mtb; 
+      init_env_meb loc None meb 
   | MEBstruct (msid, msb) -> 
-      let mp_old = !mp_short in 
-      mp_short := MPself msid; 
-      cur_env := add_structure !mp_short msb !cur_env;
-      msg (str "Begin Struct " ++ str (string_of_mp !mp_short) ++ fnl ());
-      print_msb msb;
-      msg (str "End Struct " ++ str  (string_of_mp !mp_short) ++ fnl ());
-      mp_short := mp_old
-  | MEBapply (meb, meb',_) -> 
-      print_meb meb; msg (str "@" ++ fnl ()); print_meb meb'
-
-and print_modtype l mtb = 
-  msg (str "Begin Module Type " ++ pr_label l ++ fnl ());
-  (match mtb with 
-     | MTBident mp -> ()
-     | MTBfunsig (mbid, mtb, mtb') -> 
-	 cur_env := add_functor mbid mtb !cur_env; 
-	 print_modtype l mtb'
-     | MTBsig (msid, sign) -> 
-	 let mp_old = !mp_short in
-	 mp_short := MPself msid; 
-	 cur_env := Modops.add_signature !mp_short sign !cur_env;
-	 msg (str "Begin Sig " ++ str (string_of_mp !mp_short) ++ fnl ());
-	 print_sign sign;
-	 msg (str "End Sig " ++ str  (string_of_mp !mp_short) ++ fnl ());
-	 mp_short := mp_old);
-  msg (str "End Module Type " ++ pr_label l ++ fnl ())
-
-and print_sign = function 
-  | [] -> () 
-  | spec :: sign -> print_spec spec; print_sign sign 
+      let loc = MPself msid in 
+      cur_env := add_structure loc msb !cur_env;
+      option_iter (add_aliases loc) abs; 
+      List.iter (init_env_seb loc abs) msb
+
+and init_env_modtype loc = function 
+  | MTBident mp -> ()
+  | MTBfunsig (mbid, mtb, mtb') -> 
+      cur_env := add_functor mbid mtb !cur_env; 
+      init_env_modtype loc mtb; 
+      init_env_modtype loc mtb'
+  | MTBsig (msid, sign) -> 
+      let loc = MPself msid in
+      cur_env := Modops.add_signature loc sign !cur_env;
+      List.iter (init_env_spec loc) sign
 	
-and print_spec = function 
-  | l, SPBconst {const_type=t} -> 
-      msg (str "Cst " ++ pr_label l ++ str " : " ++ pr_term t ++ fnl ())
-  | l, SPBmind mind -> 
-       let t = Inductive.type_of_inductive !cur_env ((std_kn !mp_short l),0) in 
-       msg (str "Ind " ++ pr_label l ++ str " : " ++ pr_term t ++ fnl ()) 
-  | l, SPBmodule {msb_modtype=mtb} -> print_modtype l mtb 
-  | l, SPBmodtype mtb -> print_modtype l mtb
-
+and init_env_spec loc = function 
+  | l, SPBmodule {msb_modtype=mtb} -> init_env_modtype loc mtb 
+  | l, SPBmodtype mtb -> init_env_modtype loc mtb
+  | _ -> ()
 
-let print_all () = 
+let init_env l =
   cur_env := Global.env (); 
-  mp_short := initial_path; 
   List.iter 
-    (fun (d,meb) -> 
-       msg (str "Library " ++ pr_dirpath d ++ fnl ()); print_meb meb) 
-    (environment_until None); 
-  msg (str "Toplevel" ++ fnl ()); print_meb (toplevel ())
+    (fun (mp,meb) -> init_env_meb (current_toplevel ()) (Some mp) meb) l
 
-(* 
+(*s The extraction pass. *)
 
 type visit = { mutable kn : KNset.t; mutable mp : MPset.t }
 
-let in_kn kn v = KNset.mem kn v.kn
-let in_mp mp v = MPset.mem mp v.mp
-
-let rec visit_type m eenv t =
-  let rec visit = function
-    | Tglob (r,l) -> visit_reference m eenv r; List.iter visit l  
-    | Tarr (t1,t2) -> visit t1; visit t2
-    | Tvar _ | Tdummy | Tunknown | Tcustom _ -> ()
-    | Tmeta _ | Tvar' _ -> assert false 
-  in
-  visit t
-    
-and visit_ast m eenv a =
-  let rec visit = function
-    | MLglob r -> visit_reference m eenv r
-    | MLapp (a,l) -> visit a; List.iter visit l
-    | MLlam (_,a) -> visit a
-    | MLletin (_,a,b) -> visit a; visit b
-    | MLcons (r,l) -> visit_reference m eenv r; List.iter visit l
-    | MLcase (a,br) -> 
-	visit a; 
-	Array.iter (fun (r,_,a) -> visit_reference m eenv r; visit a) br
-    | MLfix (_,_,l) -> Array.iter visit l
-    | MLcast (a,t) -> visit a; visit_type m eenv t
-    | MLmagic a -> visit a
-    | MLrel _ | MLdummy | MLexn _ | MLcustom _ -> ()
-  in
-  visit a
-
-and visit_inductive m eenv inds =
-  let visit_constructor (_,tl) = List.iter (visit_type m eenv) tl in
-  let visit_ind (_,_,cl) = List.iter visit_constructor cl in
-  List.iter visit_ind inds
-
-and visit_decl m eenv = function
-  | Dind (inds,_) -> visit_inductive m eenv inds
-  | Dtype (_,_,t) -> visit_type m eenv t
-  | Dterm (_,a,t) -> visit_ast m eenv a; visit_type m eenv t
-  | Dfix (_,c,t) -> 
-      Array.iter (visit_ast m eenv) c;
-      Array.iter (visit_type m eenv) t
-  | _ -> ()
-
-
-let rec get_structure_elem_references = function 
-  | SEind ml_ind -> 
-      
-let rec extract_msb mp all v = function 
-  | [] -> [] 
-  | (l,seb) -> 
-      let ml_msb = extract_msb v in 
-      match seb with 
-	| SEBconst cb -> 
-	    let kn = std_kn mp l in 
-	    if all || in_kn kn v then 
-	      let ml_se = extraction_constant_body kn cb in 
-	      get_structure_elem_references ml_se v; 
-	      ml_se :: ml_msb
-	    else ml_msb
-	| SEBmind mib ->
-	    let kn = std_kn mp l in 
-	    if all || in_kn kn v then 
-	      let ml_se = extraction_inductive_body kn mib in
-	      search_visit ml_se v;
-	      ml_se :: ml_msb 
-	    else ml_msb
-	| SEBmodule mb -> 
-	    let mp = MPdot (mp,l) in 
-	    if all || in_mp mp v then 
-	      SEmodule (extraction_module mp true v m) :: ml_msb
-	    else msb
-	| SEBmodtype mtb ->
-	    let kn = std_kn mp l in
-	    if all || in_kn kn v then 
-	      SEmodtype (extraction_mtb (MPdot (mp,l)) true v m) :: ml_msb
-	    else msb
-
-
-let mono_environment kn_set = 
-  let add_mp kn mpset = KNset.union (sub_modpath (modpath kn)) mpset
-  let kn_to_visit = ref kn_set 
-  and mp_to_visit = ref (KNset.fold add_mp kn_set MPset.empty)
-  in 
-  
-  let rec extract_structure_body = 
+let in_kn v kn = KNset.mem (long_kn kn) v.kn
+let in_mp v mp = MPset.mem (long_mp mp) v.mp
+
+let visit_ref v r = 
+  let kn = long_kn (kn_of_r r) in 
+  v.kn <- KNset.add kn v.kn; 
+  v.mp <- MPset.union (prefixes_mp (modpath kn)) v.mp
+
+exception Impossible
+
+let check_arity cb = 
+  if Reduction.is_arity !cur_env cb.const_type then raise Impossible
+
+let check_fix cb i = 
+  match cb.const_body with 
+    | None -> raise Impossible
+    | Some lbody -> 
+	match kind_of_term (Declarations.force lbody) with 
+	  | Fix ((_,j),recd) when i=j -> check_arity cb; (true,recd)
+	  | CoFix (j,recd) when i=j -> check_arity cb; (false,recd)
+	  | _ -> raise Impossible
+
+let factor_fix l cb msb = 
+  let _,recd as check = check_fix cb 0 in 
+  let n = Array.length (let fi,_,_ = recd in fi) in
+  if n = 1 then [|l|], recd, msb
+  else begin 
+    if List.length msb < n-1 then raise Impossible; 
+    let msb', msb'' = list_chop (n-1) msb in 
+    let labels = Array.make n l in 
+    list_iter_i 
+      (fun j -> 
+	 function 
+	   | (l,SEBconst cb') -> 
+	       if check <> check_fix cb' (j+1) then raise Impossible; 
+	       labels.(j+1) <- l; 
+	   | _ -> raise Impossible) msb'; 
+    labels, recd, msb''
+  end
 
+let logical_decl = function 
+  | Dterm (_,MLdummy,Tdummy) -> true
+  | Dtype (_,[],Tdummy) -> true 
+  | Dfix (_,av,tv) -> 
+      (array_for_all ((=) MLdummy) av) && (array_for_all ((=) Tdummy) tv)
+  | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+  | _ -> false
 
-  let top = toplevel_structure_body ()
+let logical_spec = function 
+  | Stype (_, [], Some Tdummy) -> true
+  | Sval (_,Tdummy) -> true
+  | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+  | _ -> false
 
-*)
+let get_decl_references v d = 
+  let f = visit_ref v in decl_iter_references f f f d
 
-(*s Auxiliary functions dealing with modules. *)
+let get_spec_references v s = 
+  let f = visit_ref v in spec_iter_references f f f s
 
-let dir_module_of_id m = 
-  try 
-    Nametab.full_name_module (make_short_qualid m) 
-  with Not_found ->  
-    errorlabstrm "module_message"
-      (str "Module" ++ spc () ++ pr_id m ++ spc () ++ str "not found.") 
-
-(*s Module name clash verification. *)
-
-let clash_error sn n1 n2 = 
-  errorlabstrm "clash_module_message"
-    (str ("There are two Coq modules with ML name " ^ sn ^" :") ++ 
-     fnl () ++ str ("  "^(string_of_dirpath n1)) ++ 
-     fnl () ++ str ("  "^(string_of_dirpath n2)) ++ 
-     fnl () ++ str "This is not allowed in ML. Please do some renaming first.")
-    
-let check_r m sm r = 
-  let rlm = long_module r in 
-  let rsm = List.hd (repr_dirpath rlm) in 
-  if (String.capitalize (string_of_id rsm)) = sm && m <> rlm
-  then clash_error sm m rlm
-    
-let check_decl m sm = function 
-  | Dterm (r,_,_) -> check_r m sm r 
-  | Dtype (r,_,_) -> check_r m sm r
-  | Dind (kn,_) -> check_r m sm (IndRef (kn,0))
-  | DcustomTerm (r,_) ->  check_r m sm r
-  | DcustomType (r,_) ->  check_r m sm r	
-  | Dfix(rv,_,_) -> Array.iter (check_r m sm) rv 
-
-(* [check_one_module] checks that no module names in [l] clashes with [m]. *)
-
-let check_one_module m l = 
-  let sm = String.capitalize (string_of_id (snd (split_dirpath m))) in 
-  List.iter (check_decl m sm) l
-
-(* [check_modules] checks if there are conflicts within the set [m] 
-   of modules dirpath. *) 
-
-let check_modules m = 
-  let map = ref Idmap.empty in 
-  Dirset.iter 
-    (fun m -> 
-       let sm = String.capitalize (string_of_id (snd (split_dirpath m))) in 
-       let idm = id_of_string sm in 
-       try 
-	 let m' = Idmap.find idm !map in clash_error sm m m'
-       with Not_found -> map := Idmap.add idm m !map) m
+let rec extract_msb v all loc = function 
+  | [] -> [] 
+  | (l,SEBconst cb) :: msb -> 
+      (try 
+	 let vl,recd,msb = factor_fix l cb msb in 
+	 let vkn = Array.map (make_kn loc empty_dirpath) vl in
+	 let vkn = Array.map long_kn vkn in
+	 let ms = extract_msb v all loc msb in 
+	 let b = array_exists (in_kn v) vkn in 
+	 if all || b then 
+	   let d = extract_fixpoint !cur_env vkn recd in 
+	   if (not b) && (logical_decl d) then ms 
+	   else begin get_decl_references v d;  (l,SEdecl d) :: ms end
+	 else ms
+       with Impossible ->
+	 let ms = extract_msb v all loc msb in 
+	 let kn = make_kn loc empty_dirpath l in 
+	 let b = in_kn v kn in 
+	 if all || b then 
+	   let d = extract_constant !cur_env kn cb in
+	   if (not b) && (logical_decl d) then ms 
+	   else begin get_decl_references v d; (l,SEdecl d) :: ms end
+	 else ms)
+  | (l,SEBmind mib) :: msb ->
+      let ms = extract_msb v all loc msb in
+      let kn = make_kn loc empty_dirpath l in 
+      let b = in_kn v kn in 
+      if all || b then 
+	let d = Dind (kn, extract_inductive !cur_env kn) in 
+	if (not b) && (logical_decl d) then ms 
+	else begin get_decl_references v d; (l,SEdecl d) :: ms end
+      else ms
+  | (l,SEBmodule mb) :: msb -> 
+      let ms = extract_msb v all loc msb in
+      let loc = MPdot (loc,l) in 
+      if all || in_mp v loc then 
+	(l,SEmodule (extract_module v true mb)) :: ms
+      else ms
+  | (l,SEBmodtype mtb) :: msb ->
+      let ms = extract_msb v all loc msb in
+      let kn = make_kn loc empty_dirpath l in
+      if all || in_kn v kn then 
+	(l,SEmodtype (extract_mtb v mtb)) :: ms
+      else ms
+
+and extract_meb v all = function 
+  | MEBident mp -> MEident mp 
+  | MEBapply (meb, meb',_) -> 
+      MEapply (extract_meb v true meb, extract_meb v true meb')
+  | MEBfunctor (mbid, mtb, meb) -> 
+      MEfunctor (mbid, extract_mtb v mtb, extract_meb v true meb)
+  | MEBstruct (msid, msb) -> 
+      MEstruct (msid, extract_msb v all (MPself msid) msb) 
+
+and extract_module v all mb = 
+  { ml_mod_expr = option_app (extract_meb v all) mb.mod_expr;  
+    ml_mod_type = (match mb.mod_user_type with 
+		     | None -> extract_mtb v mb.mod_type
+		     | Some mtb -> extract_mtb v mtb);
+    ml_mod_equiv = mb.mod_equiv }
+	
+and extract_mtb v = function 
+  | MTBident kn -> MTident kn 
+  | MTBfunsig (mbid, mtb, mtb') -> 
+      MTfunsig (mbid, extract_mtb v mtb, extract_mtb v mtb') 
+  | MTBsig (msid, msig) -> 
+      MTsig (msid, extract_msig v (MPself msid) msig) 
     
-(*s Recursive computation of the global references to extract. 
-    We use a set of functions visiting the extracted objects in
-    a depth-first way ([visit_type], [visit_ast] and [visit_decl]).
-    We maintain an (imperative) structure [extracted_env] containing
-    the set of already visited references and the list of 
-    references to extract. The entry point is the function [visit_reference]:
-    it first normalizes the reference, and then check it has already been 
-    visisted; if not, it adds it to the set of visited references, then
-    recursively traverses its extraction and finally adds it to the 
-    list of references to extract. *) 
-
-type extracted_env = {
-  mutable visited : Refset.t;
-  mutable to_extract : global_reference list;
-  mutable modules : Dirset.t
-}
-
-let empty () = 
-  { visited = ml_extractions (); 
-    to_extract = []; 
-    modules = Dirset.empty }
-
-let rec visit_reference m eenv r =
-  let r' = match r with
-    | ConstructRef ((sp,_),_) -> IndRef (sp,0)
-    | IndRef (sp,i) -> if i = 0 then r else IndRef (sp,0)
-    | _ -> r
-  in
-  if not (Refset.mem r' eenv.visited) then begin
-    (* we put [r'] in [visited] first to avoid loops in inductive defs 
-       and in module extraction *)
-    eenv.visited <- Refset.add r' eenv.visited;
-    if m then begin 
-      let m_name = Declare.library_part r' in 
-      if not (Dirset.mem m_name eenv.modules) then begin
-	eenv.modules <- Dirset.add m_name eenv.modules;
-	List.iter (visit_reference m eenv) (module_contents m_name)
+and extract_msig v loc = function 
+  | [] -> [] 
+  | (l,SPBconst cb) :: msig -> 
+      let kn = make_kn loc empty_dirpath l in 
+      let s = extract_constant_spec !cur_env kn cb in 
+      if logical_spec s then extract_msig v loc msig
+      else begin
+	get_spec_references v s; 
+	(l,Spec s) :: (extract_msig v loc msig)
       end
-    end;
-    visit_decl m eenv (extract_declaration r);
-    eenv.to_extract <- r' :: eenv.to_extract
-  end
-
-(* and visit_fixpoint m eenv r = 
-  match (kind_of_term (constant_value (Global.env()) (kn_of_r r))) with 
-    | Fix (_,(f,_,_)) -> 
-	(try 
-	   let d = dirpath (sp_of_global None r) in 
-	   let v = Array.map (fun id -> locate (make_qualid d id)) f in *)
-
-and visit_type m eenv t =
-  let rec visit = function
-    | Tglob (r,l) -> visit_reference m eenv r; List.iter visit l  
-    | Tarr (t1,t2) -> visit t1; visit t2
-    | Tvar _ | Tdummy | Tunknown | Tcustom _ -> ()
-    | Tmeta _ | Tvar' _ -> assert false 
-  in
-  visit t
-    
-and visit_ast m eenv a =
-  let rec visit = function
-    | MLglob r -> visit_reference m eenv r
-    | MLapp (a,l) -> visit a; List.iter visit l
-    | MLlam (_,a) -> visit a
-    | MLletin (_,a,b) -> visit a; visit b
-    | MLcons (r,l) -> visit_reference m eenv r; List.iter visit l
-    | MLcase (a,br) -> 
-	visit a; 
-	Array.iter (fun (r,_,a) -> visit_reference m eenv r; visit a) br
-    | MLfix (_,_,l) -> Array.iter visit l
-    | MLcast (a,t) -> visit a; visit_type m eenv t
-    | MLmagic a -> visit a
-    | MLrel _ | MLdummy | MLexn _ | MLcustom _ -> ()
-  in
-  visit a
-
-and visit_inductive m eenv ind =
-  let visit_constructor tl = List.iter (visit_type m eenv) tl in
-  let visit_packet p = Array.iter visit_constructor p.ip_types in
-  Array.iter visit_packet ind.ind_packets
-
-and visit_decl m eenv = function
-  | Dind (_,ind) -> visit_inductive m eenv ind
-  | Dtype (_,_,t) -> visit_type m eenv t
-  | Dterm (_,a,t) -> visit_ast m eenv a; visit_type m eenv t
-  | Dfix (_,c,t) -> 
-      Array.iter (visit_ast m eenv) c;
-      Array.iter (visit_type m eenv) t
-  | _ -> ()
-	
-(*s Recursive extracted environment for a list of reference: we just
-    iterate [visit_reference] on the list, starting with an empty
-    extracted environment, and we return the reversed list of 
-    references in the field [to_extract], and the visited_modules in 
-    case of recursive module extraction *)
-
-let extract_env rl =
-  let eenv = empty () in
-  List.iter (visit_reference false eenv) rl;
-  List.rev eenv.to_extract
-
-let modules_extract_env m =
-  let eenv = empty () in
-  eenv.modules <- Dirset.singleton m;
-  List.iter (visit_reference true eenv) (module_contents m);
-  eenv.modules, List.rev eenv.to_extract
-
-(* let toplevel_contents () = 
-  segment_contents (contents_after None)
+  | (l,SPBmind cb) :: msig -> 
+      let kn = make_kn loc empty_dirpath l in 
+      let s = Sind (kn, extract_inductive !cur_env kn) in 
+      if logical_spec s then extract_msig v loc msig
+      else begin 
+	get_spec_references v s; 
+	(l,Spec s) :: (extract_msig v loc msig)
+      end
+  | (l,SPBmodule {msb_modtype=mtb}) :: msig -> 
+      (l,Smodule (extract_mtb v mtb)) :: (extract_msig v loc msig)
+  | (l,SPBmodtype mtb) :: msig -> 
+      (l,Smodtype (extract_mtb v mtb)) :: (extract_msig v loc msig)
 
-let extract_env rl = 
-  let modules = List.rev (loaded_libraries ()) in 
-  let toplevel_list = toplevel_contents () in 
-  let modules_list = *)
+(* Searching one [ml_decl] in a [ml_structure] by its [kernel_name] *)
 
+let get_decl_in_structure r struc = 
+  try 
+    let kn = kn_of_r r in 
+    let base_mp,ll = labels_of_kn (long_kn kn) in 
+    if not (at_toplevel base_mp) then error_not_visible r;
+    let sel = List.assoc base_mp struc in
+    let rec go ll sel = match ll with 
+      | [] -> assert false
+      | l :: ll -> 
+	  match List.assoc l sel with 
+	    | SEdecl d -> d 
+	    | SEmodtype m -> assert false
+	    | SEmodule m -> 
+		match m.ml_mod_expr with 
+		  | Some (MEstruct (_,sel)) -> go ll sel 
+		  | _ -> error_not_visible r 
+    in go ll sel
+  with Not_found -> assert false
 
 (*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]. *)
 
-let decl_of_refs refs = List.map extract_declaration (extract_env refs)
-
-let print_user_extract r = 
-  msgnl (str "User defined extraction:" ++ 
-	   spc () ++ str (find_ml_extraction r) ++ fnl ())
+let unpack = function MEstruct (_,sel) -> sel | _ -> assert false 
 
-let decl_in_r r0 = function 
-  | Dterm (r,_,_) -> r = r0
-  | Dtype (r,_,_) -> r = r0
-  | Dind (kn, _) -> kn = kn_of_r r0
-  | DcustomTerm (r,_) ->  r = r0 
-  | DcustomType (r,_) ->  r = r0 
-  | Dfix (rv,_,_) -> array_exists ((=) r0) rv
+let mono_environment refs = 
+  let l = environment_until None in 
+  init_env l; 
+  let v = 
+    let kns = List.fold_right (fun r -> KNset.add (kn_of_r r)) refs KNset.empty 
+    in let add_mp kn = MPset.union (prefixes_mp (modpath kn)) 
+    in { kn = kns; mp = KNset.fold add_mp kns MPset.empty } 
+  in 
+  List.rev_map (fun (mp,m) -> mp, unpack (extract_meb v false m)) (List.rev l)
 
-let extraction qid =
+let extraction qid = 
+  if is_something_opened () then error_section (); 
   let r = Nametab.global qid in 
-  if is_ml_extraction r then
-    print_user_extract r 
-  else 
+  if is_custom r then
+    msgnl (str "User defined extraction:" ++ spc () ++ 
+	   str (find_custom r) ++ fnl ()) 
+  else begin 
     let prm = 
       { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in 
-    let decls = optimize prm (decl_of_refs [r]) in 
-    let d = list_last decls in
-    let d = if (decl_in_r r d) then d 
-    else List.find (decl_in_r r) decls in 
-    set_keywords ();
-    create_mono_renamings decls; 
-    msgnl (pp_decl () d)
+    let kn = kn_of_r r in 
+    let struc = optimize_struct prm None (mono_environment [r]) in 
+    let d = get_decl_in_structure r struc in 
+    print_one_decl struc (long_mp (modpath kn)) d;
+    reset_tables ()
+  end
 
 (*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. *)
 
 let mono_extraction (f,m) vl = 
+  if is_something_opened () then error_section (); 
   let refs = List.map Nametab.global vl in
   let prm = {modular=false; mod_name = m; to_appear= refs} in
-  let decls = decl_of_refs refs in 
-  let decls = add_ml_decls prm decls in 
-  let decls = optimize prm decls in
-  extract_to_file f prm decls
+  let struc = optimize_struct prm None (mono_environment refs) in 
+  print_structure_to_file f prm struc; 
+  reset_tables ()
 
 let extraction_rec = mono_extraction (None,id_of_string "Main")
 
 (*s Extraction to a file (necessarily recursive). 
-    The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn].
-    We just call [extract_to_file] on the saturated environment. *)
+    The vernacular command is 
+    \verb!Extraction "file"! [qualid1] ... [qualidn].*)
 
 let lang_suffix () = match lang () with 
-  | Ocaml -> ".ml"
-  | Haskell -> ".hs"
-  | Scheme -> ".scm"
+  | Ocaml -> ".ml",".mli"
+  | Haskell -> ".hs",".hi"
+  | Scheme -> ".scm",".scm"
   | Toplevel -> assert false
 
 let filename f = 
-  let s = lang_suffix () in 
+  let s,s' = lang_suffix () in
   if Filename.check_suffix f s then 
-    Some f,id_of_string (Filename.chop_suffix f s) 
-  else Some (f^s),id_of_string f
-
-let toplevel_error () = 
-  errorlabstrm "toplevel_extraction_language"
-    (str "Toplevel pseudo-ML language cannot be used outside Coq toplevel." 
-     ++ fnl () ++
-     str "You should use Extraction Language Ocaml or Haskell before.") 
+    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 toplevel_error () 
+  if lang () = Toplevel then error_toplevel () 
   else mono_extraction (filename f) vl
 
 (*s Extraction of a module. The vernacular command is 
   \verb!Extraction Module! [M]. *) 
 
-let decl_in_m m = function 
-  | Dterm (r,_,_) -> m = long_module r
-  | Dtype (r,_,_) -> m = long_module r
-  | Dind (kn,_) -> m = long_module (IndRef (kn,0))
-  | DcustomTerm (r,_) ->  m = long_module r
-  | DcustomType (r,_) ->  m = long_module r
-  | Dfix (rv,_,_) -> m = long_module rv.(0)
-
 let module_file_name m = match lang () with 
-  | Ocaml -> (String.uncapitalize (string_of_id m)) ^ ".ml"
-  | Haskell -> (String.capitalize (string_of_id m)) ^ ".hs"
+  | 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 scheme_error () = 
-  errorlabstrm "scheme_extraction_language"
-    (str "No Scheme modular extraction available yet." ++ fnl ())
+let dir_module_of_id m = 
+  try Nametab.full_name_module (make_short_qualid m) 
+  with Not_found -> error_unknown_module m
 
 let extraction_module m =
+  if is_something_opened () then error_section (); 
   match lang () with 
-    | Toplevel -> toplevel_error ()
-    | Scheme -> scheme_error ()
+    | Toplevel -> error_toplevel ()
+    | Scheme -> error_scheme ()
     | _ -> 
 	let dir_m = dir_module_of_id m in 
-	let f = module_file_name m in
+	let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in 
+	let l = environment_until (Some dir_m) in 
+	init_env l;
+	let mp,meb = list_last l in 
+	let struc = [mp, unpack (extract_meb v true meb)] in 
+	let extern_decls = 
+	  let filter kn l = 
+	    if base_mp (modpath kn) = mp then l else r_of_kn !cur_env kn :: l 
+	  in extract_env (KNset.fold filter v.kn [])
+	in 
 	let prm = {modular=true; mod_name=m; to_appear=[]} in 
-	let rl = module_contents dir_m in 
-	let decls = optimize prm (decl_of_refs rl) in
-	let decls = add_ml_decls prm decls in 
-	check_one_module dir_m decls; 
-	let decls = List.filter (decl_in_m dir_m) decls in
-	extract_to_file (Some f) prm decls
+	let struc = optimize_struct prm (Some extern_decls) struc in 
+	print_structure_to_file (Some (module_file_name m)) prm struc; 
+	reset_tables ()
 	  
 (*s Recursive Extraction of all the modules [M] depends on. 
   The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
 
 let recursive_extraction_module m =
+  if is_something_opened () then error_section (); 
   match lang () with 
-    | Toplevel -> toplevel_error () 
-    | Scheme -> scheme_error () 
+    | Toplevel -> error_toplevel () 
+    | Scheme -> error_scheme () 
     | _ -> 
 	let dir_m = dir_module_of_id m in 
-	let modules,refs = modules_extract_env dir_m in
-	check_modules modules; 
+	let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in 
+	let l = environment_until (Some dir_m) in 
+	init_env l; 
+	let struc = 
+	  let select l (mp,meb) = 
+	    if in_mp v mp then (mp, unpack (extract_meb v true meb)) :: l else l
+	  in List.fold_left select [] (List.rev l)
+	in 
 	let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
-	let decls = optimize dummy_prm (decl_of_refs refs) in
-	let decls = add_ml_decls dummy_prm decls in
-	Dirset.iter 
-	  (fun m ->
-	     let short_m = snd (split_dirpath m) in
-	     let f = module_file_name short_m in 
-	     let prm = {modular=true;mod_name=short_m;to_appear=[]} in 
-	     let decls = List.filter (decl_in_m m) decls in
-	     if decls <> [] then extract_to_file (Some f) prm decls)
-	  modules
+	let struc = optimize_struct dummy_prm None struc in 
+	let rec print = function 
+	  | [] -> () 
+	  | (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 l 
+	  | _ -> assert false
+	in print struc; 
+	reset_tables ()
+
+
+
+
+
 
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index 1dcd9abef..625afc7d1 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -18,20 +18,3 @@ val extraction_rec : reference list -> unit
 val extraction_file : string -> reference list -> unit
 val extraction_module : identifier -> unit
 val recursive_extraction_module : identifier -> unit
-
-(* debug modules -- en cours *)
-
-open Declarations
-
-val cur_env : Environ.env ref 
-val mp_short : module_path ref 
-val toplevel : unit -> module_expr_body
-val environment_until : dir_path option -> (dir_path * module_expr_body) list 
-val print_seb : label * structure_elem_body -> unit 
-val print_msb : module_structure_body -> unit 
-val print_module : label -> module_body -> unit
-val print_meb : module_expr_body  -> unit
-val print_modtype : label -> module_type_body  -> unit
-val print_sign : module_signature_body  -> unit
-val print_spec : label * specification_body  -> unit
-val print_all : unit -> unit
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 363d6c177..c676c26c2 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -37,7 +37,7 @@ let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
 
 let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
 
-let is_axiom kn = (Global.lookup_constant kn).const_body = None
+let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None
 
 (*S Generation of flags and signatures. *)
 
@@ -149,7 +149,6 @@ let parse_ind_args si args relmax =
 
 let rec extract_type env db j c args = 
   match kind_of_term (whd_betaiotazeta c) with
-    | Var _ -> error_section ()
     | App (d, args') ->
 	(* We just accumulate the arguments. *)
 	extract_type env db j d (Array.to_list args' @ args)
@@ -183,31 +182,32 @@ let rec extract_type env db j c args =
 	       if n > List.length db then Tunknown 
 	       else let n' = List.nth db (n-1) in 
 	       if n' = 0 then Tunknown else Tvar n')
-    | Const kn when is_ml_extraction (ConstRef kn) -> 
-	assert (args = []); 
-	Tglob (ConstRef kn,[])
-    | Const kn when is_axiom kn -> 
-	(* There are two kinds of informative axioms here, *)
-	(* - the types that should be realized via [Extract Constant] *)
-	(* - the type schemes that are not realizable (yet). *) 
-	if args = [] then error_axiom (ConstRef kn)
-	else error_axiom_scheme (ConstRef kn) 
-    | Const kn ->
-	let body = constant_value env kn in 
-	let mlt1 = extract_type env db j (applist (body, args)) [] in 
-	(match mlt_env (ConstRef kn) with 
-	   | Some mlt ->
-	       if mlt = Tdummy then Tdummy
-               else 
-		 let s = type_sign env (constant_type env kn) in 
-		 let mlt2 = extract_type_app env db (ConstRef kn,s) args in 
-		 (* ML type abbreviation behave badly with respect to Coq *)
-		 (* reduction. Try to find the shortest correct answer. *) 
-		 if type_eq mlt_env mlt1 mlt2 then mlt2 else mlt1
-	   | None -> mlt1)
+    | Const kn -> 
+	let kn = long_kn kn in 
+	let r = ConstRef kn in 
+	if is_custom r then Tglob (r,[])
+	else if is_axiom env kn then 
+	  (* There are two kinds of informative axioms here, *)
+	  (* - the types that should be realized via [Extract Constant] *)
+	  (* - the type schemes that are not realizable (yet). *) 
+	  if args = [] then error_axiom r else error_axiom_scheme r
+	else 
+	  let body = constant_value env kn in 
+	  let mlt1 = extract_type env db j (applist (body, args)) [] in 
+	  (match mlt_env env r with 
+	     | Some mlt ->
+		 if mlt = Tdummy then Tdummy
+		 else 
+		   let s = type_sign env (constant_type env kn) in 
+		   let mlt2 = extract_type_app env db (r,s) args in 
+		   (* ML type abbreviation behave badly with respect to Coq *)
+		   (* reduction. Try to find the shortest correct answer. *) 
+		   if type_eq (mlt_env env) mlt1 mlt2 then mlt2 else mlt1
+	     | None -> mlt1)
     | Ind ((kn,i) as ip) ->
-	let s = (extract_inductive kn).ind_packets.(i).ip_sign in  
-	extract_type_app env db (IndRef ip,s) args
+	let kn = long_kn kn in
+	let s = (extract_ind env kn).ind_packets.(i).ip_sign in  
+	extract_type_app env db (IndRef (kn,i),s) args
     | Case _ | Fix _ | CoFix _ -> Tunknown
     | _ -> assert false
 
@@ -259,15 +259,14 @@ and extract_type_scheme env db c p =
 
 (*S Extraction of an inductive type. *)
 
-and extract_inductive kn =
+and extract_ind env kn = (* kn is supposed to be in long form *)
   try lookup_ind kn with Not_found -> 
-    add_recursors kn; 
-    let env = Global.env () in 
-    let (mib,mip) = Global.lookup_inductive (kn,0) in
+    let mib = Environ.lookup_mind kn env in 
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
-    let npar = mip.mind_nparams in
-    let epar = push_rel_context mip.mind_params_ctxt env in
+    let mip0 = mib.mind_packets.(0) in 
+    let npar = mip0.mind_nparams in
+    let epar = push_rel_context mip0.mind_params_ctxt env in
     (* First pass: we store inductive signatures together with *)
     (* their type var list. *)
     let packets = 
@@ -276,7 +275,12 @@ and extract_inductive kn =
 	   let b = mip.mind_sort <> (Prop Null) in 
 	   let s,v = if b then type_sign_vl env mip.mind_nf_arity else [],[] in
 	   let t = Array.make (Array.length mip.mind_nf_lc) [] in 
-	   { ip_logical = (not b); ip_sign = s; ip_vars = v; ip_types = t }) 
+	   { ip_typename = mip.mind_typename;
+	     ip_consnames = mip.mind_consnames;
+	     ip_logical = (not b); 
+	     ip_sign = s; 
+	     ip_vars = v; 
+	     ip_types = t }) 
 	mib.mind_packets 
     in 
     add_ind kn {ind_info = Standard; ind_nparams = npar; ind_packets = packets};
@@ -305,15 +309,17 @@ and extract_inductive kn =
 	if p.ip_logical then raise (I Standard);
 	if Array.length p.ip_types <> 1 then raise (I Standard);
 	let typ = p.ip_types.(0) in 
-	let l = List.filter (type_neq mlt_env Tdummy) typ in 
+	let l = List.filter (type_neq (mlt_env env) Tdummy) typ in 
 	if List.length l = 1 && not (type_mem_kn kn (List.hd l)) 
 	then raise (I Singleton); 
-	if l = [] then raise (I Standard); 
+	if l = [] then raise (I Standard);
+	let ip = (kn, 0) in 
+	if is_custom (IndRef ip) then raise (I Standard); 
 	let projs = 
-	  try (find_structure (kn,0)).s_PROJ 
+	  try (find_structure ip).s_PROJ 
 	  with Not_found -> raise (I Standard);
 	in 
-	let s = List.map (type_neq mlt_env Tdummy) typ in
+	let s = List.map (type_neq (mlt_env env) Tdummy) typ in
 	let check (_,o) = match o with 
 	  | None -> raise (I Standard)
 	  | Some kn -> ConstRef kn 
@@ -345,14 +351,14 @@ and extract_type_cons env db dbmap c i =
 
 (*s Recording the ML type abbreviation of a Coq type scheme constant. *)
 
-and mlt_env r = match r with 
+and mlt_env env r = match r with 
   | ConstRef kn -> 
+      let kn = long_kn kn in
       (try match lookup_term kn with 
 	 | Dtype (_,vl,mlt) -> Some mlt
 	 | _ -> None
        with Not_found -> 
-	 let env = Global.env() in    
-	 let cb = Global.lookup_constant kn in
+	 let cb = Environ.lookup_constant kn env in
 	 let typ = cb.const_type in
 	 match cb.const_body with
 	   | None -> None
@@ -367,19 +373,22 @@ and mlt_env r = match r with
 		  | _ -> None))
   | _ -> None
 
-let type_expand = type_expand mlt_env
-let type_neq = type_neq mlt_env
-let type_to_sign = type_to_sign mlt_env
-let type_expunge = type_expunge mlt_env
+let type_expand env = type_expand (mlt_env env)
+let type_neq env = type_neq (mlt_env env)
+let type_to_sign env = type_to_sign (mlt_env env)
+let type_expunge env = type_expunge (mlt_env env)
 
 (*s Extraction of the type of a constant. *)
 
-let record_constant_type kn = 
+let record_constant_type env kn opt_typ = 
+  let kn = long_kn kn in 
   try lookup_type kn
   with Not_found -> 
-    let env = Global.env () in 
-    let mlt = extract_type env [] 1 (constant_type env kn) [] in 
-    let schema = (type_maxvar mlt, mlt)
+    let typ = match opt_typ with 
+      | None -> constant_type env kn 
+      | Some typ -> typ 
+    in let mlt = extract_type env [] 1 typ [] 
+    in let schema = (type_maxvar mlt, mlt)
     in add_type kn schema; schema
 
 (*S Extraction of a term. *)
@@ -425,23 +434,23 @@ let rec extract_term env mle mlt c args =
 	  let mle' = Mlenv.push_std_type mle Tdummy in 
 	  ast_pop (extract_term env' mle' mlt c2 args')
     | Const kn ->
-	extract_cst_app env mle mlt kn args
-    | Construct cp ->
-	extract_cons_app env mle mlt cp args
+	extract_cst_app env mle mlt (long_kn kn) args
+    | Construct ((kn,i),j) ->
+	extract_cons_app env mle mlt (((long_kn kn),i),j) args
     | Rel n ->
 	(* As soon as the expected [mlt] for the head is known, *)
 	(* we unify it with an fresh copy of the stored type of [Rel n]. *)
 	let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
 	in extract_app env mle mlt extract_rel args 
-    | Case ({ci_ind=ip},_,c0,br) ->
+    | Case ({ci_ind=(kn,i)},_,c0,br) ->
+	let ip = long_kn kn, i in 
  	extract_app env mle mlt (extract_case env mle (ip,c0,br)) args
     | Fix ((_,i),recd) ->
  	extract_app env mle mlt (extract_fix env mle i recd) args 
     | CoFix (i,recd) ->
  	extract_app env mle mlt (extract_fix env mle i recd) args
     | Cast (c, _) -> extract_term env mle mlt c args
-    | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ -> assert false 
-    | Var _ -> error_section ()
+    | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false 
 
 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) 
 
@@ -477,8 +486,8 @@ and make_mlargs env e s args typs =
 
 and extract_cst_app env mle mlt kn args = 
   (* First, the [ml_schema] of the constant, in expanded version. *) 
-  let nb,t = record_constant_type kn in 
-  let schema = nb, type_expand t in 
+  let nb,t = record_constant_type env kn None in 
+  let schema = nb, type_expand env t in 
   (* Then the expected type of this constant. *)
   let metas = List.map new_meta args in 
   let type_head = type_recomp (metas,mlt) in 
@@ -487,7 +496,7 @@ and extract_cst_app env mle mlt kn args =
     let h = MLglob (ConstRef kn) in 
     put_magic (type_recomp (metas,mlt), instantiation schema) h in
   (* Now, the extraction of the arguments. *)
-  let s = type_to_sign (snd schema) in 
+  let s = type_to_sign env (snd schema) in 
   let ls = List.length s in 
   let la = List.length args in
   let mla = make_mlargs env mle s args metas in 
@@ -519,11 +528,11 @@ and extract_cst_app env mle mlt kn args =
 
 and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   (* First, we build the type of the constructor, stored in small pieces. *)
-  let mi = extract_inductive kn in 
+  let mi = extract_ind env kn in 
   let params_nb = mi.ind_nparams in 
   let oi = mi.ind_packets.(i) in 
   let nb_tvars = List.length oi.ip_vars
-  and types = List.map type_expand oi.ip_types.(j-1) in
+  and types = List.map (type_expand env) oi.ip_types.(j-1) in
   let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in 
   let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
   let type_cons = instantiation (nb_tvars, type_cons) in 
@@ -562,11 +571,10 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
 and extract_case env mle ((kn,i) as ip,c,br) mlt = 
   (* [br]: bodies of each branch (in functional form) *)
   (* [ni]: number of arguments without parameters in each branch *)
-  let ni = mis_constr_nargs ip in
+  let ni = mis_constr_nargs_env env ip in
   let br_size = Array.length br in 
   assert (Array.length ni = br_size); 
-  if br_size = 0 then begin 
-    add_recursors kn; 
+  if br_size = 0 then begin
     MLexn "absurd case"
   end else 
     (* [c] has an inductive type, and is not a type scheme type. *)
@@ -576,7 +584,6 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
       begin 
 	(* Logical singleton case: *)
 	(* [match c with C i j k -> t] becomes [t'] *)
-	add_recursors kn; 
 	assert (br_size = 1);
 	let s = iterate (fun l -> false :: l) ni.(0) [] in
 	let mlt = iterate (fun t -> Tarr (Tdummy, t)) ni.(0) mlt in 
@@ -584,7 +591,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	snd (case_expunge s e)
       end 
     else 
-      let mi = extract_inductive kn in 
+      let mi = extract_ind env kn in 
       let params_nb = mi.ind_nparams in 
       let oi = mi.ind_packets.(i) in 
       let metas = Array.init (List.length oi.ip_vars) new_meta in 
@@ -594,7 +601,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
       (* The extraction of each branch. *)
       let extract_branch i = 
 	(* The types of the arguments of the corresponding constructor. *)
-	let f t = type_subst_vect metas (type_expand t) in 
+	let f t = type_subst_vect metas (type_expand env t) in 
 	let l = List.map f oi.ip_types.(i) in
 	(* Extraction of the branch (in functional form). *)
 	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in 
@@ -618,13 +625,12 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 (*s Extraction of a (co)-fixpoint. *)
 
 and extract_fix env mle i (fi,ti,ci as recd) mlt = 
-  let n = Array.length fi in
   let env = push_rec_types recd env in 
-  let metas = Array.map (fun _ -> new_meta ()) fi in 
-  let magic = needs_magic (mlt, metas.(i)) in 
+  let metas = Array.map new_meta fi in
+  metas.(i) <- mlt; 
   let mle = Array.fold_left Mlenv.push_type mle metas in 
   let ei = array_map2 (extract_maybe_term env mle) metas ci in 
-  put_magic_if magic (MLfix (i, Array.map id_of_name fi, ei))
+  MLfix (i, Array.map id_of_name fi, ei)
 
 (*S ML declarations. *)
 
@@ -646,72 +652,125 @@ let rec decomp_lams_eta env c t =
 
 (*s From a constant to a ML declaration. *)
 
-let extract_constant kn r = 
-  let env = Global.env() in    
-  let cb = Global.lookup_constant kn in
+let extract_std_constant env kn body typ = 
+  (* Decomposing the top level lambdas of [body]. *)
+  let rels,c = decomp_lams_eta env body typ in
+  (* The lambdas names. *)
+  let ids = List.map (fun (n,_) -> id_of_name n) rels in 
+  (* The according Coq environment. *)
+  let env = push_rels_assum rels env in
+  (* The ML part: *)
+  reset_meta_count (); 
+  (* The short type [t] (i.e. possibly with abbreviations). *)
+  let t = snd (record_constant_type env kn (Some typ)) in 
+  (* The real type [t']: without head lambdas, expanded, *)
+  (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
+  let l,t' = type_decomp (type_expand env (var2var' t)) in 
+  let s = List.map ((<>) Tdummy) l in 
+  (* The initial ML environment. *)
+  let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in 
+  (* The real extraction: *)
+  let e = extract_term env mle t' c [] in
+  (* Expunging term and type from dummy lambdas. *) 
+  term_expunge s (ids,e), type_expunge env t
+
+let extract_fixpoint env vkn (fi,ti,ci) = 
+  let n = Array.length vkn in 
+  let types = Array.make n Tdummy
+  and terms = Array.make n MLdummy in 
+  (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
+  let sub = List.rev_map mkConst (Array.to_list vkn) in 
+  for i = 0 to n-1 do 
+    if sort_of env ti.(i) <> InProp then begin 
+      let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
+      terms.(i) <- e; 
+      types.(i) <- t;
+    end 
+  done; 
+  Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) 
+		 
+let extract_constant env kn cb = 
+  let kn = long_kn kn in 
+  let r = ConstRef kn in 
   let typ = cb.const_type in
   match cb.const_body with
     | None -> (* A logical axiom is risky, an informative one is fatal. *) 
         (match flag_of_type env typ with
 	   | (Info,TypeScheme) -> 
-	       if isSort typ then error_axiom r
+	       if isSort typ then 
+		 if is_custom (long_r r) then Dtype (r, [], Tunknown) 
+		 else error_axiom r
 	       else error_axiom_scheme r
-           | (Info,Default) -> error_axiom r 
+           | (Info,Default) -> 
+	       if is_custom (long_r r) then 
+		 let t = snd (record_constant_type env kn (Some typ)) in 
+		 Dterm (r, MLexn "axiom!", type_expunge env t) 
+	       else error_axiom r
            | (Logic,TypeScheme) -> warning_axiom r; Dtype (r, [], Tdummy)
 	   | (Logic,Default) -> warning_axiom r; Dterm (r, MLdummy, Tdummy))
-    | Some l_body ->
+    | Some body ->
 	(match flag_of_type env typ with
 	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy)
 	   | (Logic, TypeScheme) -> Dtype (r, [], Tdummy)
 	   | (Info, Default) -> 
-	       let body = Declarations.force l_body in
-	       (* Decomposing the top level lambdas of [body]. *)
-	       let rels,c = decomp_lams_eta env body typ in
-	       (* The lambdas names. *)
-	       let ids = List.map (fun (n,_) -> id_of_name n) rels in 
-	       (* The according Coq environment. *)
-	       let env = push_rels_assum rels env in
-	       (* The ML part: *)
-	       reset_meta_count (); 
-	       (* The short type [t] (i.e. possibly with abbreviations). *)
-	       let t = snd (record_constant_type kn) in 
-	       (* The real type [t']: without head lambdas, expanded, *)
-	       (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
-	       let l,t' = type_decomp (type_expand (var2var' t)) in 
-	       let s = List.map ((<>) Tdummy) l in 
-	       (* The initial ML environment. *)
-	       let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in 
-	       (* The real extraction: *)
-	       let e = extract_term env mle t' c [] in
-	       (* Expunging term and type from dummy lambdas. *) 
-	       Dterm (r, term_expunge s (ids,e), type_expunge t)
+	       let e,t = extract_std_constant env kn (force body) typ in 
+	       Dterm (r,e,t)
 	   | (Info, TypeScheme) -> 
-	       let body = Declarations.force l_body in
 	       let s,vl = type_sign_vl env typ in 
                let db = db_from_sign s in 
-               let t = extract_type_scheme env db body (List.length s) in 
-               Dtype (r, vl, t))
-
-let extract_constant_cache kn r = 
-  try lookup_term kn 
-  with Not_found ->
-    let d = extract_constant kn r
-    in add_term kn d; d
-
-let extract_inductive_declaration kn = 
-  let ind = extract_inductive kn in 
-  let f l = List.filter (type_neq Tdummy) l in 
+               let t = extract_type_scheme env db (force body) (List.length s) 
+	       in Dtype (r, vl, t))
+
+let extract_constant_spec env kn cb = 
+  let kn = long_kn kn in 
+  let r = ConstRef kn in 
+  let typ = cb.const_type in
+  match flag_of_type env typ with 
+    | (Logic, TypeScheme) -> Stype (r, [], Some Tdummy)
+    | (Logic, Default) -> Sval (r, Tdummy) 
+    | (Info, TypeScheme) -> 
+	let s,vl = type_sign_vl env typ in 
+	(match cb.const_body with 
+	  | None -> Stype (r, vl, None)
+	  | Some body -> 
+	      let db = db_from_sign s in 
+	      let t = extract_type_scheme env db (force body) (List.length s)
+	      in Stype (r, vl, Some t)) 
+    | (Info, Default) -> 
+	let t = snd (record_constant_type env kn (Some typ)) in 
+	Sval (r, type_expunge env t)
+
+let extract_inductive env kn = 
+  let ind = extract_ind env kn in 
+  add_recursors env kn; 
+  let f l = List.filter (type_neq env Tdummy) l in 
   let packets = 
     Array.map (fun p -> { p with ip_types = Array.map f p.ip_types }) 
       ind.ind_packets
-  in Dind (kn,{ ind with ind_packets = packets })
+  in { ind with ind_packets = packets }
 
 (*s From a global reference to a ML declaration. *)
 
-let extract_declaration r = match r with
-  | ConstRef kn -> extract_constant_cache kn r
-  | IndRef (kn,_) -> extract_inductive_declaration kn
-  | ConstructRef ((kn,_),_) -> extract_inductive_declaration kn
-  | VarRef kn -> error_section ()
+let extract_declaration env r = match r with
+  | ConstRef kn -> extract_constant env kn (Environ.lookup_constant kn env)
+  | IndRef (kn,_) -> let kn = long_kn kn in Dind (kn, extract_inductive env kn)
+  | ConstructRef ((kn,_),_) -> 
+      let kn = long_kn kn in 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 cb.const_type with 
+    | (Logic,_) -> Logical
+    | (Info,TypeScheme) -> Type
+    | (Info,Default) -> Term
+
+
+  
+
+
 
 
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 268a68692..c9654d25c 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -10,10 +10,28 @@
 
 (*s Extraction from Coq terms to Miniml. *)
 
+open Names
+open Term
+open Declarations
+open Environ
 open Libnames
 open Miniml
 
+val extract_constant : env -> kernel_name -> constant_body -> ml_decl
+
+val extract_constant_spec : env -> kernel_name -> constant_body -> ml_spec
+
+val extract_fixpoint : 
+  env -> kernel_name array -> (constr, types) prec_declaration -> ml_decl 
+
+val extract_inductive : env -> kernel_name -> ml_ind
+
 (*s ML declaration corresponding to a Coq reference. *)
 
-val extract_declaration : global_reference -> ml_decl
+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
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 81ec48767..aac7f8778 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -15,6 +15,7 @@ open Util
 open Names
 open Nameops
 open Libnames
+open Table
 open Miniml
 open Mlutil
 open Ocaml
@@ -30,18 +31,22 @@ let keywords =
   Idset.empty
 
 let preamble prm used_modules (mldummy,tdummy,tunknown) =
-  let m = String.capitalize (string_of_id prm.mod_name)   in 
-  str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ 
+  let pp_mp = function 
+    | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
+    | _ -> assert false 
+  in  
+  str "module " ++ pr_upper_id prm.mod_name ++ str " where" ++ fnl () 
+  ++ fnl() ++ 
   str "import qualified Prelude" ++ fnl() ++
-  Idset.fold
-    (fun m s -> str "import qualified " ++ pr_id (uppercase_id m) ++ fnl() ++ s)
-    used_modules (mt ()) ++ fnl()
-  ++
+  prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules
+  ++ fnl () ++
   (if mldummy then 
      str "__ = Prelude.error \"Logical or arity value used\"" 
      ++ fnl () ++ fnl()
    else mt())
 
+let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO" 
+
 let pp_abst = function
   | [] -> (mt ())
   | l  -> (str "\\" ++
@@ -54,7 +59,9 @@ let pr_lower_id id = pr_id (lowercase_id id)
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_global r = P.pp_global r
+let local_mp = ref initial_path 
+
+let pp_global r = P.pp_global !local_mp r
 let empty_env () = [], P.globals()
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
@@ -111,7 +118,7 @@ let rec pp_expr par env args =
 	hv 0 
 	  (pp_par par 
 	     (hv 0 
-		(hov 2 (str "let" ++ pp_id ++ str " = " ++ pp_a1) ++ 
+		(hov 5 (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++ 
 		 spc () ++ str "in") ++
 	      spc () ++ hov 0 pp_a2))
     | MLglob r -> 
@@ -139,7 +146,6 @@ let rec pp_expr par env args =
 	str "__" (* An [MLdummy] may be applied, but I don't really care. *)
     | MLcast (a,t) -> pp_expr par env args a
     | MLmagic a ->  pp_expr par env args a
-    | MLcustom s -> str s
 
 and pp_pat env pv = 
   let pp_one_pat (name,ids,t) =
@@ -180,20 +186,20 @@ and pp_function env f t =
 let pp_comment s = str "-- " ++ s ++ fnl ()
 
 let pp_logical_ind ip packet = 
-  pp_comment (Printer.pr_global (IndRef ip) ++ str " : logical inductive") ++
+  pp_comment (pr_global (IndRef ip) ++ str " : logical inductive") ++
   pp_comment (str "with constructors : " ++ 
-	      prvect_with_sep spc Printer.pr_global 
+	      prvect_with_sep spc pr_global 
 		(Array.mapi (fun i _ -> ConstructRef (ip,i+1)) packet.ip_types)) 
 
 let pp_singleton kn packet = 
   let l = rename_tvars keywords packet.ip_vars in 
   let l' = List.rev l in 
-  hov 0 (str "type " ++ pp_global (IndRef (kn,0)) ++ spc () ++ 
+  hov 2 (str "type " ++ pp_global (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 () ++
 	 pp_comment (str "singleton inductive, whose constructor was " ++ 
-		     Printer.pr_global (ConstructRef ((kn,0),1))))
+		     pr_global (ConstructRef ((kn,0),1))))
 
 let pp_one_ind ip pl cv =
   let pl = rename_tvars keywords pl in
@@ -215,40 +221,60 @@ let pp_one_ind ip pl cv =
 	  prvect_with_sep (fun () -> fnl () ++ str "  | ") pp_constructor 
 	    (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
   
-let rec pp_ind kn i ind =
-  if i >= Array.length ind.ind_packets then mt ()
+let rec pp_ind first kn i ind =
+  if i >= Array.length ind.ind_packets then 
+    if first then mt () else fnl () 
   else 
     let ip = (kn,i) in 
     let p = ind.ind_packets.(i) in 
-    if p.ip_logical then  
-      pp_logical_ind ip p ++ pp_ind kn (i+1) ind
+    if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind 
     else 
-      pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ pp_ind kn (i+1) ind
-
+      if p.ip_logical then  
+	pp_logical_ind ip p ++ pp_ind first kn (i+1) ind
+      else 
+	pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ 
+	pp_ind false kn (i+1) ind
+	  
 
 (*s Pretty-printing of a declaration. *)
 
-let pp_decl = function
-  | Dind (kn,i) when i.ind_info = Singleton -> pp_singleton kn i.ind_packets.(0)
-  | Dind (kn,i) -> hov 0 (pp_ind kn 0 i)
+let pp_decl mp = 
+  local_mp := mp;
+  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)
   | Dtype (r, l, t) ->
-      let l = rename_tvars keywords l in
-      let l' = List.rev l in 
-      hov 0 (str "type " ++ pp_global r ++ spc () ++ 
+      if is_inline_custom r then mt () 
+      else 
+	let l = rename_tvars keywords l in
+	let l' = List.rev l in 
+	hov 2 (str "type " ++ pp_global r ++ spc () ++ 
 	       prlist_with_sep (fun () -> (str " ")) pr_id l ++
 	       (if l <> [] then (str " ") else (mt ())) ++ str "=" ++ spc () ++
-	       pp_type false l' t ++ fnl ())
+	       pp_type false l' t ++ fnl () ++ fnl ())
   | Dfix (rv, defs,_) ->
       let ppv = Array.map pp_global rv in 
-      (prlist_with_sep (fun () -> fnl () ++ fnl ()) 
-	   (fun (pi,ti) -> pp_function (empty_env ()) pi ti)
-	   (List.combine (Array.to_list ppv) (Array.to_list defs)) ++ fnl ())
+      prlist_with_sep (fun () -> fnl () ++ fnl ())
+	(fun (pi,ti) -> pp_function (empty_env ()) pi ti)
+	(List.combine (Array.to_list ppv) (Array.to_list defs)) 
+      ++ fnl () ++ fnl ()
   | Dterm (r, a, _) ->
-      hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl ())
-  | DcustomTerm (r,s) -> 
-      hov 0  (pp_global r ++ str " =" ++ spc () ++ str s ++ fnl ())
-  | DcustomType (r,s) -> 
-      hov 0  (str "type " ++ pp_global r ++ str " = " ++ str s ++ fnl ())
+      if is_inline_custom r then mt () 
+      else 
+	hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl () ++ fnl ())
+
+let pp_structure_elem mp = function 
+  | (l,SEdecl d) -> pp_decl mp 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
 
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index be60cf1c1..062b236ca 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -14,6 +14,7 @@ open Miniml
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
+val preamble : 
+  extraction_params -> module_path list -> 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 6f56f36e3..235847f32 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -56,6 +56,8 @@ type inductive_info = Record | Singleton | Coinductive | Standard
 *)
 
 type ml_ind_packet = { 
+  ip_typename : identifier; 
+  ip_consnames : identifier array; 
   ip_logical : bool;
   ip_sign : signature; 
   ip_vars : identifier list; 
@@ -83,23 +85,23 @@ type ml_ast =
   | MLdummy
   | MLcast   of ml_ast * ml_type
   | MLmagic  of ml_ast
-  | MLcustom of string
 
 (*s ML declarations. *)
 
 type ml_decl = 
   | Dind  of kernel_name * ml_ind
   | Dtype of global_reference * identifier list * ml_type
-  | Dterm   of global_reference * ml_ast * ml_type
-  | DcustomTerm of global_reference * string
-  | DcustomType of global_reference * string
-  | Dfix    of global_reference array * ml_ast array * ml_type array
+  | Dterm of global_reference * ml_ast * ml_type
+  | Dfix  of global_reference array * ml_ast array * ml_type array
+
+type ml_spec = 
+  | Sind  of kernel_name * ml_ind
+  | Stype of global_reference * identifier list * ml_type option 
+  | Sval  of global_reference * ml_type
 
 type ml_specif = 
-  | Sval of ml_type
-  | Stype of ml_type option 
-  | Smind of ml_ind
-  | Smodule of ml_module_type  (* et un module_path option ?? *) 
+  | Spec of ml_spec 
+  | Smodule of ml_module_type
   | Smodtype of ml_module_type
 
 and ml_module_sig = (label * ml_specif) list
@@ -116,10 +118,7 @@ and ml_module_expr =
   | MEapply of ml_module_expr * ml_module_expr
 
 and ml_structure_elem = 
-  | SEind of ml_ind
-  | SEtype of identifier list * ml_type
-  | SEterm of ml_ast * ml_type
-  | SEfix of global_reference array * ml_ast array * ml_type array
+  | SEdecl of ml_decl
   | SEmodule of ml_module (* pourquoi pas plutot ml_module_expr *)
   | SEmodtype of ml_module_type
 
@@ -127,25 +126,32 @@ and ml_module_structure = (label * ml_structure_elem) list
 
 and ml_module = 
     { ml_mod_expr : ml_module_expr option; 
-      ml_mod_type : ml_module_type }
+      ml_mod_type : ml_module_type;
+      ml_mod_equiv : module_path option } 
+
+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. *)
 
-type extraction_params =  
-  { modular : bool; 
-    mod_name : identifier; 
-    to_appear : global_reference list }
-
 module type Mlpp_param = sig
   val globals : unit -> Idset.t
-  val pp_global : global_reference -> std_ppcmds
+  val pp_global : module_path -> global_reference -> std_ppcmds
+  val pp_long_module : module_path -> std_ppcmds
+  val pp_short_module : identifier -> std_ppcmds
 end
 
 module type Mlpp = sig
-  val pp_decl : ml_decl -> std_ppcmds
+  val pp_decl : module_path -> 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 }
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 145d700cc..3355fc2aa 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -212,7 +212,7 @@ let kn_of_r r = match r with
     | ConstRef kn -> kn
     | IndRef (kn,_) -> kn
     | ConstructRef ((kn,_),_) -> kn
-    | VarRef _ -> error_section ()
+    | VarRef _ -> assert false
 
 let rec type_mem_kn kn = function 
   | Tmeta _ -> assert false
@@ -340,7 +340,7 @@ let ast_iter_rel f =
     | MLcons (_,l) ->  List.iter (iter n) l
     | MLcast (a,_) -> iter n a
     | MLmagic a -> iter n a
-    | MLglob _ | MLexn _ | MLdummy | MLcustom _ -> ()
+    | MLglob _ | MLexn _ | MLdummy -> ()
   in iter 0 
 
 (*s Map over asts. *)
@@ -356,7 +356,7 @@ let ast_map f = function
   | MLcons (c,l) -> MLcons (c, List.map f l)
   | MLcast (a,t) -> MLcast (f a, t)
   | MLmagic a -> MLmagic (f a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLcustom _ as a -> a
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
@@ -372,7 +372,7 @@ let ast_map_lift f n = function
   | MLcons (c,l) -> MLcons (c, List.map (f n) l)
   | MLcast (a,t) -> MLcast (f n a, t)
   | MLmagic a -> MLmagic (f n a)
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLcustom _ as a -> a	
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a	
 
 (*s Iter over asts. *) 
 
@@ -387,37 +387,7 @@ let ast_iter f = function
   | MLcons (c,l) -> List.iter f l
   | MLcast (a,t) -> f a
   | MLmagic a -> f a
-  | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLcustom _ as a -> ()
-
-(*S Searching occurrences of a particular term (no lifting done). *)
-
-let rec ast_search t a = 
-  if t = a then raise Found else ast_iter (ast_search t) a
-
-let decl_search t l = 
-  let one_decl = function 
-    | Dterm (_,a,_) -> ast_search t a
-    | Dfix (_,c,_) -> Array.iter (ast_search t) c
-    | _ -> () 
-  in 
-  try List.iter one_decl l; false with Found -> true
-
-let rec type_search t = function  
-  | Tarr (a,b) -> type_search t a; type_search t b 
-  | Tglob (r,l) -> List.iter (type_search t) l
-  | u -> if t = u then raise Found
-
-let decl_type_search t l = 
-  let one_decl = function 
-    | Dind (_,{ind_packets=p})  -> 
-	Array.iter 
-	  (fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p
-    | Dterm (_,_,u) -> type_search t u
-    | Dfix (_,_,v) -> Array.iter (type_search t) v
-    | Dtype (_,_,u) -> type_search t u
-    | _ -> () 
-  in 
-  try List.iter one_decl l; false with Found -> true
+  | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> ()
 
 (*S Operations concerning De Bruijn indices. *)
 
@@ -1032,7 +1002,7 @@ let rec non_stricts add cand = function
   | MLcase (t,v) -> 
       (* The only interesting case: for a variable to be non-strict, *)
       (* it is sufficient that it appears non-strict in at least one branch, *)
-      (* so he make an union (in fact a merge). *)
+      (* so we make an union (in fact a merge). *)
       let cand = non_stricts false cand t in 
       Array.fold_left 
 	(fun c (_,i,t)-> 
@@ -1062,10 +1032,10 @@ let is_not_strict t =
    If we could inline [t] (the user said nothing special), 
    should we inline ? 
    
-   We don't expand fixpoints, but always inductive constructors
-   and small terms.
-   Last case of inlining is a term with at least one non-strict 
-   variable (i.e. a variable that may not be evaluated). *)
+   We expand small terms with at least one non-strict 
+   variable (i.e. a variable that may not be evaluated).
+   
+   Futhermore we don't expand fixpoints. *)
 
 let inline_test t = 
   not (is_fix t) && (ml_size t < 12 && is_not_strict t)
@@ -1087,109 +1057,99 @@ let manual_inline = function
    we are free to act (AutoInline is set)
    \end{itemize} *)
 
-(*i  DEBUG 
-  let inline_test' r t = 
-  let b = inline_test t in 
-  if b then msgnl (Printer.pr_global r); 
-  b i*)
-
 let inline r t = 
   not (to_keep r) (* The user DOES want to keep it *)
+  && not (is_inline_custom r) 
   && (to_inline r (* The user DOES want to inline it *) 
      || (auto_inline () && lang () <> Haskell 
 	 && (is_recursor r || manual_inline r || inline_test t)))
 
 (*S Optimization. *)
 
-let subst_glob_ast r m = 
-  let rec substrec = function
-    | MLglob r' as t -> if r = r' then m else t
-    | t -> ast_map substrec t
-  in substrec
-
-let subst_glob_decl r m = function
-  | Dterm(r',t',typ) -> Dterm(r', subst_glob_ast r m t', typ)
-  | d -> d
-
-let inline_glob r t l = 
-  if not (inline r t) then true, l 
-  else false, List.map (subst_glob_decl r t) l
-
-let print_ml_decl prm (r,_) = 
-  not (to_inline r) || List.mem r prm.to_appear
-
-let add_ml_decls prm decls = 
-  let l1 = ml_type_extractions () in 
-  let l1 = List.filter (print_ml_decl prm) l1 in 
-  let l1 = List.map (fun (r,s)-> DcustomType (r,s)) l1 in 
-  let l2 = ml_term_extractions () in 
-  let l2 = List.filter (print_ml_decl prm) l2 in 
-  let l2 = List.map (fun (r,s)-> DcustomTerm (r,s)) l2 in
-  l1 @ l2 @ decls
-
-let rec expunge_fix_decls prm v c map b = function 
-  | [] -> b, [], map  
-  | Dterm (r, t, typ) :: l when array_exists ((=) r) v -> 
-      let t = normalize t in 
-      let t' = optimize_fix t in 
-      (match t' with 
-	 | MLfix(_,_,c') when c=c' -> 
-	     let b',l = inline_glob r t l in 
-	     let b = b || b' || List.mem r prm.to_appear in 
-	     let map = Refmap.add r typ map in 
-	     expunge_fix_decls prm v c map b l 
-	 | _ -> raise Impossible)
-  | d::l -> let b,l,map = expunge_fix_decls prm v c map b l in b, d::l, map  
-
-let rec optimize prm = function
-  | [] -> 
-      []
+let rec subst_glob_ast s t = match t with 
+  | MLglob (ConstRef kn) -> (try KNmap.find (long_kn kn) !s with Not_found -> t)
+  | _ -> ast_map (subst_glob_ast s) t
+
+let rec optim prm s = function
+  | [] -> []
   | (Dtype (r,_,Tdummy) | Dterm(r,MLdummy,_)) as d :: l ->
-      if List.mem r prm.to_appear then d :: (optimize prm l) 
-      else optimize prm l
+      if List.mem r prm.to_appear then d :: (optim prm s l) else optim prm s l
   | Dterm (r,t,typ) :: l ->
-      let t = normalize t in
-      let b,l = inline_glob r t l in 
-      let b = b || prm.modular || List.mem r prm.to_appear in 
-      let t' = optimize_fix t in
-      (try optimize_Dfix prm (r,t',typ) b l 
-       with Impossible ->
-	 if b then Dterm (r,t',typ) :: (optimize prm l)
-	 else optimize prm l)
-  | d :: l -> d :: (optimize prm l)
-
-and optimize_Dfix prm (r,t,typ) b l = 
-  match t with 
-    | MLfix (_, f, c) -> 
-	let len = Array.length f in 
-	if len = 1 then 
-	  if b then 
-	    let c = [|ast_subst (MLglob r) c.(0)|] in 
-	    Dfix ([|r|], c, [|typ|]) :: (optimize prm l)
-	  else optimize prm l
-	else 
-	  let v = try 
-	    let d = dirpath (sp_of_global None r) in 
-	    Array.map (fun id -> locate (make_qualid d id)) f 
-	  with Not_found -> raise Impossible 
-	  in 
-	  let map = Refmap.add r typ (Refmap.empty) in 
-	  let b,l,map = expunge_fix_decls prm v c map b l in 
-	  if b then 
-	    let typs = 
-	      Array.map 
-		(fun r -> try Refmap.find r map
-		 with Not_found -> Tunknown) v 
-	    in 
-	    let c = 
-	      let gv = Array.init len (fun i -> MLglob v.(len-i-1)) in 
-	      Array.map (gen_subst gv (-len)) c in 
-	    Dfix (v, c, typs) :: (optimize prm l)
-	  else optimize prm l 
-    | _ -> raise Impossible
+      let t = normalize (subst_glob_ast s t) in 
+      let i = inline r t in 
+      if i then s := KNmap.add (long_kn (kn_of_r r)) t !s; 
+      if not i || prm.modular || List.mem r prm.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)
+
+let rec optim_se top prm s = function 
+  | [] -> [] 
+  | (l,SEdecl (Dterm (r,a,t))) :: lse -> 
+      let r = long_r r in 
+      let kn = kn_of_r r in 
+      let a = normalize (subst_glob_ast s a) in 
+      let i = inline r a in 
+      if i then s := KNmap.add kn a !s; 
+      if top && i && not prm.modular && not (List.mem r prm.to_appear)
+      then optim_se top prm 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)
+  | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> 
+      let av = Array.map (fun a -> normalize (subst_glob_ast s a)) av in 
+      (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top prm s lse)
+  | (l,SEmodule m) :: lse -> 
+      let m = { m with ml_mod_expr = option_app (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) 
+
+and optim_me prm s = function 
+  | MEstruct (msid, lse) -> MEstruct (msid, optim_se false prm 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)
+
+let optimize_struct prm before struc = 
+  let subst = ref (KNmap.empty : ml_ast KNmap.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
+
+(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a 
+   [ml_structure]. *) 
+
+let struct_iter do_decl do_spec s = 
+  let rec se_iter = function 
+    | (_,SEdecl d) -> do_decl d
+    | (_,SEmodule m) -> 
+	option_iter me_iter m.ml_mod_expr; mt_iter m.ml_mod_type
+    | (_,SEmodtype m) -> mt_iter m
+  and me_iter = function 
+    | MEident _ -> () 
+    | MEfunctor (_,mt,me) -> me_iter me; mt_iter mt
+    | MEapply (me,me') -> me_iter me; me_iter me'
+    | MEstruct (msid, sel) -> List.iter se_iter sel
+  and mt_iter = function 
+    | MTident _ -> () 
+    | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
+    | MTsig (_, sign) -> List.iter spec_iter sign
+  and spec_iter = function 
+    | (_,Spec s) -> do_spec s
+    | (_,Smodule mt) -> mt_iter mt
+    | (_,Smodtype mt) -> mt_iter mt
+  in 
+  List.iter (function (_,sel) -> List.iter se_iter sel) s
 
-(* Apply some fonctions upon all references in 
-   [ml_type], [ml_ast], [ml_decl]. *)
+(*s Apply some fonctions upon all references in [ml_type], [ml_ast], 
+  [ml_decl], [ml_spec] and [ml_structure]. *)
 
 type do_ref = global_reference -> unit
 
@@ -1210,25 +1170,93 @@ let ast_iter_references do_term do_cons do_type a =
       | MLcast (_,t) -> type_iter_references do_type t 
       | _ -> ()
   in iter a
+
+let ind_iter_references do_term do_cons do_type kn ind = 
+  let type_iter = type_iter_references do_type in
+  let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in 
+  let packet_iter ip p = 
+    do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types 
+  in
+  if ind.ind_info = Record then List.iter do_term (find_projections kn); 
+  Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
   
 let decl_iter_references do_term do_cons do_type = 
   let type_iter = type_iter_references do_type 
-  and ast_iter = ast_iter_references do_term do_cons do_type in 
-  let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in 
-  let packet_iter ip p = 
-    do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in
-  let ind_iter kn ind =
-    if ind.ind_info = Record then List.iter do_term (find_projections kn); 
-    Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
-  in 
+  and ast_iter = ast_iter_references do_term do_cons do_type in
   function 
-    | Dind (kn,ind) -> ind_iter kn ind 
+    | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind 
     | Dtype (r,_,t) -> do_type r; type_iter t 
     | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t
     | Dfix(rv,c,t) -> 	
 	Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t
-    | DcustomTerm (r,_) -> do_term r
-    | DcustomType (r,_) -> do_type r
 
+let spec_iter_references do_term do_cons do_type = function 
+  | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
+  | Stype (r,_,ot) -> do_type r; option_iter (type_iter_references do_type) ot
+  | Sval (r,t) -> do_term r; type_iter_references do_type t
+
+let struct_iter_references do_term do_cons do_type = 
+  struct_iter 
+    (decl_iter_references do_term do_cons do_type) 
+    (spec_iter_references do_term do_cons do_type) 
+
+(*S Searching occurrences of a particular term (no lifting done). *)
+
+let rec ast_search t a = 
+  if t = a then raise Found else ast_iter (ast_search t) a
+
+let decl_ast_search t = function 
+  | Dterm (_,a,_) -> ast_search t a
+  | Dfix (_,c,_) -> Array.iter (ast_search t) c
+  | _ -> () 
+
+let struct_ast_search t s = 
+  try struct_iter (decl_ast_search t) (fun _ -> ()) s; false
+  with Found -> true
+
+let rec type_search t = function  
+  | Tarr (a,b) -> type_search t a; type_search t b 
+  | Tglob (r,l) -> List.iter (type_search t) l
+  | u -> if t = u then raise Found
+
+let decl_type_search t = function 
+  | Dind (_,{ind_packets=p})  -> 
+      Array.iter 
+	(fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p
+  | Dterm (_,_,u) -> type_search t u
+  | Dfix (_,_,v) -> Array.iter (type_search t) v
+  | Dtype (_,_,u) -> type_search t u
+
+let spec_type_search t = function 
+  | Sind (_,{ind_packets=p}) -> 
+      Array.iter 
+	(fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p
+  | Stype (_,_,ot) -> option_iter (type_search t) ot
+  | Sval (_,u) -> type_search t u
+
+let struct_type_search t s = 
+  try struct_iter (decl_type_search t) (spec_type_search t) s; false
+  with Found -> true
+
+
+(*s Generating the signature. *)
+
+let rec msig_of_ms = function 
+  | [] -> [] 
+  | (l,SEdecl (Dind (kn,i))) :: ms -> (l,Spec (Sind (kn,i))) :: (msig_of_ms ms)
+  | (l,SEdecl (Dterm (r,_,t))) :: ms -> (l,Spec (Sval (r,t))) :: (msig_of_ms ms)
+  | (l,SEdecl (Dtype (r,v,t))) :: ms -> 
+      (l,Spec (Stype (r,v,Some t))) :: (msig_of_ms ms) 
+  | (l,SEdecl (Dfix (rv,_,tv))) :: ms -> 
+      let msig = ref (msig_of_ms ms) in 
+      for i = Array.length rv - 1 downto 0 do 
+	msig := (l,Spec (Sval (rv.(i),tv.(i))))::!msig
+      done; 
+      !msig
+  | (l,SEmodule m) :: ms -> (l,Smodule m.ml_mod_type) :: (msig_of_ms ms)
+  | (l,SEmodtype m) :: ms -> (l,Smodtype m) :: (msig_of_ms ms)
+
+let signature_of_structure s = 
+  List.map (fun (mp,ms) -> mp,msig_of_ms ms) s 
 
 
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index c061a5369..b8f817eab 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -69,6 +69,10 @@ val type_neq : abbrev_map -> ml_type -> ml_type -> bool
 val type_to_sign : abbrev_map -> ml_type -> bool list
 val type_expunge : abbrev_map -> ml_type -> ml_type
 
+val case_expunge : bool list -> ml_ast -> identifier list * ml_ast
+val term_expunge : bool list -> identifier list * ml_ast -> ml_ast
+
+
 (*s Special identifiers. [dummy_name] is to be used for dead code
     and will be printed as [_] in concrete (Caml) code. *)
 
@@ -95,34 +99,24 @@ val ast_occurs : int -> ml_ast -> bool
 val ast_lift : int -> ml_ast -> ml_ast
 val ast_pop : ml_ast -> ml_ast
 
-(*s Some transformations of ML terms. [optimize] simplify
+(*s Some transformations of ML terms. [optimize_struct] simplify
     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. *)
 
-val optimize : 
-  extraction_params -> ml_decl list -> ml_decl list
+val optimize_struct : 
+  extraction_params -> ml_decl list option -> ml_structure -> ml_structure
 
 (* Misc. *)
 
-val decl_search : ml_ast -> ml_decl list -> bool
-val decl_type_search : ml_type -> ml_decl list -> bool
-
-val add_ml_decls : 
-  extraction_params -> ml_decl list -> ml_decl list
-
-val case_expunge : 
-  bool list -> ml_ast -> identifier list * ml_ast
-
-val term_expunge : 
-  bool list -> identifier list * ml_ast -> ml_ast
+val struct_ast_search : ml_ast -> ml_structure -> bool
+val struct_type_search : ml_type -> ml_structure -> bool
 
 type do_ref = global_reference -> unit 
 
-val type_iter_references : do_ref -> ml_type -> unit
-val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit
 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
 
-
-
+val signature_of_structure : ml_structure -> ml_signature
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 56108a225..f7a07f581 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -73,6 +73,9 @@ let rec rename_id id avoid =
 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
@@ -119,27 +122,46 @@ let keywords =
   Idset.empty
 
 let preamble _ used_modules (mldummy,tdummy,tunknown) = 
-  Idset.fold (fun m s -> str "open " ++ pr_id (uppercase_id m) ++ fnl() ++ s)
-    used_modules (mt ())
+  let pp_mp = function 
+    | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
+    | _ -> assert false 
+  in 
+  prlist (fun mp -> str "open " ++ pp_mp mp ++ fnl ()) used_modules
   ++ 
-  (if Idset.is_empty used_modules then mt () else fnl ())
+  (if used_modules = [] then mt () else fnl ())
   ++
   (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() else mt()) 
   ++
   (if mldummy then 
-     str "let __ = let rec f _ = Obj.repr f in Obj.repr f" 
-     ++ fnl ()
+     str "let __ = let rec f _ = Obj.repr f in Obj.repr f" ++ fnl ()
    else mt ()) 
   ++ 
   (if tdummy || tunknown || mldummy then fnl () else mt ())
 
+let preamble_sig _ used_modules (_,tdummy,tunknown) = 
+  let pp_mp = function 
+    | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
+    | _ -> assert false 
+  in 
+  prlist (fun mp -> str "open " ++ pp_mp mp ++ fnl ()) used_modules
+  ++ 
+  (if used_modules = [] then mt () else fnl ())
+  ++
+  (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() ++ fnl () 
+   else mt()) 
 
 (*s The pretty-printing functor. *)
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_global r = P.pp_global r
-let empty_env () = [], P.globals()
+let local_mp = ref initial_path
+
+let pp_global r = 
+  let r = long_r r in 
+  if is_inline_custom r then str (find_custom r) 
+  else P.pp_global !local_mp  r
+
+let empty_env () = [], P.globals ()
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
@@ -205,7 +227,7 @@ let rec pp_expr par env args =
 	apply (pp_global r)
     | MLcons (r,[]) ->
 	assert (args=[]);
-	if Refset.mem r !cons_cofix then 
+	if Refset.mem (long_r r) !cons_cofix then 
 	  pp_par par (str "lazy " ++ pp_global r)
 	else pp_global r
     | MLcons (r,args') -> 
@@ -215,12 +237,12 @@ let rec pp_expr par env args =
 	 with Not_found ->
 	   assert (args=[]);
 	   let tuple = pp_tuple (pp_expr true env []) args' in 
-	   if Refset.mem r !cons_cofix then 
+	   if Refset.mem (long_r r) !cons_cofix then 
 	     pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")")
 	   else pp_par par (pp_global r ++ spc () ++ tuple))
     | MLcase (t, pv) ->
 	let r,_,_ = pv.(0) in 
-	let expr = if Refset.mem r !cons_cofix then 
+	let expr = if Refset.mem (long_r r) !cons_cofix then 
 	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
 	else 
 	  (pp_expr false env [] t) 
@@ -256,7 +278,6 @@ let rec pp_expr par env args =
 		  spc () ++ pp_type true [] t))
     | MLmagic a ->
 	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
-    | MLcustom s -> str s
 	  
 and pp_record_pat (projs, args) =
    str "{ " ++
@@ -289,7 +310,8 @@ and pp_function env f t =
     let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in
     not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl)
   in
-  let is_not_cofix pv = let (r,_,_) = pv.(0) in not (Refset.mem r !cons_cofix) 
+  let is_not_cofix pv = 
+    let (r,_,_) = pv.(0) in not (Refset.mem (long_r r) !cons_cofix) 
   in					  
   match t' with 
     | MLcase(MLrel 1,pv) when is_not_cofix pv ->
@@ -326,14 +348,20 @@ let pp_val e typ =
 
 (*s Pretty-printing of [Dfix] *)
 
-let pp_Dfix env (p,c,t) = 
-  let init = 
-    pp_val p.(0) t.(0) ++ str "let rec " ++ pp_function env p.(0) c.(0) ++ fnl ()
-  in
-  iterate_for 1 (Array.length p - 1) 
-    (fun i acc -> acc ++ fnl () ++ 
-       pp_val p.(i) t.(i) ++ str "and " ++ pp_function env p.(i) c.(i) ++ fnl ())
-    init 
+let rec pp_Dfix init i ((rv,c,t) as fix) = 
+  if i >= Array.length rv then mt () 
+  else 
+    let r = long_r rv.(i) in 
+    if is_inline_custom r then pp_Dfix init (i+1) fix
+    else 
+      let e = pp_global r in
+      (if init then mt () else fnl ()) ++
+      pp_val e t.(i) ++
+      str (if init then "let rec " else "and ") ++
+      (if is_custom r then e ++ str " = " ++ str (find_custom r)
+       else pp_function (empty_env ()) e c.(i)) ++
+      fnl () ++ 
+      pp_Dfix false (i+1) fix 
 	
 (*s Pretty-printing of inductive types declaration. *)
 
@@ -358,20 +386,22 @@ let pp_one_ind prefix ip pl cv =
 let pp_comment s = str "(* " ++ s ++ str " *)" ++ fnl ()
 
 let pp_logical_ind ip packet = 
-  pp_comment (Printer.pr_global (IndRef ip) ++ str " : logical inductive") ++
+  pp_comment (pr_global (IndRef ip) ++ str " : logical inductive") ++
   pp_comment (str "with constructors : " ++ 
-	      prvect_with_sep spc Printer.pr_global 
+	      prvect_with_sep spc pr_global 
 		(Array.mapi (fun i _ -> ConstructRef (ip,i+1)) packet.ip_types)) 
     
 let pp_singleton kn packet = 
   let l = rename_tvars keywords packet.ip_vars in 
-  hov 0 (str "type " ++ pp_parameters l ++
-	 pp_global (IndRef (kn,0)) ++ str " =" ++ spc () ++
+  hov 2 (str "type " ++ pp_parameters l ++
+	 P.pp_global !local_mp (IndRef (kn,0)) ++ str " =" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
-	 pp_comment (str "singleton inductive, whose constructor was " ++ 
-		     Printer.pr_global (ConstructRef ((kn,0),1))))
+	 pp_comment 
+	   (str "singleton inductive, whose constructor was " ++ 
+	    pr_id packet.ip_consnames.(0)))
 
 let pp_record kn packet = 
+  let kn = long_kn kn in 
   let l = List.combine (find_projections kn) packet.ip_types.(0) in 
   let projs = find_projections kn in
   let pl = rename_tvars keywords packet.ip_vars in 
@@ -387,54 +417,148 @@ let pp_coind ip pl =
   pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t"
 
 let rec pp_ind co first kn i ind =
-  if i >= Array.length ind.ind_packets then mt () 
+  if i >= Array.length ind.ind_packets then 
+    if first then mt () else fnl ()
   else 
     let ip = (kn,i) in 
     let p = ind.ind_packets.(i) in 
-    if p.ip_logical then  
-      pp_logical_ind ip p ++ pp_ind co first kn (i+1) ind
+    if is_custom (IndRef (kn,i)) then pp_ind co first kn (i+1) ind
     else 
-      str (if first then "type " else "and ") ++
-      (if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ()) ++ 
-      pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++
-      fnl () ++ pp_ind co false kn (i+1) ind
+      if p.ip_logical then  
+	pp_logical_ind ip p ++ pp_ind co first kn (i+1) ind
+      else 
+	str (if first then "type " else "and ") ++
+	(if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ()) ++ 
+	pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++
+	fnl () ++ pp_ind co false kn (i+1) ind
 
 (*s Pretty-printing of a declaration. *)
 
-let pp_decl = function
-  | Dind (kn,i) as d -> 
-      (match i.ind_info with 
-	 | Singleton -> pp_singleton kn i.ind_packets.(0) 
-	 | Record -> pp_record kn i.ind_packets.(0)
-	 | Coinductive -> 
-	     let nop _ = () 
-	     and add r = cons_cofix := Refset.add r !cons_cofix in 
-	     decl_iter_references nop add nop d; 
-	     hov 0 (pp_ind true true kn 0 i)
-	 | Standard -> 
-	     hov 0 (pp_ind false true kn 0 i))
-  | Dtype (r, l, t) ->
-      let l = rename_tvars keywords l in 
-      hov 0 (str "type" ++ spc () ++ pp_parameters l ++ 
-	       pp_global r ++ spc () ++ str "=" ++ spc () ++ 
-	       pp_type false l t ++ fnl ())
-  | Dfix (rv, defs, typs) ->
-      (* We compute renamings of [rv] before asking [empty_env ()]... *)
-      let ppv = Array.map pp_global rv in 
-      hov 0 (pp_Dfix (empty_env ()) (ppv,defs,typs))
-  | Dterm (r, a, t) when is_projection r -> 
-      let e = pp_global r in 
-      (pp_val e t ++ 
-       hov 0 (str "let " ++ e ++ str " x = x." ++ e ++ fnl())) 
-  | Dterm (r, a, t) ->
-      let e = pp_global r in 
-      (pp_val e t ++ 
-       hov 0 (str "let " ++ pp_function (empty_env ()) e a ++ fnl ()))
-  | DcustomTerm (r,s) -> 
-      hov 0 (str "let " ++ pp_global r ++ 
-	     str " =" ++ spc () ++ str s ++ fnl ())
-  | DcustomType (r,s) -> 
-      hov 0 (str "type " ++ pp_global r ++ str " = " ++ str s ++ fnl ())
+let pp_mind kn i = 
+  let kn = long_kn kn in 
+  (match i.ind_info with 
+     | Singleton -> pp_singleton kn i.ind_packets.(0) ++ fnl ()
+     | Coinductive -> 
+	 let nop _ = () 
+	 and add r = cons_cofix := Refset.add (long_r r) !cons_cofix in 
+	 decl_iter_references nop add nop (Dind (kn,i)); 
+	 hov 0 (pp_ind true true kn 0 i) ++ fnl () 
+     | Record -> pp_record kn i.ind_packets.(0) ++ fnl () 
+     | _ -> hov 0 (pp_ind false true kn 0 i))
+  
+let pp_decl mp = 
+  local_mp := mp; 
+  function
+    | Dind (kn,i) as d -> pp_mind kn i
+    | Dtype (r, l, t) ->
+	if is_inline_custom r then mt () 
+	else 
+	  let l = rename_tvars keywords l in 
+	  let def = try str (find_custom r) with not_found -> pp_type false l t 
+	  in 
+	  hov 0 (str "type" ++ spc () ++ pp_parameters l ++ pp_global r ++ 
+		 spc () ++ str "=" ++ spc () ++ def ++ fnl () ++ fnl ())
+    | Dterm (r, a, t) -> 
+	if is_inline_custom r then mt () 
+	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) ++ fnl () 
+	     else if is_projection r then e ++ str " x = x." ++ e ++ fnl () 
+	     else pp_function (empty_env ()) e a ++ fnl ()) ++ fnl ()
+    | Dfix (rv,defs,typs) ->
+	hov 0 (pp_Dfix true 0 (rv,defs,typs)) ++ fnl ()
+
+let pp_spec mp = 
+  local_mp := mp; 
+  function 
+    | Sind (kn,i) -> pp_mind kn i
+    | Sval (r,t) -> 
+	if is_inline_custom r then mt () 
+	else 
+	  hov 0 (str "val" ++ spc () ++ pp_global r ++ str " :" ++ spc () ++
+		 pp_type false [] t ++ fnl () ++ fnl ())
+    | Stype (r,vl,ot) -> 
+	if is_inline_custom r then mt () 
+	else 
+	  let l = rename_tvars keywords vl in 
+	  let def = 
+	    try str "= " ++ str (find_custom r) 
+	    with not_found -> 
+	      match ot with 
+		| None -> mt () 
+		| Some t -> str "=" ++ spc () ++ pp_type false l t 
+	  in 
+	  hov 0 (str "type" ++ spc () ++ pp_parameters l ++ 
+		 pp_global r ++ spc () ++ def ++ fnl () ++ fnl ())
+
+let rec pp_structure_elem mp = function 
+  | (_,SEdecl d) -> pp_decl mp d
+  | (l,SEmodule m) ->
+      str "module " ++ P.pp_short_module (id_of_label l) ++ 
+      (match m.ml_mod_equiv with 
+	 | None -> 
+	     str ":" ++ fnl () ++ pp_module_type m.ml_mod_type ++ fnl () ++ 
+	     str " = " ++ fnl () ++ 
+	     (match m.ml_mod_expr with 
+		| None -> failwith "TODO: if this happens, see Jacek"
+		| Some me -> pp_module_expr me ++ fnl ())
+	 | Some mp -> str " = " ++ P.pp_long_module mp ++ fnl ()) ++ fnl ()
+  | (l,SEmodtype m) -> 
+      str "module type " ++ P.pp_short_module (id_of_label l) ++
+      str " = " ++ pp_module_type m ++ fnl () ++ fnl ()
+
+and pp_module_expr = function 
+  | MEident mp -> P.pp_long_module mp 
+  | MEfunctor (mbid, mt, me) -> 
+      str "functor (" ++ 
+      P.pp_short_module (id_of_mbid mbid) ++
+      str ":" ++
+      pp_module_type mt ++
+      str ") ->" ++
+      pp_module_expr me
+  | MEapply (me, me') -> 
+      str "(" ++ pp_module_expr me ++ str " (" ++ pp_module_expr me' ++ str ")"
+  | MEstruct (msid, sel) -> 
+      str "struct " ++ fnl () ++
+      prlist_with_sep fnl (pp_structure_elem (MPself msid)) sel ++ fnl () ++
+      str "end" 
+
+and pp_module_type = function 
+  | MTident kn -> 
+      let mp,_,l = repr_kn kn in P.pp_long_module (MPdot (mp,l)) 
+  | MTfunsig (mbid, mt, mt') -> 
+      str "functor (" ++ 
+      P.pp_short_module (id_of_mbid mbid) ++
+      str ":" ++
+      pp_module_type mt ++
+      str ") ->" ++ 
+      pp_module_type mt'
+  | MTsig (msid, sign) -> 
+      str "sig " ++ fnl () ++ 
+      prlist_with_sep fnl (pp_specif (MPself msid)) sign ++ fnl () ++
+      str "end"
+
+and pp_specif mp = function 
+  | (_,Spec s) -> pp_spec mp s 
+  | (l,Smodule mt) -> 
+      str "module " ++ 
+      P.pp_short_module (id_of_label l) ++
+      str " : " ++ pp_module_type mt ++ fnl () ++ fnl ()
+  | (l,Smodtype mt) -> 
+      str "module type " ++
+      P.pp_short_module (id_of_label l) ++
+      str " : " ++ pp_module_type mt ++ fnl () ++ fnl ()
+
+let pp_struct =
+  prlist (fun (mp,sel) -> prlist (pp_structure_elem mp) sel)
+
+let pp_signature = 
+  prlist (fun (mp,sign) -> prlist (pp_specif mp) sign)
 
 end
 
+
+
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index da2706f68..babe170c2 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -27,6 +27,8 @@ 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
@@ -36,7 +38,11 @@ val get_db_name : int -> env -> identifier
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
+val preamble : 
+  extraction_params -> module_path list -> 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 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 75533f788..b6d0014ac 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -17,6 +17,7 @@ open Nameops
 open Libnames
 open Miniml
 open Mlutil
+open Table
 open Ocaml
 
 (*s Scheme renaming issues. *)
@@ -46,7 +47,7 @@ let pp_abst st = function
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_global r = P.pp_global r
+let pp_global r = P.pp_global initial_path r
 let empty_env () = [], P.globals()
 
 (*s Pretty-printing of expressions.  *)
@@ -109,8 +110,6 @@ let rec pp_expr env args =
 	pp_expr env args a
     | MLmagic a ->
 	pp_expr env args a
-    | MLcustom s -> str s
-
 
 and pp_one_pat env (r,ids,t) = 
   let pp_arg id = str "?" ++ pr_id id in 
@@ -141,10 +140,9 @@ 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 () 
-  | DcustomType _ -> mt ()
   | Dfix (rv, defs,_) ->
       let ppv = Array.map pp_global rv in 
       prvect_with_sep fnl 
@@ -153,12 +151,25 @@ let pp_decl = function
 	     (paren (str "define " ++ pi ++ spc () ++ 
 		     (pp_expr (empty_env ()) [] ti)) 
 	      ++ fnl ()))
-	(array_map2 (fun p b -> (p,b)) ppv defs)
+	(array_map2 (fun p b -> (p,b)) ppv defs) ++
+      fnl ()
   | Dterm (r, a, _) ->
-      hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
-		    pp_expr (empty_env ()) [] a)) ++ fnl ()  
-  | DcustomTerm (r,s) -> 
-      hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ str s) ++ fnl ())
+      if is_inline_custom r then mt () 
+      else 
+	hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
+		      pp_expr (empty_env ()) [] a)) ++ fnl ()  ++ fnl ()
+
+let pp_structure_elem mp = function 
+  | (l,SEdecl d) -> pp_decl mp 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
 
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index 84940bbe7..4bd2a3d8b 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -16,7 +16,8 @@ open Names
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
+val preamble : 
+  extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 223bc77b3..1aa3daec2 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -11,6 +11,7 @@
 open Names
 open Term
 open Declarations
+open Nameops
 open Summary
 open Libobject
 open Goptions
@@ -19,46 +20,239 @@ open Util
 open Pp
 open Miniml
 
+(*S Extraction environment, shared with [extract_env.ml] *)
+
+let cur_env = ref Environ.empty_env
+
+let id_of_global = function 
+  | ConstRef kn -> let _,_,l = repr_kn kn in id_of_label l
+  | IndRef (kn,i) -> 
+      let mib = Environ.lookup_mind kn !cur_env in 
+      mib.mind_packets.(i).mind_typename
+  | ConstructRef ((kn,i),j) -> 
+      let mib = Environ.lookup_mind kn !cur_env in 
+      mib.mind_packets.(i).mind_consnames.(j-1)
+  | _ -> assert false
+
+let pr_global r = pr_id (id_of_global r)
+
 (*S Warning and Error messages. *)
 
+let err s = errorlabstrm "Extraction" s
+
 let error_axiom_scheme r = 
-  errorlabstrm "Extraction" 
-    (str "Extraction cannot accept the type scheme axiom " ++ spc () ++
-     Printer.pr_global r ++ spc () ++ str ".") 
+  err (str "Extraction cannot accept the type scheme axiom " ++ spc () ++
+       pr_global r ++ spc () ++ str ".") 
 
 let error_axiom r =
-  errorlabstrm "Extraction"
-    (str "You must specify an extraction for axiom" ++ spc () ++ 
-     Printer.pr_global r ++ spc () ++ str "first.")
+  err (str "You must specify an extraction for axiom" ++ spc () ++ 
+       pr_global r ++ spc () ++ str "first.")
 
 let warning_axiom r = 
   Options.if_verbose warn 
     (str "This extraction depends on logical axiom" ++ spc () ++ 
-     Printer.pr_global r ++ str "." ++ 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 error_section () = 
-  errorlabstrm "Extraction"
-    (str "You can't do that within a section. Close it and try again.")
+  err (str "You can't do that within a module or a section." ++ fnl () ++
+       str "Close it and try again.")
 
 let error_constant r = 
-  errorlabstrm "Extraction"
-    (Printer.pr_global r ++ spc () ++ str "is not a constant.") 
+  err (pr_global r ++ str " is not a constant.") 
+
+let error_fixpoint r = 
+  err (str "Fixpoint " ++ pr_global r ++ str " cannot be inlined.") 
 
 let error_type_scheme r = 
-  errorlabstrm "Extraction"
-    (Printer.pr_global r ++ spc () ++ str "is a type scheme, not a type.")
+  err (pr_global r ++ spc () ++ str "is a type scheme, not a type.")
 
 let error_inductive r = 
-  errorlabstrm "Extraction"
-    (Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
+  err (pr_global r ++ spc () ++ str "is not an inductive type.")
 
 let error_nb_cons () = 
-  errorlabstrm "Extraction" (str "Not the right number of constructors.")
+  err (str "Not the right number of constructors.")
+
+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.")
+
+let error_unknown_module m = 
+  err (str "Module" ++ spc () ++ pr_id 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.")
+
+let error_not_visible r = 
+  err (pr_global r ++ str " is not directly visible.\n" ++
+       str "For example, it may be inside an applied functor." ++
+       str "Use Recursive Extraction to get the whole environment.")
+
+let error_unqualified_name s1 s2 = 
+  err (str (s1 ^ " is used in " ^ s2 ^ " where it cannot be disambiguated\n" ^
+	    "in ML from another name sharing the same basename.\n"  ^
+	    "Please do some renaming.\n"))
+
+(*S Utilities concerning [module_path] *)
+
+let current_toplevel () = fst (Lib.current_prefix ())
+
+let is_toplevel mp = 
+  mp = initial_path || mp = current_toplevel ()
+
+let is_something_opened () = 
+  try ignore (Lib.what_is_opened ()); true
+  with Not_found -> false
+
+let rec base_mp = function 
+  | MPdot (mp,l) -> base_mp mp 
+  | mp -> mp 
+
+let rec prefixes_mp mp = match mp with 
+  | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
+  | _ -> MPset.singleton mp 
+
+let is_modfile = function 
+  | MPfile _ -> true 
+  | _ -> false
+
+let rec modfile_of_mp mp = match mp with 
+  | MPfile _ -> mp
+  | MPdot (mp,_) -> modfile_of_mp mp 
+  | _ -> raise Not_found
+
+let at_toplevel mp = 
+  is_modfile mp || is_toplevel mp
+
+let rec fst_level_module_of_mp mp = match mp with 
+  | MPdot (mp, l) when is_toplevel mp -> mp,l 
+  | MPdot (mp, l) -> fst_level_module_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_kn kn = 
+  let mp,_,l = repr_kn kn in parse_labels [l] mp
+
+(*S The main tables: constants, inductives, records, ... *)
+
+(*s Module path aliases. *) 
+
+(* A [MPbound] has no aliases except itself: it's its own long and short form.*)
+(* A [MPself] is a short form, and the table contains its long form. *)
+(* A [MPfile] is a long form, and the table contains its short form. *)
+(* Since the table does not contain all intermediate forms, a [MPdot] 
+   is dealt by first expending its head, and then looking in the table. *)
+
+let aliases = ref (MPmap.empty : module_path MPmap.t)
+let init_aliases () = aliases := MPmap.empty
+let add_aliases mp mp' = aliases := MPmap.add mp mp' (MPmap.add mp' mp !aliases)
+
+let rec long_mp mp = match mp with 
+  | MPbound _ | MPfile _ -> mp 
+  | MPself _ -> (try MPmap.find mp !aliases with Not_found -> mp)
+  | MPdot (mp1,l) -> 
+      let mp2 = long_mp mp1 in 
+      if mp1 == mp2 then mp else MPdot (mp2,l)
 
+(*i let short_mp mp = match mp with
+  | MPself _ | MPbound _ -> mp 
+  | MPfile _ -> (try MPmap.find mp !aliases with Not_found -> mp)
+  | MPdot _ -> (try MPmap.find (long_mp mp) !aliases with Not_found -> mp)
+i*)
 
-(*S Extraction AutoInline *)
+let long_kn kn = 
+  let (mp,s,l) = repr_kn kn in 
+  let mp' = long_mp mp in 
+  if mp' == mp then kn else make_kn mp' s l 
+
+(*i let short_kn kn = 
+  let (mp,s,l) = repr_kn kn in 
+  let mp' = short_mp mp in 
+  if mp' == mp then kn else make_kn mp' s l 
+i*)
+
+let long_r = function 
+  | ConstRef kn -> ConstRef (long_kn kn)
+  | IndRef (kn,i) -> IndRef (long_kn kn, i)
+  | ConstructRef ((kn,i),j) -> ConstructRef ((long_kn kn,i),j)
+  | _ -> assert false
+
+(*s Constants tables. *) 
+
+let terms = ref (KNmap.empty : ml_decl KNmap.t)
+let init_terms () = terms := KNmap.empty
+let add_term kn d = terms := KNmap.add (long_kn kn) d !terms
+let lookup_term kn = KNmap.find (long_kn kn) !terms
+
+let types = ref (KNmap.empty : ml_schema KNmap.t)
+let init_types () = types := KNmap.empty
+let add_type kn s = types := KNmap.add (long_kn kn) s !types
+let lookup_type kn = KNmap.find (long_kn kn) !types 
+
+(*s Inductives table. *)
+
+let inductives = ref (KNmap.empty : ml_ind KNmap.t)
+let init_inductives () = inductives := KNmap.empty
+let add_ind kn m = inductives := KNmap.add (long_kn kn) m !inductives
+let lookup_ind kn = KNmap.find (long_kn kn) !inductives
+
+(*s Recursors table. *)
+
+let recursors = ref KNset.empty
+let init_recursors () = recursors := KNset.empty
+
+let add_recursors env kn = 
+  let kn = long_kn kn in 
+  let make_kn id = make_kn (modpath kn) empty_dirpath (label_of_id id) in 
+  let mib = Environ.lookup_mind kn env in 
+  Array.iter 
+    (fun mip -> 
+       let id = mip.mind_typename in 
+       let kn_rec = make_kn (Nameops.add_suffix id "_rec")
+       and kn_rect = make_kn (Nameops.add_suffix id "_rect") in 
+       recursors := KNset.add kn_rec (KNset.add kn_rect !recursors))
+    mib.mind_packets
+
+let is_recursor = function 
+  | ConstRef kn -> KNset.mem (long_kn kn) !recursors
+  | _ -> false
+
+(*s Record tables. *)
+
+let records = ref (KNmap.empty : global_reference list KNmap.t)
+let init_records () = records := KNmap.empty
+
+let projs = ref Refset.empty
+let init_projs () = projs := Refset.empty
+
+let add_record kn l = 
+  records := KNmap.add (long_kn kn) l !records; 
+  projs := List.fold_right (fun r -> Refset.add (long_r r)) l !projs
+
+let find_projections kn = KNmap.find (long_kn kn) !records
+let is_projection r = Refset.mem (long_r r) !projs
+
+(*s Tables synchronization. *)
+
+let reset_tables () = 
+  init_terms (); init_types (); init_inductives (); init_recursors (); 
+  init_records (); init_projs (); init_aliases ()
+
+
+
+(*S The Extraction auxiliary commands *)
+
+(*s Extraction AutoInline *)
 
 let auto_inline_ref = ref true
 
@@ -72,7 +266,7 @@ let _ = declare_bool_option
 	   optwrite = (:=) auto_inline_ref}
 
 
-(*S Extraction Optimize *)
+(*s Extraction Optimize *)
 
 let optim_ref = ref true
 
@@ -86,7 +280,7 @@ let _ = declare_bool_option
 	   optwrite = (:=) optim_ref}
 
 
-(*S Extraction Lang *)
+(*s Extraction Lang *)
 
 type lang = Ocaml | Haskell | Scheme | Toplevel
 
@@ -110,15 +304,15 @@ let _ = declare_summary "Extraction Lang"
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
 
-(*S Extraction Inline/NoInline *)
+(*s Extraction Inline/NoInline *)
 
 let empty_inline_table = (Refset.empty,Refset.empty)
 
 let inline_table = ref empty_inline_table
 
-let to_inline r = Refset.mem r (fst !inline_table)
+let to_inline r = Refset.mem (long_r r) (fst !inline_table)
 
-let to_keep r = Refset.mem r (snd !inline_table)
+let to_keep r = Refset.mem (long_r r) (snd !inline_table)
 
 let add_inline_entries b l = 
   let f b = if b then Refset.add else Refset.remove in 
@@ -127,7 +321,14 @@ let add_inline_entries b l =
      (List.fold_right (f b) l i), 
      (List.fold_right (f (not b)) l k)
 
-(*s Registration of operations for rollback. *)
+let is_fixpoint kn = 
+  match (Global.lookup_constant kn).const_body with 
+    | None -> false
+    | Some body -> match kind_of_term (force body) with 
+	| Fix _ | CoFix _ -> true
+	| _ -> false
+
+(* Registration of operations for rollback. *)
 
 let (inline_extraction,_) = 
   declare_object 
@@ -142,15 +343,19 @@ let _ = declare_summary "Extraction Inline"
 	    init_function = (fun () -> inline_table := empty_inline_table);
 	    survive_section = true }
 
-(*s Grammar entries. *)
+(* Grammar entries. *)
 
 let extraction_inline b l =
-  if Lib.sections_are_opened () then error_section (); 
+  if is_something_opened () then error_section (); 
   let refs = List.map Nametab.global l in 
-  List.iter (function  ConstRef _ -> () | r -> error_constant r) refs; 
+  List.iter 
+    (fun r -> match r with 
+       | ConstRef kn when b && is_fixpoint kn -> error_fixpoint r
+       | ConstRef _ -> ()
+       | _ -> error_constant r) refs; 
   Lib.add_anonymous_leaf (inline_extraction (b,refs))
 
-(*s Printing part *)
+(* Printing part *)
 
 let print_extraction_inline () = 
   let (i,n)= !inline_table in 
@@ -159,13 +364,13 @@ let print_extraction_inline () =
     (str "Extraction Inline:" ++ fnl () ++ 
      Refset.fold
        (fun r p -> 
-	  (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++
+	  (p ++ str "   " ++ pr_global r ++ fnl ())) i' (mt ()) ++
      str "Extraction NoInline:" ++ fnl () ++ 
      Refset.fold
        (fun r p -> 
-	  (p ++ str "   " ++ Printer.pr_global r ++ fnl ())) n (mt ()))
+	  (p ++ str "   " ++ pr_global r ++ fnl ())) n (mt ()))
 
-(*s Reset part *)
+(* Reset part *)
 
 let (reset_inline,_) = 
   declare_object
@@ -177,7 +382,7 @@ let (reset_inline,_) =
 let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 
-(*S Extract Constant/Inductive. *)
+(*s Extract Constant/Inductive. *)
 
 type kind = Term | Type | Ind | Construct 
 
@@ -191,131 +396,63 @@ let check_term_or_type r = match r with
       else (r,Term)
   | _ -> error_constant r
 	
-let empty_extractions = (Refmap.empty, Refset.empty)
+let customs = ref Refmap.empty
 
-let extractions = ref empty_extractions
+let all_customs () = 
+  Refmap.fold (fun r _ -> Refset.add r) !customs Refset.empty
 
-let ml_extractions () = snd !extractions
+let term_customs () = 
+  Refmap.fold (fun r (k,s) l -> if k=Term then (r,s)::l else l) !customs []
 
-let ml_term_extractions () = 
-  Refmap.fold (fun r (k,s) l -> if k=Term then (r,s)::l else l)
-    (fst !extractions) []
-
-let ml_type_extractions () = 
-  Refmap.fold (fun r (k,s) l -> if k=Type then (r,s)::l else l) 
-    (fst !extractions) []
+let type_customs () = 
+  Refmap.fold (fun r (k,s) l -> if k=Type then (r,s)::l else l) !customs []
     
-let add_ml_extraction r k s = 
-  let (map,set) = !extractions in
-  extractions := (Refmap.add r (k,s) map, Refset.add r set)
+let add_custom r k s = customs := Refmap.add r (k,s) !customs
+
+let is_custom r = Refmap.mem (long_r r) !customs
 
-let is_ml_extraction r = Refset.mem r (snd !extractions)
+let is_inline_custom r = 
+  let r = long_r r in (is_custom r) && (to_inline r) 
 
-let find_ml_extraction r = snd (Refmap.find r (fst !extractions))
+let find_custom r = snd (Refmap.find (long_r r) !customs)
 
-(*s Registration of operations for rollback. *)
+(* Registration of operations for rollback. *)
 
-let (in_ml_extraction,_) = 
+let (in_customs,_) = 
   declare_object 
     {(default_object "ML extractions") with 
-       cache_function = (fun (_,(r,k,s)) -> add_ml_extraction r k s);
-       load_function = (fun _ (_,(r,k,s)) -> add_ml_extraction r k s);
+       cache_function = (fun (_,(r,k,s)) -> add_custom r k s);
+       load_function = (fun _ (_,(r,k,s)) -> add_custom r k s);
        export_function = (fun x -> Some x)}
 
 let _ = declare_summary "ML extractions"
-	  { freeze_function = (fun () -> !extractions);
-	    unfreeze_function = ((:=) extractions);
-	    init_function = (fun () -> extractions := empty_extractions);
+	  { freeze_function = (fun () -> !customs);
+	    unfreeze_function = ((:=) customs);
+	    init_function = (fun () -> customs := Refmap.empty);
 	    survive_section = true }
 
-(*s Grammar entries. *)
+(* Grammar entries. *)
 
 let extract_constant_inline inline r s =
-  if Lib.sections_are_opened () then error_section (); 
+  if is_something_opened () then error_section (); 
   let g,k = check_term_or_type (Nametab.global r) in
   Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
-  Lib.add_anonymous_leaf (in_ml_extraction (g,k,s))
+  Lib.add_anonymous_leaf (in_customs (g,k,s))
 
 let extract_inductive r (s,l) =
-  if Lib.sections_are_opened () then error_section (); 
+  if is_something_opened () then error_section (); 
   let g = Nametab.global r in match g with
   | IndRef ((kn,i) as ip) ->
       let mib = Global.lookup_mind kn in
       let n = Array.length mib.mind_packets.(i).mind_consnames in
       if n <> List.length l then error_nb_cons (); 
       Lib.add_anonymous_leaf (inline_extraction (true,[g]));
-      Lib.add_anonymous_leaf (in_ml_extraction (g,Ind,s));
+      Lib.add_anonymous_leaf (in_customs (g,Ind,s));
       list_iter_i
 	(fun j s -> 
 	   let g = ConstructRef (ip,succ j) in 
 	   Lib.add_anonymous_leaf (inline_extraction (true,[g]));
-	   Lib.add_anonymous_leaf (in_ml_extraction (g,Construct,s))) l
+	   Lib.add_anonymous_leaf (in_customs (g,Construct,s))) l
   | _ -> error_inductive g 
 
 
-(*S The other tables: constants, inductives, records, ... *)
-
-(*s Constants tables. *) 
-
-let terms = ref (KNmap.empty : ml_decl KNmap.t)
-let add_term kn d = terms := KNmap.add kn d !terms
-let lookup_term kn = KNmap.find kn !terms
-
-let types = ref (KNmap.empty : ml_schema KNmap.t)
-let add_type kn s = types := KNmap.add kn s !types
-let lookup_type kn = KNmap.find kn !types 
-
-(*s Inductives table. *)
-
-let inductives = ref (KNmap.empty : ml_ind KNmap.t)
-let add_ind kn m = inductives := KNmap.add kn m !inductives
-let lookup_ind kn = KNmap.find kn !inductives
-
-(*s Recursors table. *)
-
-let recursors = ref KNset.empty
-
-let add_recursors kn = 
-  let make_kn id = make_kn (modpath kn) empty_dirpath (label_of_id id) in 
-  let mib = Global.lookup_mind kn in 
-  Array.iter 
-    (fun mip -> 
-       let id = mip.mind_typename in 
-       let kn_rec = make_kn (Nameops.add_suffix id "_rec")
-       and kn_rect = make_kn (Nameops.add_suffix id "_rect") in 
-       recursors := KNset.add kn_rec (KNset.add kn_rect !recursors))
-    mib.mind_packets
-
-let is_recursor = function 
-  | ConstRef kn -> KNset.mem kn !recursors
-  | _ -> false
-
-(*s Record tables. *)
-
-let records = ref (KNmap.empty : global_reference list KNmap.t)
-let projs = ref Refset.empty
-
-let add_record kn l = 
-  records := KNmap.add kn l !records; 
-  projs := List.fold_right Refset.add l !projs
-
-let find_projections kn = KNmap.find kn !records
-let is_projection r = Refset.mem r !projs
-
-(*s Tables synchronization. *)
-
-let freeze () = !terms, !types, !inductives, !recursors, !records, !projs
-
-let unfreeze (te,ty,id,re,rd,pr) = 
-  terms:=te; types:=ty; inductives:=id; recursors:=re; records:=rd; projs:=pr
-
-let _ = declare_summary "Extraction tables"
-	  { freeze_function = freeze;
-	    unfreeze_function = unfreeze;
-	    init_function = (fun () -> ());
-	    survive_section = true }
-
-
-
-
-
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index e6495add6..917e7884a 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -12,6 +12,12 @@ open Names
 open Libnames
 open Miniml
 
+val cur_env : Environ.env ref
+
+val id_of_global : global_reference -> identifier
+
+val pr_global : global_reference -> Pp.std_ppcmds
+
 (*s Warning and Error messages. *)
 
 val error_axiom_scheme : global_reference -> 'a
@@ -19,9 +25,57 @@ val error_axiom : global_reference -> 'a
 val warning_axiom : global_reference -> unit
 val error_section : unit -> 'a
 val error_constant : global_reference -> 'a
+val error_fixpoint : global_reference -> 'a
 val error_type_scheme : 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 : identifier -> 'a
+val error_toplevel : unit -> 'a
+val error_scheme : unit -> 'a
+val error_not_visible : global_reference -> 'a
+val error_unqualified_name : string -> string -> 'a 
+
+(*s utilities concerning [module_path]. *)
+
+val current_toplevel : unit -> module_path
+
+val is_toplevel : module_path -> bool 
+val at_toplevel : module_path -> bool
+val base_mp : module_path -> module_path
+val prefixes_mp : module_path -> MPset.t
+val is_modfile : module_path -> bool 
+val modfile_of_mp : module_path -> module_path
+val fst_level_module_of_mp : module_path -> module_path * label
+val labels_of_mp : module_path -> module_path * label list 
+val labels_of_kn : kernel_name -> module_path * label list
+
+val is_something_opened : unit -> bool
+
+(*s Some table-related operations *)
+
+val add_term : kernel_name -> ml_decl -> unit
+val lookup_term : kernel_name -> ml_decl
+
+val add_type : kernel_name -> ml_schema -> unit
+val lookup_type : kernel_name -> ml_schema
+
+val add_ind : kernel_name -> ml_ind -> unit
+val lookup_ind : kernel_name -> ml_ind
+
+val add_recursors : Environ.env -> kernel_name -> unit
+val is_recursor : global_reference -> bool 
+
+val add_record : kernel_name -> global_reference list -> unit
+val find_projections : kernel_name -> global_reference list
+val is_projection : global_reference -> bool 
+
+val add_aliases : module_path -> module_path -> unit
+val long_mp : module_path -> module_path 
+val long_kn : kernel_name -> kernel_name
+val long_r : global_reference -> global_reference
+
+val reset_tables : unit -> unit
 
 (*s AutoInline parameter *) 
 
@@ -41,13 +95,14 @@ val lang : unit -> lang
 val to_inline : global_reference -> bool
 val to_keep : global_reference -> bool
 
-(*s Table for direct ML extractions. *)
+(*s Table for user-given custom ML extractions. *)
 
-val is_ml_extraction : global_reference -> bool
-val find_ml_extraction : global_reference -> string
-val ml_extractions : unit -> Refset.t
-val ml_type_extractions : unit -> (global_reference * string) list
-val ml_term_extractions : unit -> (global_reference * string) list
+val is_custom : global_reference -> bool
+val is_inline_custom : global_reference -> bool
+val find_custom : global_reference -> string
+val all_customs : unit -> Refset.t
+val type_customs : unit -> (global_reference * string) list
+val term_customs : unit -> (global_reference * string) list
 
 (*s Extraction commands. *)
 
@@ -58,22 +113,6 @@ val reset_extraction_inline : unit -> unit
 val extract_constant_inline : bool -> reference -> string -> unit
 val extract_inductive : reference -> string * string list -> unit
 
-(*s Some table-related operations *)
-
-val add_term : kernel_name -> ml_decl -> unit
-val lookup_term : kernel_name -> ml_decl
-
-val add_type : kernel_name -> ml_schema -> unit
-val lookup_type : kernel_name -> ml_schema
-
-val add_ind : kernel_name -> ml_ind -> unit
-val lookup_ind : kernel_name -> ml_ind
 
-val add_recursors : kernel_name -> unit
-val is_recursor : global_reference -> bool 
-
-val add_record : kernel_name -> global_reference list -> unit
-val find_projections : kernel_name -> global_reference list
-val is_projection : global_reference -> bool 
 
 
diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend
index 952a8e087..f70e81319 100644
--- a/contrib/extraction/test/.depend
+++ b/contrib/extraction/test/.depend
@@ -78,6 +78,12 @@ theories/Bool/bool.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \
     theories/Bool/bool.cmi 
 theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \
     theories/Bool/bool.cmi 
+theories/Bool/bvector.cmo: theories/Bool/bool.cmi theories/Init/datatypes.cmi \
+    theories/Arith/minus.cmi theories/Init/peano.cmi \
+    theories/Bool/bvector.cmi 
+theories/Bool/bvector.cmx: theories/Bool/bool.cmx theories/Init/datatypes.cmx \
+    theories/Arith/minus.cmx theories/Init/peano.cmx \
+    theories/Bool/bvector.cmi 
 theories/Bool/decBool.cmo: theories/Init/specif.cmi theories/Bool/decBool.cmi 
 theories/Bool/decBool.cmx: theories/Init/specif.cmx theories/Bool/decBool.cmi 
 theories/Bool/ifProp.cmo: theories/Init/datatypes.cmi \
@@ -156,16 +162,16 @@ theories/IntMap/fset.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
     theories/Init/specif.cmx theories/IntMap/fset.cmi 
 theories/IntMap/lsort.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
     theories/Bool/bool.cmi theories/Init/datatypes.cmi \
-    theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \
-    theories/IntMap/mapiter.cmi theories/Lists/polyList.cmi \
-    theories/Init/specif.cmi theories/Bool/sumbool.cmi \
-    theories/IntMap/lsort.cmi 
+    theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \
+    theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi \
+    theories/Bool/sumbool.cmi theories/IntMap/lsort.cmi 
 theories/IntMap/lsort.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \
     theories/Bool/bool.cmx theories/Init/datatypes.cmx \
-    theories/ZArith/fast_integer.cmx theories/IntMap/map.cmx \
-    theories/IntMap/mapiter.cmx theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx theories/Bool/sumbool.cmx \
-    theories/IntMap/lsort.cmi 
+    theories/ZArith/fast_integer.cmx theories/Init/logic.cmx \
+    theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \
+    theories/Lists/polyList.cmx theories/Init/specif.cmx \
+    theories/Bool/sumbool.cmx theories/IntMap/lsort.cmi 
 theories/IntMap/mapaxioms.cmo: theories/IntMap/mapaxioms.cmi 
 theories/IntMap/mapaxioms.cmx: theories/IntMap/mapaxioms.cmi 
 theories/IntMap/mapcanon.cmo: theories/IntMap/map.cmi \
@@ -174,13 +180,13 @@ theories/IntMap/mapcanon.cmx: theories/IntMap/map.cmx \
     theories/Init/specif.cmx theories/IntMap/mapcanon.cmi 
 theories/IntMap/mapcard.cmo: theories/IntMap/addec.cmi \
     theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
-    theories/IntMap/map.cmi theories/Init/peano.cmi \
+    theories/Init/logic.cmi theories/IntMap/map.cmi theories/Init/peano.cmi \
     theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \
     theories/Init/specif.cmi theories/Bool/sumbool.cmi \
     theories/IntMap/mapcard.cmi 
 theories/IntMap/mapcard.cmx: theories/IntMap/addec.cmx \
     theories/IntMap/addr.cmx theories/Init/datatypes.cmx \
-    theories/IntMap/map.cmx theories/Init/peano.cmx \
+    theories/Init/logic.cmx theories/IntMap/map.cmx theories/Init/peano.cmx \
     theories/Arith/peano_dec.cmx theories/Arith/plus.cmx \
     theories/Init/specif.cmx theories/Bool/sumbool.cmx \
     theories/IntMap/mapcard.cmi 
@@ -357,13 +363,15 @@ theories/Sets/uniset.cmo: theories/Init/datatypes.cmi \
 theories/Sets/uniset.cmx: theories/Init/datatypes.cmx \
     theories/Init/specif.cmx theories/Sets/uniset.cmi 
 theories/Sorting/heap.cmo: theories/Init/datatypes.cmi \
-    theories/Sets/multiset.cmi theories/Init/peano.cmi \
-    theories/Lists/polyList.cmi theories/Sorting/sorting.cmi \
-    theories/Init/specif.cmi theories/Sorting/heap.cmi 
+    theories/Init/logic.cmi theories/Sets/multiset.cmi \
+    theories/Init/peano.cmi theories/Lists/polyList.cmi \
+    theories/Sorting/sorting.cmi theories/Init/specif.cmi \
+    theories/Sorting/heap.cmi 
 theories/Sorting/heap.cmx: theories/Init/datatypes.cmx \
-    theories/Sets/multiset.cmx theories/Init/peano.cmx \
-    theories/Lists/polyList.cmx theories/Sorting/sorting.cmx \
-    theories/Init/specif.cmx theories/Sorting/heap.cmi 
+    theories/Init/logic.cmx theories/Sets/multiset.cmx \
+    theories/Init/peano.cmx theories/Lists/polyList.cmx \
+    theories/Sorting/sorting.cmx theories/Init/specif.cmx \
+    theories/Sorting/heap.cmi 
 theories/Sorting/permutation.cmo: theories/Init/datatypes.cmi \
     theories/Sets/multiset.cmi theories/Init/peano.cmi \
     theories/Lists/polyList.cmi theories/Init/specif.cmi \
@@ -372,10 +380,12 @@ theories/Sorting/permutation.cmx: theories/Init/datatypes.cmx \
     theories/Sets/multiset.cmx theories/Init/peano.cmx \
     theories/Lists/polyList.cmx theories/Init/specif.cmx \
     theories/Sorting/permutation.cmi 
-theories/Sorting/sorting.cmo: theories/Lists/polyList.cmi \
-    theories/Init/specif.cmi theories/Sorting/sorting.cmi 
-theories/Sorting/sorting.cmx: theories/Lists/polyList.cmx \
-    theories/Init/specif.cmx theories/Sorting/sorting.cmi 
+theories/Sorting/sorting.cmo: theories/Init/logic.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi \
+    theories/Sorting/sorting.cmi 
+theories/Sorting/sorting.cmx: theories/Init/logic.cmx \
+    theories/Lists/polyList.cmx theories/Init/specif.cmx \
+    theories/Sorting/sorting.cmi 
 theories/Wellfounded/disjoint_Union.cmo: \
     theories/Wellfounded/disjoint_Union.cmi 
 theories/Wellfounded/disjoint_Union.cmx: \
@@ -436,6 +446,14 @@ theories/ZArith/zArith_dec.cmx: theories/ZArith/fast_integer.cmx \
     theories/ZArith/zArith_dec.cmi 
 theories/ZArith/zArith.cmo: theories/ZArith/zArith.cmi 
 theories/ZArith/zArith.cmx: theories/ZArith/zArith.cmi 
+theories/ZArith/zbinary.cmo: theories/Bool/bvector.cmi \
+    theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \
+    theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi \
+    theories/ZArith/zbinary.cmi 
+theories/ZArith/zbinary.cmx: theories/Bool/bvector.cmx \
+    theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \
+    theories/ZArith/zarith_aux.cmx theories/ZArith/zmisc.cmx \
+    theories/ZArith/zbinary.cmi 
 theories/ZArith/zbool.cmo: theories/Init/datatypes.cmi \
     theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \
     theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \
@@ -473,11 +491,13 @@ theories/ZArith/zmisc.cmx: theories/Init/datatypes.cmx \
     theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \
     theories/ZArith/zmisc.cmi 
 theories/ZArith/zpower.cmo: theories/Init/datatypes.cmi \
-    theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \
-    theories/ZArith/zmisc.cmi theories/ZArith/zpower.cmi 
+    theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \
+    theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi \
+    theories/ZArith/zpower.cmi 
 theories/ZArith/zpower.cmx: theories/Init/datatypes.cmx \
-    theories/ZArith/fast_integer.cmx theories/ZArith/zarith_aux.cmx \
-    theories/ZArith/zmisc.cmx theories/ZArith/zpower.cmi 
+    theories/ZArith/fast_integer.cmx theories/Init/logic.cmx \
+    theories/ZArith/zarith_aux.cmx theories/ZArith/zmisc.cmx \
+    theories/ZArith/zpower.cmi 
 theories/ZArith/zsqrt.cmo: theories/ZArith/fast_integer.cmi \
     theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \
     theories/ZArith/zarith_aux.cmi theories/ZArith/zsqrt.cmi 
@@ -512,6 +532,8 @@ theories/Arith/wf_nat.cmi: theories/Init/datatypes.cmi
 theories/Bool/boolEq.cmi: theories/Init/datatypes.cmi \
     theories/Init/specif.cmi 
 theories/Bool/bool.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi 
+theories/Bool/bvector.cmi: theories/Bool/bool.cmi theories/Init/datatypes.cmi \
+    theories/Arith/minus.cmi theories/Init/peano.cmi 
 theories/Bool/decBool.cmi: theories/Init/specif.cmi 
 theories/Bool/ifProp.cmi: theories/Init/datatypes.cmi \
     theories/Init/specif.cmi 
@@ -537,14 +559,15 @@ theories/IntMap/fset.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
     theories/Init/specif.cmi 
 theories/IntMap/lsort.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \
     theories/Bool/bool.cmi theories/Init/datatypes.cmi \
-    theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \
-    theories/IntMap/mapiter.cmi theories/Lists/polyList.cmi \
-    theories/Init/specif.cmi theories/Bool/sumbool.cmi 
+    theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \
+    theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi \
+    theories/Bool/sumbool.cmi 
 theories/IntMap/mapcanon.cmi: theories/IntMap/map.cmi \
     theories/Init/specif.cmi 
 theories/IntMap/mapcard.cmi: theories/IntMap/addec.cmi \
     theories/IntMap/addr.cmi theories/Init/datatypes.cmi \
-    theories/IntMap/map.cmi theories/Init/peano.cmi \
+    theories/Init/logic.cmi theories/IntMap/map.cmi theories/Init/peano.cmi \
     theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \
     theories/Init/specif.cmi theories/Bool/sumbool.cmi 
 theories/IntMap/mapfold.cmi: theories/IntMap/addr.cmi \
@@ -584,14 +607,14 @@ theories/Sets/powerset.cmi: theories/Sets/partial_Order.cmi
 theories/Sets/uniset.cmi: theories/Init/datatypes.cmi \
     theories/Init/specif.cmi 
 theories/Sorting/heap.cmi: theories/Init/datatypes.cmi \
-    theories/Sets/multiset.cmi theories/Init/peano.cmi \
-    theories/Lists/polyList.cmi theories/Sorting/sorting.cmi \
-    theories/Init/specif.cmi 
+    theories/Init/logic.cmi theories/Sets/multiset.cmi \
+    theories/Init/peano.cmi theories/Lists/polyList.cmi \
+    theories/Sorting/sorting.cmi theories/Init/specif.cmi 
 theories/Sorting/permutation.cmi: theories/Init/datatypes.cmi \
     theories/Sets/multiset.cmi theories/Init/peano.cmi \
     theories/Lists/polyList.cmi theories/Init/specif.cmi 
-theories/Sorting/sorting.cmi: theories/Lists/polyList.cmi \
-    theories/Init/specif.cmi 
+theories/Sorting/sorting.cmi: theories/Init/logic.cmi \
+    theories/Lists/polyList.cmi theories/Init/specif.cmi 
 theories/Wellfounded/well_Ordering.cmi: theories/Init/specif.cmi 
 theories/ZArith/fast_integer.cmi: theories/Init/datatypes.cmi \
     theories/Init/peano.cmi 
@@ -602,6 +625,9 @@ theories/ZArith/zarith_aux.cmi: theories/Init/datatypes.cmi \
     theories/ZArith/fast_integer.cmi theories/Init/specif.cmi 
 theories/ZArith/zArith_dec.cmi: theories/ZArith/fast_integer.cmi \
     theories/Init/specif.cmi theories/Bool/sumbool.cmi 
+theories/ZArith/zbinary.cmi: theories/Bool/bvector.cmi \
+    theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \
+    theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi 
 theories/ZArith/zbool.cmi: theories/Init/datatypes.cmi \
     theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \
     theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \
@@ -618,8 +644,8 @@ theories/ZArith/zlogarithm.cmi: theories/ZArith/fast_integer.cmi \
 theories/ZArith/zmisc.cmi: theories/Init/datatypes.cmi \
     theories/ZArith/fast_integer.cmi theories/Init/specif.cmi 
 theories/ZArith/zpower.cmi: theories/Init/datatypes.cmi \
-    theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \
-    theories/ZArith/zmisc.cmi 
+    theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \
+    theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi 
 theories/ZArith/zsqrt.cmi: theories/ZArith/fast_integer.cmi \
     theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \
     theories/ZArith/zarith_aux.cmi 
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 646e8b6ba..4ab5fe7fb 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -42,8 +42,8 @@ depend: $(ML)
 tree:
 	mkdir -p $(DIRS)
 
-%.mli:%.ml
-	./make_mli $< > $@
+#%.mli:%.ml
+#	./make_mli $< > $@
 
 %.cmi:%.mli
 	ocamlc $(INCL) -c -i $<
diff --git a/contrib/extraction/test/Makefile.haskell b/contrib/extraction/test/Makefile.haskell
index 347e99887..bd50f9bf5 100644
--- a/contrib/extraction/test/Makefile.haskell
+++ b/contrib/extraction/test/Makefile.haskell
@@ -7,6 +7,7 @@ TOPDIR=../../..
 # Files with axioms to be realized: can't be extracted directly
 
 AXIOMSVO:= \
+theories/Init/PeanoSyntax.vo \
 theories/Init/Prelude.vo \
 theories/Arith/Arith.vo \
 theories/Lists/List.vo \
@@ -68,69 +69,77 @@ v2hs: v2hs.ml
 
 # DO NOT DELETE: Beginning of Haskell dependencies
 theories/Arith/Between.o : theories/Arith/Between.hs
-theories/Arith/Compare.o : theories/Arith/Compare.hs
-theories/Arith/Compare.o : theories/Arith/Compare_dec.o
-theories/Arith/Compare.o : theories/Init/Specif.o
+theories/Arith/Bool_nat.o : theories/Arith/Bool_nat.hs
+theories/Arith/Bool_nat.o : theories/Bool/Sumbool.o
+theories/Arith/Bool_nat.o : theories/Init/Specif.o
+theories/Arith/Bool_nat.o : theories/Arith/Peano_dec.o
+theories/Arith/Bool_nat.o : theories/Init/Datatypes.o
+theories/Arith/Bool_nat.o : theories/Arith/Compare_dec.o
 theories/Arith/Compare_dec.o : theories/Arith/Compare_dec.hs
-theories/Arith/Compare_dec.o : theories/Init/Datatypes.o
-theories/Arith/Compare_dec.o : theories/Init/Logic.o
 theories/Arith/Compare_dec.o : theories/Init/Specif.o
+theories/Arith/Compare_dec.o : theories/Init/Logic.o
+theories/Arith/Compare_dec.o : theories/Init/Datatypes.o
+theories/Arith/Compare.o : theories/Arith/Compare.hs
+theories/Arith/Compare.o : theories/Init/Specif.o
+theories/Arith/Compare.o : theories/Init/Datatypes.o
+theories/Arith/Compare.o : theories/Arith/Compare_dec.o
 theories/Arith/Div2.o : theories/Arith/Div2.hs
-theories/Arith/Div2.o : theories/Init/Datatypes.o
+theories/Arith/Div2.o : theories/Init/Specif.o
 theories/Arith/Div2.o : theories/Init/Peano.o
+theories/Arith/Div2.o : theories/Init/Datatypes.o
 theories/Arith/EqNat.o : theories/Arith/EqNat.hs
-theories/Arith/EqNat.o : theories/Init/Datatypes.o
 theories/Arith/EqNat.o : theories/Init/Specif.o
-theories/Arith/Euclid.o : theories/Arith/Compare_dec.o
+theories/Arith/EqNat.o : theories/Init/Datatypes.o
 theories/Arith/Euclid.o : theories/Arith/Euclid.hs
-theories/Arith/Euclid.o : theories/Arith/Minus.o
 theories/Arith/Euclid.o : theories/Arith/Wf_nat.o
-theories/Arith/Euclid.o : theories/Init/Datatypes.o
 theories/Arith/Euclid.o : theories/Init/Specif.o
+theories/Arith/Euclid.o : theories/Arith/Minus.o
+theories/Arith/Euclid.o : theories/Init/Datatypes.o
+theories/Arith/Euclid.o : theories/Arith/Compare_dec.o
 theories/Arith/Even.o : theories/Arith/Even.hs
-theories/Arith/Even.o : theories/Init/Datatypes.o
 theories/Arith/Even.o : theories/Init/Specif.o
+theories/Arith/Even.o : theories/Init/Datatypes.o
 theories/Arith/Gt.o : theories/Arith/Gt.hs
 theories/Arith/Le.o : theories/Arith/Le.hs
 theories/Arith/Lt.o : theories/Arith/Lt.hs
 theories/Arith/Max.o : theories/Arith/Max.hs
-theories/Arith/Max.o : theories/Init/Datatypes.o
-theories/Arith/Max.o : theories/Init/Logic.o
 theories/Arith/Max.o : theories/Init/Specif.o
+theories/Arith/Max.o : theories/Init/Logic.o
+theories/Arith/Max.o : theories/Init/Datatypes.o
 theories/Arith/Min.o : theories/Arith/Min.hs
-theories/Arith/Min.o : theories/Init/Datatypes.o
-theories/Arith/Min.o : theories/Init/Logic.o
 theories/Arith/Min.o : theories/Init/Specif.o
+theories/Arith/Min.o : theories/Init/Logic.o
+theories/Arith/Min.o : theories/Init/Datatypes.o
 theories/Arith/Minus.o : theories/Arith/Minus.hs
 theories/Arith/Minus.o : theories/Init/Datatypes.o
 theories/Arith/Mult.o : theories/Arith/Mult.hs
 theories/Arith/Mult.o : theories/Arith/Plus.o
 theories/Arith/Mult.o : theories/Init/Datatypes.o
 theories/Arith/Peano_dec.o : theories/Arith/Peano_dec.hs
-theories/Arith/Peano_dec.o : theories/Init/Datatypes.o
 theories/Arith/Peano_dec.o : theories/Init/Specif.o
+theories/Arith/Peano_dec.o : theories/Init/Datatypes.o
 theories/Arith/Plus.o : theories/Arith/Plus.hs
-theories/Arith/Plus.o : theories/Init/Datatypes.o
-theories/Arith/Plus.o : theories/Init/Logic.o
 theories/Arith/Plus.o : theories/Init/Specif.o
+theories/Arith/Plus.o : theories/Init/Logic.o
+theories/Arith/Plus.o : theories/Init/Datatypes.o
 theories/Arith/Wf_nat.o : theories/Arith/Wf_nat.hs
-theories/Arith/Wf_nat.o : theories/Init/Datatypes.o
-theories/Arith/Wf_nat.o : theories/Init/Logic.o
 theories/Arith/Wf_nat.o : theories/Init/Wf.o
-theories/Bool/Bool.o : theories/Bool/Bool.hs
-theories/Bool/Bool.o : theories/Init/Datatypes.o
-theories/Bool/Bool.o : theories/Init/Specif.o
+theories/Arith/Wf_nat.o : theories/Init/Logic.o
+theories/Arith/Wf_nat.o : theories/Init/Datatypes.o
 theories/Bool/BoolEq.o : theories/Bool/BoolEq.hs
-theories/Bool/BoolEq.o : theories/Init/Datatypes.o
 theories/Bool/BoolEq.o : theories/Init/Specif.o
+theories/Bool/BoolEq.o : theories/Init/Datatypes.o
+theories/Bool/Bool.o : theories/Bool/Bool.hs
+theories/Bool/Bool.o : theories/Init/Specif.o
+theories/Bool/Bool.o : theories/Init/Datatypes.o
 theories/Bool/DecBool.o : theories/Bool/DecBool.hs
 theories/Bool/DecBool.o : theories/Init/Specif.o
 theories/Bool/IfProp.o : theories/Bool/IfProp.hs
-theories/Bool/IfProp.o : theories/Init/Datatypes.o
 theories/Bool/IfProp.o : theories/Init/Specif.o
+theories/Bool/IfProp.o : theories/Init/Datatypes.o
 theories/Bool/Sumbool.o : theories/Bool/Sumbool.hs
-theories/Bool/Sumbool.o : theories/Init/Datatypes.o
 theories/Bool/Sumbool.o : theories/Init/Specif.o
+theories/Bool/Sumbool.o : theories/Init/Datatypes.o
 theories/Bool/Zerob.o : theories/Bool/Zerob.hs
 theories/Bool/Zerob.o : theories/Init/Datatypes.o
 theories/Init/Datatypes.o : theories/Init/Datatypes.hs
@@ -139,188 +148,200 @@ theories/Init/Logic.o : theories/Init/Logic.hs
 theories/Init/LogicSyntax.o : theories/Init/LogicSyntax.hs
 theories/Init/Logic_Type.o : theories/Init/Logic_Type.hs
 theories/Init/Logic_TypeSyntax.o : theories/Init/Logic_TypeSyntax.hs
-theories/Init/Peano.o : theories/Init/Datatypes.o
 theories/Init/Peano.o : theories/Init/Peano.hs
-theories/Init/Specif.o : theories/Init/Datatypes.o
-theories/Init/Specif.o : theories/Init/Logic.o
+theories/Init/Peano.o : theories/Init/Datatypes.o
 theories/Init/Specif.o : theories/Init/Specif.hs
+theories/Init/Specif.o : theories/Init/Logic.o
+theories/Init/Specif.o : theories/Init/Datatypes.o
 theories/Init/SpecifSyntax.o : theories/Init/SpecifSyntax.hs
 theories/Init/Wf.o : theories/Init/Wf.hs
+theories/IntMap/Adalloc.o : theories/IntMap/Adalloc.hs
+theories/IntMap/Adalloc.o : theories/ZArith/Fast_integer.o
 theories/IntMap/Adalloc.o : theories/Bool/Sumbool.o
-theories/IntMap/Adalloc.o : theories/Init/Datatypes.o
-theories/IntMap/Adalloc.o : theories/Init/Logic.o
 theories/IntMap/Adalloc.o : theories/Init/Specif.o
-theories/IntMap/Adalloc.o : theories/IntMap/Adalloc.hs
-theories/IntMap/Adalloc.o : theories/IntMap/Addec.o
-theories/IntMap/Adalloc.o : theories/IntMap/Addr.o
 theories/IntMap/Adalloc.o : theories/IntMap/Map.o
-theories/IntMap/Adalloc.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Adalloc.o : theories/Init/Logic.o
+theories/IntMap/Adalloc.o : theories/Init/Datatypes.o
+theories/IntMap/Adalloc.o : theories/IntMap/Addr.o
+theories/IntMap/Adalloc.o : theories/IntMap/Addec.o
+theories/IntMap/Addec.o : theories/IntMap/Addec.hs
+theories/IntMap/Addec.o : theories/ZArith/Fast_integer.o
 theories/IntMap/Addec.o : theories/Bool/Sumbool.o
-theories/IntMap/Addec.o : theories/Init/Datatypes.o
 theories/IntMap/Addec.o : theories/Init/Specif.o
-theories/IntMap/Addec.o : theories/IntMap/Addec.hs
+theories/IntMap/Addec.o : theories/Init/Datatypes.o
 theories/IntMap/Addec.o : theories/IntMap/Addr.o
-theories/IntMap/Addec.o : theories/ZArith/Fast_integer.o
-theories/IntMap/Addr.o : theories/Bool/Bool.o
-theories/IntMap/Addr.o : theories/Init/Datatypes.o
-theories/IntMap/Addr.o : theories/Init/Specif.o
 theories/IntMap/Addr.o : theories/IntMap/Addr.hs
 theories/IntMap/Addr.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Addr.o : theories/Init/Specif.o
+theories/IntMap/Addr.o : theories/Init/Datatypes.o
+theories/IntMap/Addr.o : theories/Bool/Bool.o
+theories/IntMap/Adist.o : theories/IntMap/Adist.hs
+theories/IntMap/Adist.o : theories/ZArith/Fast_integer.o
 theories/IntMap/Adist.o : theories/Arith/Min.o
 theories/IntMap/Adist.o : theories/Init/Datatypes.o
 theories/IntMap/Adist.o : theories/IntMap/Addr.o
-theories/IntMap/Adist.o : theories/IntMap/Adist.hs
-theories/IntMap/Adist.o : theories/ZArith/Fast_integer.o
 theories/IntMap/Allmaps.o : theories/IntMap/Allmaps.hs
-theories/IntMap/Fset.o : theories/Init/Datatypes.o
-theories/IntMap/Fset.o : theories/Init/Logic.o
-theories/IntMap/Fset.o : theories/Init/Specif.o
-theories/IntMap/Fset.o : theories/IntMap/Addec.o
-theories/IntMap/Fset.o : theories/IntMap/Addr.o
 theories/IntMap/Fset.o : theories/IntMap/Fset.hs
+theories/IntMap/Fset.o : theories/Init/Specif.o
 theories/IntMap/Fset.o : theories/IntMap/Map.o
-theories/IntMap/Lsort.o : theories/Bool/Bool.o
+theories/IntMap/Fset.o : theories/Init/Logic.o
+theories/IntMap/Fset.o : theories/Init/Datatypes.o
+theories/IntMap/Fset.o : theories/IntMap/Addr.o
+theories/IntMap/Fset.o : theories/IntMap/Addec.o
+theories/IntMap/Lsort.o : theories/IntMap/Lsort.hs
+theories/IntMap/Lsort.o : theories/ZArith/Fast_integer.o
 theories/IntMap/Lsort.o : theories/Bool/Sumbool.o
-theories/IntMap/Lsort.o : theories/Init/Datatypes.o
-theories/IntMap/Lsort.o : theories/Init/Logic.o
 theories/IntMap/Lsort.o : theories/Init/Specif.o
-theories/IntMap/Lsort.o : theories/IntMap/Addec.o
-theories/IntMap/Lsort.o : theories/IntMap/Addr.o
-theories/IntMap/Lsort.o : theories/IntMap/Lsort.hs
-theories/IntMap/Lsort.o : theories/IntMap/Mapiter.o
 theories/IntMap/Lsort.o : theories/Lists/PolyList.o
-theories/IntMap/Lsort.o : theories/ZArith/Fast_integer.o
-theories/IntMap/Map.o : theories/Init/Datatypes.o
-theories/IntMap/Map.o : theories/Init/Peano.o
-theories/IntMap/Map.o : theories/Init/Specif.o
-theories/IntMap/Map.o : theories/IntMap/Addec.o
-theories/IntMap/Map.o : theories/IntMap/Addr.o
-theories/IntMap/Map.o : theories/IntMap/Map.hs
-theories/IntMap/Map.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Lsort.o : theories/IntMap/Mapiter.o
+theories/IntMap/Lsort.o : theories/IntMap/Map.o
+theories/IntMap/Lsort.o : theories/Init/Logic.o
+theories/IntMap/Lsort.o : theories/Init/Datatypes.o
+theories/IntMap/Lsort.o : theories/Bool/Bool.o
+theories/IntMap/Lsort.o : theories/IntMap/Addr.o
+theories/IntMap/Lsort.o : theories/IntMap/Addec.o
 theories/IntMap/Mapaxioms.o : theories/IntMap/Mapaxioms.hs
-theories/IntMap/Mapc.o : theories/IntMap/Mapc.hs
-theories/IntMap/Mapcanon.o : theories/IntMap/Map.o
 theories/IntMap/Mapcanon.o : theories/IntMap/Mapcanon.hs
-theories/IntMap/Mapcard.o : theories/Arith/Peano_dec.o
-theories/IntMap/Mapcard.o : theories/Arith/Plus.o
+theories/IntMap/Mapcanon.o : theories/Init/Specif.o
+theories/IntMap/Mapcanon.o : theories/IntMap/Map.o
+theories/IntMap/Mapcard.o : theories/IntMap/Mapcard.hs
 theories/IntMap/Mapcard.o : theories/Bool/Sumbool.o
-theories/IntMap/Mapcard.o : theories/Init/Datatypes.o
-theories/IntMap/Mapcard.o : theories/Init/Logic.o
-theories/IntMap/Mapcard.o : theories/Init/Peano.o
 theories/IntMap/Mapcard.o : theories/Init/Specif.o
-theories/IntMap/Mapcard.o : theories/IntMap/Addec.o
-theories/IntMap/Mapcard.o : theories/IntMap/Addr.o
+theories/IntMap/Mapcard.o : theories/Arith/Plus.o
+theories/IntMap/Mapcard.o : theories/Arith/Peano_dec.o
+theories/IntMap/Mapcard.o : theories/Init/Peano.o
 theories/IntMap/Mapcard.o : theories/IntMap/Map.o
-theories/IntMap/Mapcard.o : theories/IntMap/Mapcard.hs
-theories/IntMap/Mapfold.o : theories/Init/Datatypes.o
-theories/IntMap/Mapfold.o : theories/Init/Logic.o
-theories/IntMap/Mapfold.o : theories/Init/Specif.o
-theories/IntMap/Mapfold.o : theories/IntMap/Fset.o
-theories/IntMap/Mapfold.o : theories/IntMap/Map.o
+theories/IntMap/Mapcard.o : theories/Init/Logic.o
+theories/IntMap/Mapcard.o : theories/Init/Datatypes.o
+theories/IntMap/Mapcard.o : theories/IntMap/Addr.o
+theories/IntMap/Mapcard.o : theories/IntMap/Addec.o
+theories/IntMap/Mapc.o : theories/IntMap/Mapc.hs
 theories/IntMap/Mapfold.o : theories/IntMap/Mapfold.hs
+theories/IntMap/Mapfold.o : theories/Init/Specif.o
 theories/IntMap/Mapfold.o : theories/IntMap/Mapiter.o
+theories/IntMap/Mapfold.o : theories/IntMap/Map.o
+theories/IntMap/Mapfold.o : theories/Init/Logic.o
+theories/IntMap/Mapfold.o : theories/IntMap/Fset.o
+theories/IntMap/Mapfold.o : theories/Init/Datatypes.o
+theories/IntMap/Mapfold.o : theories/IntMap/Addr.o
+theories/IntMap/Map.o : theories/IntMap/Map.hs
+theories/IntMap/Map.o : theories/ZArith/Fast_integer.o
+theories/IntMap/Map.o : theories/Init/Specif.o
+theories/IntMap/Map.o : theories/Init/Peano.o
+theories/IntMap/Map.o : theories/Init/Datatypes.o
+theories/IntMap/Map.o : theories/IntMap/Addr.o
+theories/IntMap/Map.o : theories/IntMap/Addec.o
+theories/IntMap/Mapiter.o : theories/IntMap/Mapiter.hs
 theories/IntMap/Mapiter.o : theories/Bool/Sumbool.o
-theories/IntMap/Mapiter.o : theories/Init/Datatypes.o
-theories/IntMap/Mapiter.o : theories/Init/Logic.o
 theories/IntMap/Mapiter.o : theories/Init/Specif.o
-theories/IntMap/Mapiter.o : theories/IntMap/Addec.o
-theories/IntMap/Mapiter.o : theories/IntMap/Addr.o
-theories/IntMap/Mapiter.o : theories/IntMap/Map.o
-theories/IntMap/Mapiter.o : theories/IntMap/Mapiter.hs
 theories/IntMap/Mapiter.o : theories/Lists/PolyList.o
-theories/IntMap/Maplists.o : theories/Bool/Bool.o
+theories/IntMap/Mapiter.o : theories/IntMap/Map.o
+theories/IntMap/Mapiter.o : theories/Init/Logic.o
+theories/IntMap/Mapiter.o : theories/Init/Datatypes.o
+theories/IntMap/Mapiter.o : theories/IntMap/Addr.o
+theories/IntMap/Mapiter.o : theories/IntMap/Addec.o
+theories/IntMap/Maplists.o : theories/IntMap/Maplists.hs
 theories/IntMap/Maplists.o : theories/Bool/Sumbool.o
-theories/IntMap/Maplists.o : theories/Init/Datatypes.o
-theories/IntMap/Maplists.o : theories/Init/Logic.o
 theories/IntMap/Maplists.o : theories/Init/Specif.o
-theories/IntMap/Maplists.o : theories/IntMap/Addec.o
-theories/IntMap/Maplists.o : theories/IntMap/Map.o
-theories/IntMap/Maplists.o : theories/IntMap/Mapiter.o
-theories/IntMap/Maplists.o : theories/IntMap/Maplists.hs
 theories/IntMap/Maplists.o : theories/Lists/PolyList.o
-theories/IntMap/Mapsubset.o : theories/Bool/Bool.o
-theories/IntMap/Mapsubset.o : theories/Init/Datatypes.o
-theories/IntMap/Mapsubset.o : theories/IntMap/Fset.o
-theories/IntMap/Mapsubset.o : theories/IntMap/Map.o
-theories/IntMap/Mapsubset.o : theories/IntMap/Mapiter.o
+theories/IntMap/Maplists.o : theories/IntMap/Mapiter.o
+theories/IntMap/Maplists.o : theories/IntMap/Map.o
+theories/IntMap/Maplists.o : theories/Init/Logic.o
+theories/IntMap/Maplists.o : theories/IntMap/Fset.o
+theories/IntMap/Maplists.o : theories/Init/Datatypes.o
+theories/IntMap/Maplists.o : theories/Bool/Bool.o
+theories/IntMap/Maplists.o : theories/IntMap/Addr.o
+theories/IntMap/Maplists.o : theories/IntMap/Addec.o
 theories/IntMap/Mapsubset.o : theories/IntMap/Mapsubset.hs
-theories/Lists/ListSet.o : theories/Init/Datatypes.o
-theories/Lists/ListSet.o : theories/Init/Logic.o
-theories/Lists/ListSet.o : theories/Init/Specif.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Mapiter.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Map.o
+theories/IntMap/Mapsubset.o : theories/IntMap/Fset.o
+theories/IntMap/Mapsubset.o : theories/Init/Datatypes.o
+theories/IntMap/Mapsubset.o : theories/Bool/Bool.o
 theories/Lists/ListSet.o : theories/Lists/ListSet.hs
+theories/Lists/ListSet.o : theories/Init/Specif.o
 theories/Lists/ListSet.o : theories/Lists/PolyList.o
-theories/Lists/PolyList.o : theories/Init/Datatypes.o
-theories/Lists/PolyList.o : theories/Init/Specif.o
+theories/Lists/ListSet.o : theories/Init/Logic.o
+theories/Lists/ListSet.o : theories/Init/Datatypes.o
 theories/Lists/PolyList.o : theories/Lists/PolyList.hs
+theories/Lists/PolyList.o : theories/Init/Specif.o
+theories/Lists/PolyList.o : theories/Init/Datatypes.o
 theories/Lists/PolyListSyntax.o : theories/Lists/PolyListSyntax.hs
-theories/Lists/Streams.o : theories/Init/Datatypes.o
 theories/Lists/Streams.o : theories/Lists/Streams.hs
-theories/Lists/TheoryList.o : theories/Bool/DecBool.o
-theories/Lists/TheoryList.o : theories/Init/Datatypes.o
+theories/Lists/Streams.o : theories/Init/Datatypes.o
+theories/Lists/TheoryList.o : theories/Lists/TheoryList.hs
 theories/Lists/TheoryList.o : theories/Init/Specif.o
 theories/Lists/TheoryList.o : theories/Lists/PolyList.o
-theories/Lists/TheoryList.o : theories/Lists/TheoryList.hs
+theories/Lists/TheoryList.o : theories/Bool/DecBool.o
+theories/Lists/TheoryList.o : theories/Init/Datatypes.o
 theories/Logic/Berardi.o : theories/Logic/Berardi.hs
+theories/Logic/ClassicalFacts.o : theories/Logic/ClassicalFacts.hs
 theories/Logic/Classical.o : theories/Logic/Classical.hs
 theories/Logic/Classical_Pred_Set.o : theories/Logic/Classical_Pred_Set.hs
 theories/Logic/Classical_Pred_Type.o : theories/Logic/Classical_Pred_Type.hs
 theories/Logic/Classical_Prop.o : theories/Logic/Classical_Prop.hs
 theories/Logic/Classical_Type.o : theories/Logic/Classical_Type.hs
 theories/Logic/Decidable.o : theories/Logic/Decidable.hs
-theories/Logic/Elimdep.o : theories/Logic/Elimdep.hs
-theories/Logic/Eqdep.o : theories/Logic/Eqdep.hs
 theories/Logic/Eqdep_dec.o : theories/Logic/Eqdep_dec.hs
+theories/Logic/Eqdep.o : theories/Logic/Eqdep.hs
+theories/Logic/Hurkens.o : theories/Logic/Hurkens.hs
 theories/Logic/JMeq.o : theories/Logic/JMeq.hs
+theories/Logic/ProofIrrelevance.o : theories/Logic/ProofIrrelevance.hs
 theories/Relations/Newman.o : theories/Relations/Newman.hs
 theories/Relations/Operators_Properties.o : theories/Relations/Operators_Properties.hs
 theories/Relations/Relation_Definitions.o : theories/Relations/Relation_Definitions.hs
 theories/Relations/Relation_Operators.o : theories/Relations/Relation_Operators.hs
+theories/Relations/Relation_Operators.o : theories/Init/Specif.o
+theories/Relations/Relation_Operators.o : theories/Lists/PolyList.o
 theories/Relations/Relations.o : theories/Relations/Relations.hs
 theories/Relations/Rstar.o : theories/Relations/Rstar.hs
 theories/Setoids/Setoid.o : theories/Setoids/Setoid.hs
 theories/Sets/Classical_sets.o : theories/Sets/Classical_sets.hs
 theories/Sets/Constructive_sets.o : theories/Sets/Constructive_sets.hs
 theories/Sets/Cpo.o : theories/Sets/Cpo.hs
+theories/Sets/Cpo.o : theories/Sets/Partial_Order.o
 theories/Sets/Ensembles.o : theories/Sets/Ensembles.hs
-theories/Sets/Finite_sets.o : theories/Sets/Finite_sets.hs
 theories/Sets/Finite_sets_facts.o : theories/Sets/Finite_sets_facts.hs
+theories/Sets/Finite_sets.o : theories/Sets/Finite_sets.hs
 theories/Sets/Image.o : theories/Sets/Image.hs
 theories/Sets/Infinite_sets.o : theories/Sets/Infinite_sets.hs
 theories/Sets/Integers.o : theories/Sets/Integers.hs
 theories/Sets/Integers.o : theories/Sets/Partial_Order.o
-theories/Sets/Multiset.o : theories/Init/Datatypes.o
-theories/Sets/Multiset.o : theories/Init/Peano.o
-theories/Sets/Multiset.o : theories/Init/Specif.o
+theories/Sets/Integers.o : theories/Init/Datatypes.o
 theories/Sets/Multiset.o : theories/Sets/Multiset.hs
+theories/Sets/Multiset.o : theories/Init/Specif.o
+theories/Sets/Multiset.o : theories/Init/Peano.o
+theories/Sets/Multiset.o : theories/Init/Datatypes.o
 theories/Sets/Partial_Order.o : theories/Sets/Partial_Order.hs
 theories/Sets/Permut.o : theories/Sets/Permut.hs
-theories/Sets/Powerset.o : theories/Sets/Partial_Order.o
-theories/Sets/Powerset.o : theories/Sets/Powerset.hs
 theories/Sets/Powerset_Classical_facts.o : theories/Sets/Powerset_Classical_facts.hs
 theories/Sets/Powerset_facts.o : theories/Sets/Powerset_facts.hs
-theories/Sets/Relations_1.o : theories/Sets/Relations_1.hs
+theories/Sets/Powerset.o : theories/Sets/Powerset.hs
+theories/Sets/Powerset.o : theories/Sets/Partial_Order.o
 theories/Sets/Relations_1_facts.o : theories/Sets/Relations_1_facts.hs
-theories/Sets/Relations_2.o : theories/Sets/Relations_2.hs
+theories/Sets/Relations_1.o : theories/Sets/Relations_1.hs
 theories/Sets/Relations_2_facts.o : theories/Sets/Relations_2_facts.hs
-theories/Sets/Relations_3.o : theories/Sets/Relations_3.hs
+theories/Sets/Relations_2.o : theories/Sets/Relations_2.hs
 theories/Sets/Relations_3_facts.o : theories/Sets/Relations_3_facts.hs
-theories/Sets/Uniset.o : theories/Bool/Bool.o
-theories/Sets/Uniset.o : theories/Init/Datatypes.o
-theories/Sets/Uniset.o : theories/Init/Specif.o
+theories/Sets/Relations_3.o : theories/Sets/Relations_3.hs
 theories/Sets/Uniset.o : theories/Sets/Uniset.hs
-theories/Sorting/Heap.o : theories/Init/Logic.o
+theories/Sets/Uniset.o : theories/Init/Specif.o
+theories/Sets/Uniset.o : theories/Init/Datatypes.o
+theories/Sets/Uniset.o : theories/Bool/Bool.o
+theories/Sorting/Heap.o : theories/Sorting/Heap.hs
 theories/Sorting/Heap.o : theories/Init/Specif.o
+theories/Sorting/Heap.o : theories/Sorting/Sorting.o
 theories/Sorting/Heap.o : theories/Lists/PolyList.o
 theories/Sorting/Heap.o : theories/Sets/Multiset.o
-theories/Sorting/Heap.o : theories/Sorting/Heap.hs
-theories/Sorting/Heap.o : theories/Sorting/Sorting.o
+theories/Sorting/Heap.o : theories/Init/Logic.o
+theories/Sorting/Permutation.o : theories/Sorting/Permutation.hs
+theories/Sorting/Permutation.o : theories/Init/Specif.o
 theories/Sorting/Permutation.o : theories/Lists/PolyList.o
 theories/Sorting/Permutation.o : theories/Sets/Multiset.o
-theories/Sorting/Permutation.o : theories/Sorting/Permutation.hs
-theories/Sorting/Sorting.o : theories/Init/Logic.o
+theories/Sorting/Sorting.o : theories/Sorting/Sorting.hs
 theories/Sorting/Sorting.o : theories/Init/Specif.o
 theories/Sorting/Sorting.o : theories/Lists/PolyList.o
-theories/Sorting/Sorting.o : theories/Sorting/Sorting.hs
+theories/Sorting/Sorting.o : theories/Init/Logic.o
 theories/Wellfounded/Disjoint_Union.o : theories/Wellfounded/Disjoint_Union.hs
 theories/Wellfounded/Inclusion.o : theories/Wellfounded/Inclusion.hs
 theories/Wellfounded/Inverse_Image.o : theories/Wellfounded/Inverse_Image.hs
@@ -328,51 +349,73 @@ theories/Wellfounded/Lexicographic_Exponentiation.o : theories/Wellfounded/Lexic
 theories/Wellfounded/Lexicographic_Product.o : theories/Wellfounded/Lexicographic_Product.hs
 theories/Wellfounded/Transitive_Closure.o : theories/Wellfounded/Transitive_Closure.hs
 theories/Wellfounded/Union.o : theories/Wellfounded/Union.hs
-theories/Wellfounded/Well_Ordering.o : theories/Init/Specif.o
-theories/Wellfounded/Well_Ordering.o : theories/Init/Wf.o
-theories/Wellfounded/Well_Ordering.o : theories/Wellfounded/Well_Ordering.hs
 theories/Wellfounded/Wellfounded.o : theories/Wellfounded/Wellfounded.hs
+theories/Wellfounded/Well_Ordering.o : theories/Wellfounded/Well_Ordering.hs
+theories/Wellfounded/Well_Ordering.o : theories/Init/Wf.o
+theories/Wellfounded/Well_Ordering.o : theories/Init/Specif.o
 theories/ZArith/Auxiliary.o : theories/ZArith/Auxiliary.hs
-theories/ZArith/Fast_integer.o : theories/Init/Datatypes.o
-theories/ZArith/Fast_integer.o : theories/Init/Peano.o
 theories/ZArith/Fast_integer.o : theories/ZArith/Fast_integer.hs
-theories/ZArith/Wf_Z.o : theories/Init/Datatypes.o
-theories/ZArith/Wf_Z.o : theories/Init/Logic.o
-theories/ZArith/Wf_Z.o : theories/Init/Peano.o
-theories/ZArith/Wf_Z.o : theories/Init/Specif.o
-theories/ZArith/Wf_Z.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Fast_integer.o : theories/Init/Peano.o
+theories/ZArith/Fast_integer.o : theories/Init/Datatypes.o
 theories/ZArith/Wf_Z.o : theories/ZArith/Wf_Z.hs
 theories/ZArith/Wf_Z.o : theories/ZArith/Zarith_aux.o
-theories/ZArith/ZArith.o : theories/ZArith/ZArith.hs
+theories/ZArith/Wf_Z.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Wf_Z.o : theories/Init/Specif.o
+theories/ZArith/Wf_Z.o : theories/Init/Peano.o
+theories/ZArith/Wf_Z.o : theories/Init/Logic.o
+theories/ZArith/Wf_Z.o : theories/Init/Datatypes.o
+theories/ZArith/Zarith_aux.o : theories/ZArith/Zarith_aux.hs
+theories/ZArith/Zarith_aux.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zarith_aux.o : theories/Init/Specif.o
+theories/ZArith/Zarith_aux.o : theories/Init/Datatypes.o
+theories/ZArith/ZArith_base.o : theories/ZArith/ZArith_base.hs
+theories/ZArith/ZArith_dec.o : theories/ZArith/ZArith_dec.hs
+theories/ZArith/ZArith_dec.o : theories/ZArith/Fast_integer.o
 theories/ZArith/ZArith_dec.o : theories/Bool/Sumbool.o
-theories/ZArith/ZArith_dec.o : theories/Init/Logic.o
 theories/ZArith/ZArith_dec.o : theories/Init/Specif.o
-theories/ZArith/ZArith_dec.o : theories/ZArith/Fast_integer.o
-theories/ZArith/ZArith_dec.o : theories/ZArith/ZArith_dec.hs
-theories/ZArith/Zarith_aux.o : theories/Init/Datatypes.o
-theories/ZArith/Zarith_aux.o : theories/Init/Specif.o
-theories/ZArith/Zarith_aux.o : theories/ZArith/Fast_integer.o
-theories/ZArith/Zarith_aux.o : theories/ZArith/Zarith_aux.hs
-theories/ZArith/Zcomplements.o : theories/Init/Datatypes.o
-theories/ZArith/Zcomplements.o : theories/Init/Logic.o
-theories/ZArith/Zcomplements.o : theories/Init/Specif.o
+theories/ZArith/ZArith_dec.o : theories/Init/Logic.o
+theories/ZArith/ZArith.o : theories/ZArith/ZArith.hs
+theories/ZArith/Zbool.o : theories/ZArith/Zbool.hs
+theories/ZArith/Zbool.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zbool.o : theories/ZArith/Zmisc.o
+theories/ZArith/Zbool.o : theories/ZArith/ZArith_dec.o
+theories/ZArith/Zbool.o : theories/Bool/Sumbool.o
+theories/ZArith/Zbool.o : theories/Init/Specif.o
+theories/ZArith/Zbool.o : theories/Init/Datatypes.o
+theories/ZArith/Zcomplements.o : theories/ZArith/Zcomplements.hs
+theories/ZArith/Zcomplements.o : theories/ZArith/Zarith_aux.o
 theories/ZArith/Zcomplements.o : theories/ZArith/Fast_integer.o
 theories/ZArith/Zcomplements.o : theories/ZArith/Wf_Z.o
-theories/ZArith/Zcomplements.o : theories/ZArith/ZArith_dec.o
-theories/ZArith/Zcomplements.o : theories/ZArith/Zarith_aux.o
-theories/ZArith/Zcomplements.o : theories/ZArith/Zcomplements.hs
+theories/ZArith/Zcomplements.o : theories/Init/Specif.o
+theories/ZArith/Zcomplements.o : theories/Init/Logic.o
+theories/ZArith/Zcomplements.o : theories/Init/Datatypes.o
+theories/ZArith/Zdiv.o : theories/ZArith/Zdiv.hs
+theories/ZArith/Zdiv.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zdiv.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zdiv.o : theories/ZArith/Zmisc.o
+theories/ZArith/Zdiv.o : theories/ZArith/ZArith_dec.o
+theories/ZArith/Zdiv.o : theories/Init/Specif.o
+theories/ZArith/Zdiv.o : theories/Init/Logic.o
+theories/ZArith/Zdiv.o : theories/Init/Datatypes.o
 theories/ZArith/Zhints.o : theories/ZArith/Zhints.hs
-theories/ZArith/Zlogarithm.o : theories/ZArith/Fast_integer.o
-theories/ZArith/Zlogarithm.o : theories/ZArith/Zarith_aux.o
 theories/ZArith/Zlogarithm.o : theories/ZArith/Zlogarithm.hs
-theories/ZArith/Zmisc.o : theories/Init/Datatypes.o
-theories/ZArith/Zmisc.o : theories/Init/Specif.o
-theories/ZArith/Zmisc.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zlogarithm.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zlogarithm.o : theories/ZArith/Fast_integer.o
 theories/ZArith/Zmisc.o : theories/ZArith/Zmisc.hs
-theories/ZArith/Zpower.o : theories/Init/Datatypes.o
-theories/ZArith/Zpower.o : theories/Init/Logic.o
-theories/ZArith/Zpower.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zmisc.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zmisc.o : theories/Init/Specif.o
+theories/ZArith/Zmisc.o : theories/Init/Datatypes.o
+theories/ZArith/Zpower.o : theories/ZArith/Zpower.hs
 theories/ZArith/Zpower.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zpower.o : theories/ZArith/Fast_integer.o
 theories/ZArith/Zpower.o : theories/ZArith/Zmisc.o
-theories/ZArith/Zpower.o : theories/ZArith/Zpower.hs
+theories/ZArith/Zpower.o : theories/Init/Logic.o
+theories/ZArith/Zpower.o : theories/Init/Datatypes.o
+theories/ZArith/Zsqrt.o : theories/ZArith/Zsqrt.hs
+theories/ZArith/Zsqrt.o : theories/ZArith/Zarith_aux.o
+theories/ZArith/Zsqrt.o : theories/ZArith/Fast_integer.o
+theories/ZArith/Zsqrt.o : theories/ZArith/ZArith_dec.o
+theories/ZArith/Zsqrt.o : theories/Init/Specif.o
+theories/ZArith/Zsqrt.o : theories/Init/Logic.o
+theories/ZArith/Zwf.o : theories/ZArith/Zwf.hs
 # DO NOT DELETE: End of Haskell dependencies