BIG MAJ Extraction:

------------------
- (Recursive) Extraction Module devient (Recursive) Extraction Library
  (pour cause d'ambiguite avec les nouveaux modules Coq).
- un nouveau Extraction Module qui extrait dans le toplevel tout module Coq
- tout fixpoint est de nouveau inlinable (Yves).
- fix bug du calcul d'env minimal des modules en extraction monolithique.
- un nouveau fichier Modutil regroupant manques de Modops & functions
  specifiques aux modules MiniML
- plus d'aliases a trainer (mais des substitutions des le depart)
- ET SURTOUT: un nommage correct (ou du moins moins pire) dans les modtypes
  et les functors.


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

19 files changed, 1008 insertions, 865 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 1a785fe73..fe0c06631 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -17,46 +17,9 @@ open Nameops
 open Libnames
 open Table
 open Miniml
-open Mlutil
+open Modutil
 open Ocaml
 
-(* 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 = 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 
-      | SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env 
-      | SEBmodtype mtb -> Environ.add_modtype kn mtb env  
-  in List.fold_left add_one env msb
-
-let add_functor mbid mtb env = 
-  Modops.add_module (MPbound mbid) (Modops.module_body_of_type mtb) env 
-
-(*s Get all references used in one [ml_structure]. *)
-
-module Orefset = struct 
-  type t = { set : Refset.t ; list : global_reference list }
-  let empty = { set = Refset.empty ; list = [] }
-  let add r o = 
-    if Refset.mem r o.set then o 
-    else { set = Refset.add r o.set ; list = r :: o.list }
-  let set o = o.set
-  let list o = o.list
-end
-
-type updown = { mutable up : Orefset.t ; mutable down : Orefset.t }
-
-let struct_get_references struc = 
-  let o = { up = Orefset.empty ; down = Orefset.empty } 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 
-  struct_iter_references do_term do_cons do_type struc; o
-
 (*S Renamings. *)
 
 (*s Tables of global renamings *)
@@ -69,7 +32,14 @@ let renamings = Hashtbl.create 97
 let rename r s = Hashtbl.add renamings r s
 let get_renamings r = Hashtbl.find renamings r 
 
-let must_qualify = ref Refset.empty
+let modvisited = ref MPset.empty
+let modcontents = ref Gset.empty
+let add_module_contents mp s = modcontents := Gset.add (mp,s) !modcontents
+let module_contents mp s = Gset.mem (mp,s) !modcontents
+
+let to_qualify = ref Refset.empty
+
+(*s Uppercase/lowercase renamings. *) 
 
 let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 
@@ -87,23 +57,21 @@ let modular_rename up id =
 
 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 print_labels = List.map (fun l -> rename_module (id_of_label l))
+
+let print_base_mp = function 
+  | MPfile d -> String.capitalize (string_of_id (List.hd (repr_dirpath d)))
+  | MPself msid -> rename_module (id_of_msid msid)
+  | MPbound mbid -> rename_module (id_of_mbid mbid)
+  | _ -> assert false
+
+(*s From a [module_path] to a list of [identifier]. *)
+
+let mp2l mp = 
+  let base_mp,l = labels_of_mp mp in 
+  if !modular || not (at_toplevel base_mp)
+  then (print_base_mp base_mp) :: (print_labels l)
+  else print_labels l 
 
 let string_of_modlist l = 
   List.fold_right (fun s s' -> if s' = "" then s else s ^ "." ^ s') l ""
@@ -111,86 +79,92 @@ let string_of_modlist 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 env = function 
-    | (l, SEBconst cb) -> 
-	(match Extraction.constant_kind 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
-    | _ -> ()
+(* [clash mp0 l s mpl] checks if [mp0-l-s] can be printed as [l-s] when 
+   [mpl] is the context of visible modules. More precisely, we check if 
+   there exists a mp1, module (sub-)path of an element of [mpl], such as 
+   module [mp1-l] contains [s]. 
+   The verification stops if we encounter [mp1=mp0]. *)
+
+exception Stop 
+
+let clash mp0 l s mpl = 
+  let rec clash_one mp = match mp with
+    | _ when mp = mp0 -> raise Stop
+    | MPdot (mp',_) -> 
+	(module_contents (add_labels_mp mp l) s) || (clash_one mp') 
+    | mp when is_toplevel mp -> false
+    | _ -> module_contents (add_labels_mp mp l) s
   in
-  match (Global.lookup_module mp).mod_expr with 
-    | Some (MEBstruct (msid,msb)) -> 
-	let env = add_structure (MPself msid) msb (Global.env ()) in 
-	List.iter (contents_seb env) msb; (mp,!s)
-    | _ -> mp,!s
-
-(* The previous functions might fail if [mp] isn't a directly visible module. *)
-(* Ex: [MPself] under functor, [MPbound], etc ... *)
-(* Exception [Not_found] is catched in [pp_global]. *) 
-
-let contents_first_level = 
-  let cache = ref MPmap.empty in 
-  fun mp -> 
-    try MPmap.find mp !cache 
-    with Not_found -> 
-      let res = contents_first_level mp in 
-      cache := MPmap.add mp res !cache; 
-      res
-
-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 (Global.lookup_module mp).mod_expr with 
-    | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; !s
-    | _ -> !s
+  let rec clash_list = function 
+    | [] -> false
+    | mp :: mpl -> (clash_one mp) || (clash_list mpl) 
+  in try clash_list mpl with Stop -> false
+
+(*s [contents_first_level mp] finds the names of the first-level objects 
+  exported by module [mp]. Nota: it might fail if [mp] isn't a directly 
+  visible module. Ex: [MPself] under functor, [MPbound], etc ... *)
 
-let 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 contents_first_level mp = 
+  if not (MPset.mem mp !modvisited) then begin 
+    modvisited := MPset.add mp !modvisited; 
+    match (Global.lookup_module mp).mod_type with 
+      | MTBsig (msid,msb) -> 
+	  let add b id = add_module_contents mp (modular_rename b id) in 
+	  let upper_type = (lang () = Haskell) in
+	  List.iter 
+	    (function 
+	       | (l, SPBconst cb) -> 
+		   (match Extraction.constant_kind (Global.env ()) cb with 
+		      | Extraction.Logical -> () 
+		      | Extraction.Type -> add upper_type (id_of_label l)
+		      | Extraction.Term -> add false (id_of_label l))
+	       | (_, SPBmind mib) ->
+		   Array.iter 
+		     (fun mip -> if mip.mind_sort <> (Prop Null) then begin
+			add upper_type mip.mind_typename; 
+			Array.iter (add true) mip.mind_consnames
+		      end)
+		     mib.mind_packets
+	       | _ -> ())
+	    (Modops.subst_signature_msid msid mp msb)
+      | _ -> ()
+  end
+
+(*s Initial renamings creation, for modular extraction. *) 
 
 let create_modular_renamings struc = 
-  let cur_mp = fst (List.hd struc) in
+  let current_module = fst (List.hd struc) in 
   let modfiles = ref MPset.empty in 
-  let { up = u ; down = d } = struct_get_references struc 
+  let { up = u ; down = d } = struct_get_references_set struc 
   in 
-  (* 1) create renamings of objects *)
+  (* 1) creates 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
+      if mp <> current_module 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)
+    Hashtbl.add renamings r s
   in
-  Refset.iter (add true) (Orefset.set u); 
-  Refset.iter (add false) (Orefset.set d); 
+  Refset.iter (add true) u; 
+  Refset.iter (add false) d; 
   
-  (* 2) determine the opened libraries and the potential clashes *)
+  (* 2) determines the opened libraries. *)
   let used_modules = MPset.elements !modfiles in 
-  let s = ref (modules_first_level cur_mp) in 
+
+  (* [s] will contain all first-level sub-modules of [cur_mp] *)
+  let s = ref Stringset.empty in 
+  begin 
+    let add l = s := Stringset.add (rename_module (id_of_label l)) !s in 
+    match (Global.lookup_module current_module).mod_type with 
+      | MTBsig (_,msb) ->
+	  List.iter (function (l,SPBmodule _) -> add l | _ -> ()) msb
+      | _ -> ()
+  end;
+  (* We now compare [s] with the modules coming from [used_modules]. *)
   List.iter 
     (function 
        | MPfile d -> 
@@ -200,22 +174,25 @@ let create_modular_renamings struc =
 	   else s:= Stringset.add s_mp !s 
        | _ -> assert false)
     used_modules;
-  let env = List.rev_map contents_first_level used_modules in 
+
+  (* 3) determines the potential clashes *)
+  List.iter contents_first_level used_modules; 
+  let used_modules' = List.rev used_modules in 
   let needs_qualify r = 
     let 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 
-  Refset.iter needs_qualify (Orefset.set u);
-  Refset.iter needs_qualify (Orefset.set d); 
+    if (is_modfile mp) && mp <> current_module && 
+      (clash mp [] (get_renamings r) used_modules')
+    then to_qualify := Refset.add r !to_qualify
+  in
+  Refset.iter needs_qualify u;
+  Refset.iter needs_qualify d; 
   used_modules
 
+(*s Initial renamings creation, for monolithic extraction. *)
+
 let create_mono_renamings struc = 
   let fst_level_modules = ref Idmap.empty in 
-  let { up = u ; down = d } = struct_get_references struc 
+  let { up = u ; down = d } = struct_get_references_list struc 
   in 
   (* 1) create renamings of objects *)
   let add upper r = 
@@ -228,18 +205,17 @@ let create_mono_renamings struc =
       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 
+      if at_toplevel (modpath (kn_of_r r)) 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)
+    Hashtbl.add renamings r (string_of_id id) 
   in
-  List.iter (add true) (List.rev (Orefset.list u)); 
-  List.iter (add false) (List.rev (Orefset.list d))
+  List.iter (add true) (List.rev u); 
+  List.iter (add false) (List.rev d)
 		    
 (*s Renaming issues at toplevel *)
 
@@ -252,63 +228,54 @@ 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 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 
+  (* TODO: remettre des conditions [lang () = Haskell] disant de qualifier. *)
+
+  let pp_global mpl r = 
+    let s = get_renamings 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 not (is_modfile (base_mp cur_mp)) && (is_modfile (base_mp mp)) then 
-      str (string_of_ren (mp_to_list' mp) s)
-    else
-      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 
-	  try 
-	    if clash_in_contents mp s (decreasing_contents cur_mp) 
-	    then str (string_of_ren l s)
-	    else str s
-	  with Not_found -> str (string_of_ren l s) 
+    let final = 
+      if mp = List.hd mpl then s (* simpliest situation *)
+      else 
+	try (* has [mp] something in common with one of those in [mpl] ? *)
+	  let pref = common_prefix_from_list mp mpl in 
+	  let l = labels_after_prefix pref mp in 
+	  if clash pref l s mpl 
+	  then error_unqualified_name (string_of_ren (print_labels l) s) 
+	    (string_of_modlist (mp2l (List.hd mpl)))
+	  else (string_of_ren (print_labels l) s)
+	with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
+	  let base, l = labels_of_mp mp in 
+	  let short = string_of_ren (print_labels l) s in
+	  if not (at_toplevel mp) ||
+	    (!modular && 
+	     (l <> [] || (Refset.mem r !to_qualify) || (clash base l s mpl)))
+	  then (print_base_mp base)^"."^short
+	  else short
+    in 
+    add_module_contents mp s; (* update the visible environment *)
+    str s
+
+  let pp_long_module mpl mp = 
+    try (* has [mp] something in common with one of those in [mpl] ? *)
+      let pref = common_prefix_from_list mp mpl in 
+      let l = labels_after_prefix pref mp in 
+(*i   TODO: comment adapter cela ??   
+      if clash pref l s mpl 
+      then error_unqualified_name (string_of_ren (print_labels l) s) 
+	(string_of_modlist (mp2l (List.hd mpl))) 
       else 
-	let nl = List.length l in 
-	if n = nl && nl < List.length cur_l then (* strict prefix *)
-	  try 
-	    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
-	  with Not_found -> str (string_of_ren l 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 cur_mp mp = 
-    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 mp = long_mp mp in 
-    let l = if !modular then mp_to_list mp else mp_to_list' mp in 
-    str (string_of_modlist (remove_common cur_l l))
+i*)	
+      str (string_of_modlist (print_labels l))
+    with Not_found -> (* [mp] is othogonal with every element of [mp]. *)
+      let base_mp, l = labels_of_mp mp in 
+      let short = string_of_modlist (print_labels l) in
+      if not (at_toplevel mp) || !modular 
+      then str ((print_base_mp base_mp)^(if short = "" then "" else "."^short))
+      else str short
 
   let pp_short_module id = str (rename_module id)
 end
@@ -342,7 +309,7 @@ let set_keywords () =
     | Scheme -> keywords := Scheme.keywords
     | Toplevel -> keywords := Idset.empty);
   global_ids := !keywords; 
-  must_qualify := Refset.empty
+  to_qualify := Refset.empty
     
 let preamble prm = match lang () with 
   | Ocaml -> Ocaml.preamble prm   
@@ -360,13 +327,15 @@ let print_one_decl struc mp decl =
   set_keywords (); 
   modular := false; 
   create_mono_renamings struc;
-  msgnl (pp_decl mp decl)
+  msgnl (pp_decl [mp] decl)
 
 (*S Extraction to a file. *)
 
 let print_structure_to_file f prm struc =
   cons_cofix := Refset.empty;
   Hashtbl.clear renamings;
+  modcontents := Gset.empty;
+  modvisited := MPset.empty; 
   set_keywords ();
   modular := prm.modular; 
   let used_modules =
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 2d3a7d47b..ea4d99623 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -8,18 +8,10 @@
 
 (*i $Id$ i*)
 
-open Pp
 open Names
-open Declarations
-open Environ
-open Libnames
 open Miniml
 open Mlutil
 
-val add_structure : module_path -> module_structure_body -> env -> env
-
-val add_functor : mod_bound_id -> module_type_body -> env -> env
-
 val print_one_decl :
   ml_structure -> module_path -> ml_decl -> unit
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 9170d4f24..0495e6244 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -17,7 +17,7 @@ open Util
 open Miniml
 open Table
 open Extraction
-open Mlutil
+open Modutil
 open Common
 
 (*s Obtaining Coq environment. *)
@@ -52,59 +52,14 @@ let environment_until dir_opt =
 	  | _ -> assert false
   in parse (Library.loaded_libraries ())
 
-(*s First, we parse everything in order to produce 
-   a table of aliases between short and long [module_path]. *)
-
-let rec init_aliases_seb loc abs = function 
-  | l, SEBmodule mb -> 
-      init_aliases_module loc (option_app (fun mp -> MPdot (mp,l)) abs) mb 
-  | l, SEBmodtype mtb -> init_aliases_modtype loc mtb 
-  | _ -> () 
-
-and init_aliases_module loc abs mb = 
-  option_iter (init_aliases_meb loc abs) mb.mod_expr
-
-and init_aliases_meb loc abs = function 
-  | MEBident mp -> ()
-  | MEBapply (meb, meb',_) -> 
-      init_aliases_meb loc None meb; init_aliases_meb loc None meb'
-  | MEBfunctor (mbid, mtb, meb) -> 
-      init_aliases_modtype loc mtb; 
-      init_aliases_meb loc None meb 
-  | MEBstruct (msid, msb) -> 
-      let loc = MPself msid in 
-      option_iter (add_aliases loc) abs; 
-      List.iter (init_aliases_seb loc abs) msb
-
-and init_aliases_modtype loc = function 
-  | MTBident mp -> ()
-  | MTBfunsig (mbid, mtb, mtb') -> 
-      init_aliases_modtype loc mtb; 
-      init_aliases_modtype loc mtb'
-  | MTBsig (msid, sign) -> 
-      let loc = MPself msid in
-      List.iter (init_aliases_spec loc) sign
-	
-and init_aliases_spec loc = function 
-  | l, SPBmodule {msb_modtype=mtb} -> init_aliases_modtype loc mtb 
-  | l, SPBmodtype mtb -> init_aliases_modtype loc mtb
-  | _ -> ()
-
-let init_aliases l =
-  List.iter 
-    (fun (mp,meb) -> init_aliases_meb (current_toplevel ()) (Some mp) meb) l
-
-(*s The extraction pass. *)
-
 type visit = { mutable kn : KNset.t; mutable mp : MPset.t }
 
-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 in_kn v kn = KNset.mem kn v.kn
+let in_mp v mp = MPset.mem 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
+let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp
+let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn)
+let visit_ref v r = visit_kn v (kn_of_r r) 
 
 exception Impossible
 
@@ -138,43 +93,67 @@ let factor_fix env l cb 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 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
 
 let get_spec_references v s = 
   let f = visit_ref v in spec_iter_references f f f s
 
-let rec extract_msb env v all loc = function 
+let rec extract_msig env v mp = function 
+  | [] -> [] 
+  | (l,SPBconst cb) :: msig -> 
+      let kn = make_kn mp empty_dirpath l in 
+      let s = extract_constant_spec env kn cb in 
+      if logical_spec s then extract_msig env v mp msig
+      else begin
+	get_spec_references v s; 
+	(l,Spec s) :: (extract_msig env v mp msig)
+      end
+  | (l,SPBmind cb) :: msig -> 
+      let kn = make_kn mp empty_dirpath l in 
+      let s = Sind (kn, extract_inductive env kn) in 
+      if logical_spec s then extract_msig env v mp msig
+      else begin 
+	get_spec_references v s; 
+	(l,Spec s) :: (extract_msig env v mp msig)
+      end
+  | (l,SPBmodule {msb_modtype=mtb}) :: msig -> 
+(*      let mpo = Some (MPdot (mp,l)) in  *)
+      (l,Smodule (extract_mtb env v None (* mpo *) mtb)) :: (extract_msig env v mp msig)
+  | (l,SPBmodtype mtb) :: msig -> 
+      (l,Smodtype (extract_mtb env v None mtb)) :: (extract_msig env v mp msig)
+
+and extract_mtb env v mpo = function 
+  | MTBident kn -> visit_kn v kn; MTident kn 
+  | MTBfunsig (mbid, mtb, mtb') -> 
+      let mp = MPbound mbid in 
+      let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in 
+      MTfunsig (mbid, extract_mtb env v None mtb, 
+		extract_mtb env' v None mtb') 
+  | MTBsig (msid, msig) -> 
+      let mp, msig = match mpo with 
+	| None -> MPself msid, msig
+	| Some mp -> mp, Modops.subst_signature_msid msid mp msig
+      in
+      let env' = Modops.add_signature mp msig env in 
+      MTsig (msid, extract_msig env' v mp msig) 
+
+let rec extract_msb env v mp all = function 
   | [] -> [] 
   | (l,SEBconst cb) :: msb -> 
       (try 
 	 let vl,recd,msb = factor_fix env 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 env v all loc msb in 
+	 let vkn = Array.map (fun id -> make_kn mp empty_dirpath id) vl in
+	 let ms = extract_msb env v mp all msb in 
 	 let b = array_exists (in_kn v) vkn in 
 	 if all || b then 
 	   let d = extract_fixpoint 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 begin get_decl_references v d; (l,SEdecl d) :: ms end
 	 else ms
        with Impossible ->
-	 let ms = extract_msb env v all loc msb in 
-	 let kn = make_kn loc empty_dirpath l in 
+	 let ms = extract_msb env v mp all msb in 
+	 let kn = make_kn mp empty_dirpath l in 
 	 let b = in_kn v kn in 
 	 if all || b then 
 	   let d = extract_constant env kn cb in
@@ -182,8 +161,8 @@ let rec extract_msb env v all loc = function
 	   else begin get_decl_references v d; (l,SEdecl d) :: ms end
 	 else ms)
   | (l,SEBmind mib) :: msb ->
-      let ms = extract_msb env v all loc msb in
-      let kn = make_kn loc empty_dirpath l in 
+      let ms = extract_msb env v mp all msb in
+      let kn = make_kn mp empty_dirpath l in 
       let b = in_kn v kn in 
       if all || b then 
 	let d = Dind (kn, extract_inductive env kn) in 
@@ -191,90 +170,46 @@ let rec extract_msb env v all loc = function
 	else begin get_decl_references v d; (l,SEdecl d) :: ms end
       else ms
   | (l,SEBmodule mb) :: msb -> 
-      let ms = extract_msb env v all loc msb in
-      let loc = MPdot (loc,l) in 
-      if all || in_mp v loc then 
-	(l,SEmodule (extract_module env v true mb)) :: ms
+      let ms = extract_msb env v mp all msb in
+      let mp = MPdot (mp,l) in 
+      if all || in_mp v mp then 
+	(l,SEmodule (extract_module env v mp true mb)) :: ms
       else ms
   | (l,SEBmodtype mtb) :: msb ->
-      let ms = extract_msb env v all loc msb in
-      let kn = make_kn loc empty_dirpath l in
+      let ms = extract_msb env v mp all msb in
+      let kn = make_kn mp empty_dirpath l in
       if all || in_kn v kn then 
-	(l,SEmodtype (extract_mtb env v mtb)) :: ms
+	(l,SEmodtype (extract_mtb env v None mtb)) :: ms
       else ms
 
-and extract_meb env v all = function 
-  | MEBident mp -> MEident mp 
+and extract_meb env v mpo all = function 
+  | MEBident mp -> visit_mp v mp; MEident mp 
   | MEBapply (meb, meb',_) -> 
-      MEapply (extract_meb env v true meb, extract_meb env v true meb')
+      MEapply (extract_meb env v None true meb, 
+	       extract_meb env v None true meb')
   | MEBfunctor (mbid, mtb, meb) -> 
-      let env' = add_functor mbid mtb env in 
-      MEfunctor (mbid, extract_mtb env v mtb, extract_meb env' v true meb)
+      let mp = MPbound mbid in 
+      let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in 
+      MEfunctor (mbid, extract_mtb env v None mtb, 
+		 extract_meb env' v None true meb)
   | MEBstruct (msid, msb) -> 
-      let loc = MPself msid in 
-      let env' = add_structure loc msb env in 
-      MEstruct (msid, extract_msb env' v all loc msb) 
-
-and extract_module env v all mb = 
-  { ml_mod_expr = option_app (extract_meb env v all) mb.mod_expr;  
-    ml_mod_type = (match mb.mod_user_type with 
-		     | None -> extract_mtb env v mb.mod_type
-		     | Some mtb -> extract_mtb env v mtb);
-    ml_mod_equiv = mb.mod_equiv }
-	
-and extract_mtb env v = function 
-  | MTBident kn -> MTident kn 
-  | MTBfunsig (mbid, mtb, mtb') -> 
-      let env' = add_functor mbid mtb env in
-      MTfunsig (mbid, extract_mtb env v mtb, extract_mtb env' v mtb') 
-  | MTBsig (msid, msig) -> 
-      let loc = MPself msid in 
-      let env' = Modops.add_signature loc msig env in  
-      MTsig (msid, extract_msig env' v loc msig) 
-
-and extract_msig env v loc = function 
-  | [] -> [] 
-  | (l,SPBconst cb) :: msig -> 
-      let kn = make_kn loc empty_dirpath l in 
-      let s = extract_constant_spec env kn cb in 
-      if logical_spec s then extract_msig env v loc msig
-      else begin
-	get_spec_references v s; 
-	(l,Spec s) :: (extract_msig env v loc msig)
-      end
-  | (l,SPBmind cb) :: msig -> 
-      let kn = make_kn loc empty_dirpath l in 
-      let s = Sind (kn, extract_inductive env kn) in 
-      if logical_spec s then extract_msig env v loc msig
-      else begin 
-	get_spec_references v s; 
-	(l,Spec s) :: (extract_msig env v loc msig)
-      end
-  | (l,SPBmodule {msb_modtype=mtb}) :: msig -> 
-      (l,Smodule (extract_mtb env v mtb)) :: (extract_msig env v loc msig)
-  | (l,SPBmodtype mtb) :: msig -> 
-      (l,Smodtype (extract_mtb env v mtb)) :: (extract_msig env v loc msig)
-
-(* 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
+      let mp,msb = match mpo with 
+	| None -> MPself msid, msb 
+	| Some mp -> mp, subst_msb (map_msid msid mp) msb
+      in 
+      let env' = add_structure mp msb env in 
+      MEstruct (msid, extract_msb env' v mp all msb) 
+
+and extract_module env v mp all mb = 
+  (* [mb.mod_expr <> None ], since we look at modules from outside. *)
+  (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
+  let meb = out_some mb.mod_expr in
+  let mtb = match mb.mod_user_type with None -> mb.mod_type | Some mt -> mt in
+  (* Because of the "with" construct, the module type can be [MTBsig] with *)
+  (* a msid different from the one of the module. Here is the patch. *)
+  let mtb = replicate_msid meb mtb in
+  { ml_mod_expr = extract_meb env v (Some mp) all meb;
+    ml_mod_type = extract_mtb env v None mtb }
 
 (*s Extraction in the Coq toplevel. We display the extracted term in
     Ocaml syntax and we use the Coq printers for globals. The
@@ -284,14 +219,13 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
 
 let mono_environment refs = 
   let l = environment_until None in 
-  init_aliases 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 
   let env = Global.env () in 
-  List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v false m)) 
+  List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) false m)) 
     (List.rev l)
 
 let extraction qid = 
@@ -306,7 +240,7 @@ let extraction qid =
     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;
+    print_one_decl struc (modpath kn) d;
     reset_tables ()
   end
 
@@ -345,8 +279,39 @@ let extraction_file f vl =
   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]. *) 
+(*s Extraction of a module at the toplevel. *)
+
+let extraction_module m = 
+  if is_something_opened () then error_section (); 
+  match lang () with 
+    | Toplevel -> error_toplevel ()
+    | Scheme -> error_scheme ()
+    | _ -> 
+	let q = snd (qualid_of_reference m) in 
+	let mp = 
+	  try Nametab.locate_module q
+	  with Not_found -> error_unknown_module q
+	in 
+	let b = is_modfile mp in 
+	let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in
+	let l = environment_until None in 
+	let v = { kn = KNset.empty ; mp = prefixes_mp mp } in
+	let env = Global.env () in 
+	let struc = 
+	  List.rev_map
+	    (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) b m)) 
+	    (List.rev l)
+	in 
+	let struc = optimize_struct prm None struc in 
+	let struc = 
+	  let bmp = base_mp mp in 
+	  try [bmp, List.assoc bmp struc] with Not_found -> assert false
+	in
+	print_structure_to_file None prm struc; 
+	reset_tables ()
+
+(*s Extraction of a library. The vernacular command is 
+  \verb!Extraction Library! [M]. *) 
 
 let module_file_name m = match lang () with 
   | Ocaml -> let f = String.uncapitalize (string_of_id m) in  f^".ml", f^".mli"
@@ -354,26 +319,27 @@ let module_file_name m = match lang () with
   | _ -> assert false
 
 let dir_module_of_id m = 
-  try Nametab.full_name_module (make_short_qualid m) 
-  with Not_found -> error_unknown_module m
+  let q = make_short_qualid m in 
+  try Nametab.full_name_module q with Not_found -> error_unknown_module q
 
-let extraction_module m =
+let extraction_library m =
   if is_something_opened () then error_section (); 
-   match lang () with 
+  match lang () with 
     | Toplevel -> error_toplevel ()
     | Scheme -> error_scheme ()
     | _ -> 
 	let dir_m = dir_module_of_id m in 
 	let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in 
 	let l = environment_until (Some dir_m) in 
-	init_aliases l;
-(* TEMPORARY: make Extraction Module look like Recursive Extraction Module *)
+(* TEMPORARY: make Extraction Library look like Recursive Extraction Library *)
 	let struc = 
 	  let env = Global.env () in
 	  let select l (mp,meb) = 
-	    if in_mp v mp then (mp, unpack (extract_meb env v true meb)) :: l 
+	    if in_mp v mp (* mp est long -> in_mp peut etre sans long_mp *)
+	    then (mp, unpack (extract_meb env v (Some mp) true meb)) :: l 
 	    else l
-	  in List.fold_left select [] (List.rev l)
+	  in 
+	  List.fold_left select [] (List.rev l)
 	in 
 	let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
 	let struc = optimize_struct dummy_prm None struc in 
@@ -390,10 +356,10 @@ let extraction_module m =
 	in print struc; 
 	reset_tables ()
 	  
-(*s Recursive Extraction of all the modules [M] depends on. 
-  The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
+(*s Recursive Extraction of all the libraries [M] depends on. 
+  The vernacular command is \verb!Recursive Extraction Library! [M]. *) 
 
-let recursive_extraction_module m =
+let recursive_extraction_library m =
   if is_something_opened () then error_section (); 
   match lang () with 
     | Toplevel -> error_toplevel ()
@@ -402,12 +368,14 @@ let recursive_extraction_module m =
 	let dir_m = dir_module_of_id m in 
 	let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in 
 	let l = environment_until (Some dir_m) in 
-	init_aliases l; 
 	let struc = 
 	  let env = Global.env () in
 	  let select l (mp,meb) = 
-	    if in_mp v mp then (mp, unpack (extract_meb env v true meb)) :: l else l
-	  in List.fold_left select [] (List.rev l)
+	    if in_mp v mp (* mp est long -> in_mp peut etre sans long_mp *)
+	    then (mp, unpack (extract_meb env v (Some mp) 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 struc = optimize_struct dummy_prm None struc in 
diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli
index 625afc7d1..bdce5706e 100644
--- a/contrib/extraction/extract_env.mli
+++ b/contrib/extraction/extract_env.mli
@@ -16,5 +16,6 @@ open Libnames
 val extraction : reference -> unit
 val extraction_rec : reference list -> unit
 val extraction_file : string -> reference list -> unit
-val extraction_module : identifier -> unit
-val recursive_extraction_module : identifier -> unit
+val extraction_module : reference -> unit
+val extraction_library : identifier -> unit
+val recursive_extraction_library : identifier -> unit
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 05ad8f48f..824a48568 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -95,7 +95,7 @@ let rec type_scheme_nb_args env c =
 	if is_info_scheme env t then n+1 else n
     | _ -> 0
 
-let _ = ugly_hack_arity_nb_args := type_scheme_nb_args
+let _ = register_type_scheme_nb_args type_scheme_nb_args
 
 (*s [type_sign_vl] does the same, plus a type var list. *)
 
@@ -201,7 +201,6 @@ let rec extract_type env db j c args =
 	       else let n' = List.nth db (n-1) in 
 	       if n' = 0 then Tunknown else Tvar n')
     | Const kn -> 
-	let kn = long_kn kn in 
 	let r = ConstRef kn in 
 	let cb = lookup_constant kn env in 
 	let typ = cb.const_type in 
@@ -228,7 +227,6 @@ let rec extract_type env db j c args =
 		      let newc = applist (Declarations.force lbody, args) in 
 		      extract_type env db j newc []))
     | Ind ((kn,i) as ip) ->
-	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
@@ -284,9 +282,9 @@ and extract_type_scheme env db c p =
 
 and extract_ind env kn = (* kn is supposed to be in long form *)
   try 
-    if (!internal_call = Some kn) || (is_modfile (base_mp (modpath kn))) 
-    then lookup_ind kn
-    else raise Not_found 
+    if (!internal_call = Some kn) then lookup_ind kn (* Already started. *)
+    else if visible_kn kn then lookup_ind kn (* Standard situation. *)
+    else raise Not_found (* Never trust the table for a internal kn. *)
   with Not_found -> 
     internal_call := Some kn;
     let mib = Environ.lookup_mind kn env in 
@@ -384,13 +382,11 @@ and extract_type_cons env db dbmap c i =
 
 and mlt_env env r = match r with 
   | ConstRef kn -> 
-      let kn = long_kn kn in
       (try 
-	 if is_modfile (base_mp (modpath kn)) then
-	   match lookup_term kn with 
-	     | Dtype (_,vl,mlt) -> Some mlt
-	     | _ -> None
-	 else raise Not_found
+	 if not (visible_kn kn) then raise Not_found; 
+	 match lookup_term kn with 
+	   | Dtype (_,vl,mlt) -> Some mlt
+	   | _ -> None
        with Not_found -> 
 	 let cb = Environ.lookup_constant kn env in
 	 let typ = cb.const_type in
@@ -415,10 +411,9 @@ let type_expunge env = type_expunge (mlt_env env)
 (*s Extraction of the type of a constant. *)
 
 let record_constant_type env kn opt_typ = 
-  let kn = long_kn kn in 
   try 
-    if is_modfile (base_mp (modpath kn)) then lookup_type kn
-    else raise Not_found 
+    if not (visible_kn kn) then raise Not_found; 
+    lookup_type kn 
   with Not_found ->
     let typ = match opt_typ with 
       | None -> constant_type env kn 
@@ -470,16 +465,15 @@ 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 (long_kn kn) args
-    | Construct ((kn,i),j) ->
-	extract_cons_app env mle mlt (((long_kn kn),i),j) args
+	extract_cst_app env mle mlt kn args
+    | Construct cp ->
+	extract_cons_app env mle mlt cp 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=(kn,i)},_,c0,br) ->
-	let ip = long_kn kn, i in 
+    | Case ({ci_ind=ip},_,c0,br) ->
  	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 
@@ -743,17 +737,16 @@ let extract_fixpoint env vkn (fi,ti,ci) =
   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 is_custom (long_r r) then Dtype (r, [], Tunknown) 
+	       if is_custom r then Dtype (r, [], Tunknown) 
 	       else error_axiom r
            | (Info,Default) -> 
-	       if is_custom (long_r r) then 
+	       if is_custom 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
@@ -773,7 +766,6 @@ let extract_constant env kn cb =
 	       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 
@@ -792,7 +784,6 @@ let extract_constant_spec env kn cb =
 	Sval (r, type_expunge env t)
 
 let extract_inductive env kn = 
-  let kn = long_kn kn in 
   let ind = extract_ind env kn in 
   add_recursors env kn; 
   let f l = List.filter (type_neq env Tdummy) l in 
@@ -805,9 +796,8 @@ let extract_inductive env kn =
 
 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)
+  | IndRef (kn,_) -> Dind (kn, extract_inductive env kn)
+  | ConstructRef ((kn,_),_) -> Dind (kn, extract_inductive env kn)
   | VarRef kn -> assert false
 
 (*s Without doing complete extraction, just guess what a constant would be. *) 
@@ -820,6 +810,23 @@ let constant_kind env cb =
     | (Info,TypeScheme) -> Type
     | (Info,Default) -> Term
 
+(*s Is a [ml_decl] logical ? *) 
+
+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
+
+(*s Is a [ml_spec] logical ? *)
+
+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
 
   
 
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index c9654d25c..882fa74b4 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -35,3 +35,8 @@ val extract_declaration : env -> global_reference -> ml_decl
 type kind = Logical | Term | Type 
 
 val constant_kind : env -> constant_body -> kind
+
+(*s Is a [ml_decl] or a [ml_spec] logical ? *) 
+
+val logical_decl : ml_decl -> bool
+val logical_spec : ml_spec -> bool
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index ae79dda81..80496af52 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -42,15 +42,21 @@ VERNAC COMMAND EXTEND Extraction
   -> [ extraction_file f l ]
 END
 
-(* Modular extraction (one Coq module = one ML module) *)
+(* Extraction of a Coq module in the Coq toplevel *)
 VERNAC COMMAND EXTEND ExtractionModule
-| [ "Extraction" "Module" ident(m) ]
-  -> [ extraction_module m ]
+| [ "Extraction" "Module" global(m) ] 
+  -> [ extraction_module m ]   
 END
 
-VERNAC COMMAND EXTEND RecursiveExtractionModule
-| [ "Recursive" "Extraction" "Module" ident(m) ]
-  -> [ recursive_extraction_module m ]
+(* Modular extraction (one Coq library = one ML module) *)
+VERNAC COMMAND EXTEND ExtractionLibrary
+| [ "Extraction" "Library" ident(m) ]
+  -> [ extraction_library m ]
+END
+
+VERNAC COMMAND EXTEND RecursiveExtractionLibrary
+| [ "Recursive" "Extraction" "Library" ident(m) ]
+  -> [ recursive_extraction_library m ]
 END
 
 (* Target Language *)
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 7092efad5..15101037b 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -59,9 +59,9 @@ let pr_lower_id id = pr_id (lowercase_id id)
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let local_mp = ref initial_path 
+let local_mpl = ref ([] : module_path list)
 
-let pp_global r = P.pp_global !local_mp r
+let pp_global r = P.pp_global !local_mpl r
 let empty_env () = [], P.globals()
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
@@ -237,8 +237,8 @@ let rec pp_ind first kn i ind =
 
 (*s Pretty-printing of a declaration. *)
 
-let pp_decl mp = 
-  local_mp := mp;
+let pp_decl mpl = 
+  local_mpl := mpl;
   function
   | Dind (kn,i) when i.ind_info = Singleton -> 
       pp_singleton kn i.ind_packets.(0) ++ fnl ()
@@ -262,15 +262,15 @@ let pp_decl mp =
       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
+let pp_structure_elem mpl = function 
+  | (l,SEdecl d) -> pp_decl mpl 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)
+  prlist (fun (mp,sel) -> prlist (pp_structure_elem [mp]) sel)
 
 let pp_signature s = failwith "TODO"
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 3b255a440..4a92f4833 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -104,30 +104,32 @@ type ml_specif =
   | Smodule of ml_module_type
   | Smodtype of ml_module_type
 
-and ml_module_sig = (label * ml_specif) list
-
 and ml_module_type = 
   | MTident of kernel_name
   | MTfunsig of mod_bound_id * ml_module_type * ml_module_type
   | MTsig of mod_self_id * ml_module_sig
 
+and ml_module_sig = (label * ml_specif) list
+
+type ml_structure_elem = 
+  | SEdecl of ml_decl
+  | SEmodule of ml_module
+  | SEmodtype of ml_module_type
+
 and ml_module_expr =
   | MEident of module_path
   | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr 
   | MEstruct of mod_self_id * ml_module_structure
   | MEapply of ml_module_expr * ml_module_expr
 
-and ml_structure_elem = 
-  | SEdecl of ml_decl
-  | SEmodule of ml_module (* pourquoi pas plutot ml_module_expr *)
-  | SEmodtype of ml_module_type
-
 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_equiv : module_path option } 
+    { ml_mod_expr : ml_module_expr; 
+      ml_mod_type : ml_module_type }
+
+(* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp] 
+   implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *)
 
 type ml_structure = (module_path * ml_module_structure) list
 
@@ -140,13 +142,13 @@ type ml_signature = (module_path * ml_module_sig) list
 
 module type Mlpp_param = sig
   val globals : unit -> Idset.t
-  val pp_global : module_path -> global_reference -> std_ppcmds
-  val pp_long_module : module_path -> module_path -> std_ppcmds
+  val pp_global : module_path list -> global_reference -> std_ppcmds
+  val pp_long_module : module_path list -> module_path -> std_ppcmds
   val pp_short_module : identifier -> std_ppcmds
 end
 
 module type Mlpp = sig
-  val pp_decl : module_path -> ml_decl -> std_ppcmds
+  val pp_decl : module_path list -> ml_decl -> std_ppcmds
   val pp_struct : ml_structure -> std_ppcmds
   val pp_signature : ml_signature -> std_ppcmds
 end
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index ba0659b32..e2316ecd3 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -208,12 +208,6 @@ end
 
 (*s Does a section path occur in a ML type ? *)
 
-let kn_of_r r = match r with 
-    | ConstRef kn -> kn
-    | IndRef (kn,_) -> kn
-    | ConstructRef ((kn,_),_) -> kn
-    | VarRef _ -> assert false
-
 let rec type_mem_kn kn = function 
   | Tmeta _ -> assert false
   | Tglob (r,l) -> (kn_of_r r) = kn || List.exists (type_mem_kn kn) l
@@ -808,7 +802,7 @@ let case_expunge s e =
   let m = List.length s in 
   let n = nb_lams e in 
   let p = if m <= n then collect_n_lams m e 
-  else eta_expansion_sign (snd (list_chop n s)) (collect_lams e) in 
+  else eta_expansion_sign (list_skipn n s) (collect_lams e) in 
   kill_some_lams (List.rev s) p
 
 (*s [term_expunge] takes a function [fun idn ... id1 -> c] 
@@ -1064,199 +1058,3 @@ let inline r t =
      || (auto_inline () && lang () <> Haskell && not (is_projection r)
          && (is_recursor r || manual_inline r || inline_test t)))
 
-(*S Optimization. *)
-
-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 :: (optim prm s l) else optim prm s l
-  | Dterm (r,t,typ) :: l ->
-      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
-
-(*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
-
-let type_iter_references do_type t = 
-  let rec iter = function 
-    | Tglob (r,l) -> do_type r; List.iter iter l 
-    | Tarr (a,b) -> iter a; iter b 
-    | _ -> () 
-  in iter t
-
-let ast_iter_references do_term do_cons do_type a = 
-  let rec iter a = 
-    ast_iter iter a;
-    match a with 
-      | MLglob r -> do_term r
-      | MLcons (r,_) -> do_cons r
-      | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> do_cons r) v
-      | 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
-  function 
-    | 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
-
-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 13f37b32b..489df1a66 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -50,8 +50,6 @@ end
 
 (*s Utility functions over ML types without meta *)
 
-val kn_of_r : global_reference -> kernel_name
-
 val type_mem_kn : kernel_name -> ml_type -> bool
 
 val type_maxvar : ml_type -> int
@@ -94,30 +92,17 @@ val eta_args_sign : int -> bool list -> ml_ast list
 
 (*s Utility functions over ML terms. *)
 
+val ast_map : (ml_ast -> ml_ast) -> ml_ast -> ml_ast
+val ast_map_lift : (int -> ml_ast -> ml_ast) -> int -> ml_ast -> ml_ast
 val ast_iter : (ml_ast -> unit) -> ml_ast -> unit
 val ast_occurs : int -> ml_ast -> bool
 val ast_occurs_itvl : int -> int -> ml_ast -> bool
 val ast_lift : int -> ml_ast -> ml_ast
 val ast_pop : ml_ast -> ml_ast
+val ast_subst : ml_ast -> ml_ast -> ml_ast
 
-(*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_struct : 
-  extraction_params -> ml_decl list option -> ml_structure -> ml_structure
-
-(* Misc. *)
-
-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 normalize : ml_ast -> ml_ast 
+val optimize_fix : ml_ast -> ml_ast
+val inline : global_reference -> ml_ast -> bool
 
-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/modutil.ml b/contrib/extraction/modutil.ml
new file mode 100644
index 000000000..343861ee4
--- /dev/null
+++ b/contrib/extraction/modutil.ml
@@ -0,0 +1,416 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Names
+open Declarations
+open Environ
+open Libnames
+open Util
+open Miniml
+open Table
+open Mlutil
+
+(*S Functions upon modules missing in [Modops]. *) 
+
+(*s 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 = 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 
+      | SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env 
+      | SEBmodtype mtb -> Environ.add_modtype kn mtb env  
+  in List.fold_left add_one env msb
+
+(*s Apply a module path substitution on a module.
+   Build on the [Modops.subst_modtype] model. *)
+
+let rec subst_module sub mb =
+  let mtb' = Modops.subst_modtype sub mb.mod_type
+  and meb' = option_smartmap (subst_meb sub) mb.mod_expr
+  and mtb'' = option_smartmap (Modops.subst_modtype sub) mb.mod_user_type
+  and mpo' = option_smartmap (subst_mp sub) mb.mod_equiv in
+  if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) && 
+    (mtb''==mb.mod_user_type) && (mpo'==mb.mod_equiv)
+  then mb
+  else { mod_expr= meb'; 
+	 mod_type=mtb'; 
+	 mod_user_type=mtb''; 
+	 mod_equiv=mpo'; 
+	 mod_constraints=mb.mod_constraints }
+
+and subst_meb sub = function 
+  | MEBident mp -> MEBident (subst_mp sub mp) 
+  | MEBfunctor (mbid, mtb, meb) -> 
+      assert (not (occur_mbid mbid sub)); 
+      MEBfunctor (mbid, Modops.subst_modtype sub mtb, subst_meb sub meb)
+  | MEBstruct (msid, msb) -> 
+      assert (not (occur_msid msid sub));
+      MEBstruct (msid, subst_msb sub msb)
+  | MEBapply (meb, meb', c) -> 
+      MEBapply (subst_meb sub meb, subst_meb sub meb', c)
+
+and subst_msb sub msb = 
+  let subst_body = function
+    | SEBconst cb -> SEBconst (subst_const_body sub cb)
+    | SEBmind mib -> SEBmind (subst_mind sub mib)
+    | SEBmodule mb -> SEBmodule (subst_module sub mb)
+    | SEBmodtype mtb -> SEBmodtype (Modops.subst_modtype sub mtb)
+  in List.map (fun (l,b) -> (l,subst_body b)) msb
+
+(*s Change a msid in a module type, to follow a module expr. 
+  Because of the "with" construct, the module type of a module can be a 
+  [MTBsig] with a msid different from the one of the module. *)
+
+let rec replicate_msid meb mtb = match meb,mtb with 
+  | MEBfunctor (_, _, meb), MTBfunsig (mbid, mtb1, mtb2) -> 
+      let mtb' = replicate_msid meb mtb2 in 
+      if mtb' == mtb2 then mtb else MTBfunsig (mbid, mtb1, mtb')
+  | MEBstruct (msid, _), MTBsig (msid1, msig) when msid <> msid1 -> 
+      let msig' = Modops.subst_signature_msid msid1 (MPself msid) msig in
+      if msig' == msig then MTBsig (msid, msig) else MTBsig (msid, msig')
+  | _ -> mtb
+
+
+(*S More functions concerning [module_path]. *)
+
+let rec prefixes_mp mp = match mp with 
+  | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
+  | _ -> MPset.singleton mp 
+
+let rec common_prefix prefixes_mp1 mp2 = 
+  if MPset.mem mp2 prefixes_mp1 then mp2 
+  else match mp2 with 
+    | MPdot (mp,_) -> common_prefix prefixes_mp1 mp 
+    | _ -> raise Not_found
+
+let common_prefix_from_list mp0 mpl = 
+  let prefixes_mp0 = prefixes_mp mp0 in 
+  let rec f = function 
+    | [] -> raise Not_found
+    | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l
+  in f mpl
+
+let rec modfile_of_mp mp = match mp with 
+  | MPfile _ -> mp
+  | MPdot (mp,_) -> modfile_of_mp mp 
+  | _ -> raise Not_found
+
+let rec 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
+
+let labels_after_prefix mp0 mp = 
+  let n0 = List.length (snd (labels_of_mp mp0)) 
+  and l = snd (labels_of_mp mp)
+  in 
+  assert (n0 <= List.length l);
+  list_skipn n0 l
+
+let rec add_labels_mp mp = function 
+  | [] -> mp 
+  | l :: ll -> add_labels_mp (MPdot (mp,l)) ll
+
+
+(*S Functions upon ML modules. *)
+
+(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a 
+   [ml_structure]. *) 
+
+let struct_iter do_decl do_spec s = 
+  let rec 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
+  let rec se_iter = function 
+    | (_,SEdecl d) -> do_decl d
+    | (_,SEmodule m) -> 
+	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
+  in 
+  List.iter (function (_,sel) -> List.iter se_iter sel) s
+
+(*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
+
+let type_iter_references do_type t = 
+  let rec iter = function 
+    | Tglob (r,l) -> do_type r; List.iter iter l 
+    | Tarr (a,b) -> iter a; iter b 
+    | _ -> () 
+  in iter t
+
+let ast_iter_references do_term do_cons do_type a = 
+  let rec iter a = 
+    ast_iter iter a;
+    match a with 
+      | MLglob r -> do_term r
+      | MLcons (r,_) -> do_cons r
+      | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> do_cons r) v
+      | 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
+  function 
+    | 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
+
+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 Get all references used in one [ml_structure], either in [list] or [set]. *)
+
+type 'a updown = { mutable up : 'a ; mutable down : 'a }
+
+let struct_get_references empty add struc = 
+  let o = { up = empty ; down = empty } in 
+  let do_term r = o.down <- add r o.down in
+  let do_cons r = o.up <- add r o.up in 
+  let do_type = if lang () = Haskell then do_cons else do_term in 
+  struct_iter_references do_term do_cons do_type struc; o
+
+let struct_get_references_set = struct_get_references Refset.empty Refset.add
+
+module Orefset = struct 
+  type t = { set : Refset.t ; list : global_reference list }
+  let empty = { set = Refset.empty ; list = [] }
+  let add r o = 
+    if Refset.mem r o.set then o 
+    else { set = Refset.add r o.set ; list = r :: o.list }
+  let set o = o.set
+  let list o = o.list
+end
+
+let struct_get_references_list struc = 
+  let o = struct_get_references Orefset.empty Orefset.add struc in 
+  { up = Orefset.list o.up; down = Orefset.list o.down }
+
+
+(*s Searching occurrences of a particular term (no lifting done). *)
+
+exception Found
+
+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 
+
+
+(*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *)
+
+let get_decl_in_structure r struc = 
+  try 
+    let kn = kn_of_r r in 
+    let base_mp,ll = labels_of_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 
+		  | MEstruct (_,sel) -> go ll sel 
+		  | _ -> error_not_visible r 
+    in go ll sel
+  with Not_found -> assert false
+
+
+(*s Optimization of a [ml_structure]. *)
+
+(* 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. *)
+
+let rec subst_glob_ast s t = match t with 
+  | MLglob (ConstRef kn) -> (try KNmap.find kn s with Not_found -> t)
+  | _ -> ast_map (subst_glob_ast s) t
+
+let dfix_to_mlfix rv av i = 
+  let rec make_subst n s = 
+    if n < 0 then s 
+    else make_subst (n-1) (KNmap.add (kn_of_r rv.(n)) (n+1) s)
+  in 
+  let s = make_subst (Array.length rv - 1) KNmap.empty 
+  in 
+  let rec subst n t = match t with 
+    | MLglob (ConstRef kn) -> 
+	(try MLrel (n + (KNmap.find kn s)) with Not_found -> t)
+    | _ -> ast_map_lift subst n t 
+  in 
+  let ids = Array.map (fun r -> id_of_label (label (kn_of_r r))) rv in 
+  let c = Array.map (subst 0) av 
+  in MLfix(i, ids, c)
+
+let rec optim prm s = function
+  | [] -> []
+  | (Dtype (r,_,Tdummy) | Dterm(r,MLdummy,_)) as d :: l ->
+      if List.mem r prm.to_appear then d :: (optim prm s l) else optim prm s l
+  | Dterm (r,t,typ) :: l ->
+      let t = normalize (subst_glob_ast !s t) in 
+      let i = inline r t in 
+      if i then s := KNmap.add (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 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 
+      let all = ref true in 
+      for i = 0 to Array.length rv - 1 do 
+	if inline rv.(i) av.(i)
+	then s := KNmap.add (kn_of_r rv.(i)) (dfix_to_mlfix rv av i) !s
+	else all := false
+      done; 
+      if !all && top && not prm.modular 
+	&& (array_for_all (fun r -> not (List.mem r prm.to_appear)) rv)  
+      then optim_se top prm s lse
+      else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top prm s lse)
+  | (l,SEmodule m) :: lse -> 
+      let m = { m with ml_mod_expr = optim_me prm s m.ml_mod_expr}
+      in (l,SEmodule m) :: (optim_se top prm s lse)
+  | se :: lse -> se :: (optim_se top prm s lse) 
+
+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
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
new file mode 100644
index 000000000..41a041d9a
--- /dev/null
+++ b/contrib/extraction/modutil.mli
@@ -0,0 +1,72 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ i*)
+
+open Names
+open Declarations
+open Environ
+open Libnames
+open Miniml
+
+(*s Functions upon modules missing in [Modops]. *) 
+
+(* Add _all_ direct subobjects of a module, not only those exported. 
+   Build on the [Modops.add_signature] model. *)
+
+val add_structure : module_path -> module_structure_body -> env -> env 
+
+(* Apply a module path substitution on a module.
+   Build on the [Modops.subst_modtype] model. *)
+
+val subst_module : substitution -> module_body -> module_body 
+val subst_meb : substitution -> module_expr_body -> module_expr_body
+val subst_msb : substitution -> module_structure_body -> module_structure_body
+
+(* Change a msid in a module type, to follow a module expr. *)
+
+val replicate_msid : module_expr_body -> module_type_body -> module_type_body
+
+(*s More utilities concerning [module_path]. *)
+
+val modfile_of_mp : module_path -> module_path
+val fst_level_module_of_mp : module_path -> module_path * label
+val prefixes_mp : module_path -> MPset.t
+val common_prefix_from_list : module_path -> module_path list -> module_path
+val labels_after_prefix : module_path -> module_path -> label list 
+val labels_of_mp : module_path -> module_path * label list
+val add_labels_mp : module_path -> label list -> module_path
+
+(*s Functions upon ML modules. *)
+
+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 decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit
+val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit
+val struct_iter_references : do_ref -> do_ref -> do_ref -> ml_structure -> unit
+
+type 'a updown = { mutable up : 'a ; mutable down : 'a }
+
+val struct_get_references_set : ml_structure -> Refset.t updown
+val struct_get_references_list : ml_structure -> global_reference list updown
+
+val signature_of_structure : ml_structure -> ml_signature
+
+val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
+
+(* 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_struct : 
+  extraction_params -> ml_decl list option -> ml_structure -> ml_structure
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 5fb08d091..6d718f9b6 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -18,6 +18,7 @@ open Libnames
 open Table
 open Miniml
 open Mlutil
+open Modutil
 
 let cons_cofix = ref Refset.empty
 
@@ -156,12 +157,11 @@ let preamble_sig _ used_modules (_,tdummy,tunknown) =
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let local_mp = ref initial_path
+let local_mpl = ref ([] : module_path list)
 
 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
+  else P.pp_global !local_mpl  r
 
 let empty_env () = [], P.globals ()
 
@@ -224,13 +224,13 @@ let rec pp_expr par env args =
 	      spc () ++ hov 0 pp_a2))
     | MLglob r -> 
 	(try 
-	   let _,args = list_chop (projection_arity r) args in 
+	   let args = list_skipn (projection_arity r) args in 
 	   let record = List.hd args in 
 	   pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
 	 with _ -> apply (pp_global r))
     | MLcons (r,[]) ->
 	assert (args=[]);
-	if Refset.mem (long_r r) !cons_cofix then 
+	if Refset.mem r !cons_cofix then 
 	  pp_par par (str "lazy " ++ pp_global r)
 	else pp_global r
     | MLcons (r,args') -> 
@@ -240,12 +240,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 (long_r r) !cons_cofix then 
+	   if Refset.mem 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 (long_r r) !cons_cofix then 
+	let expr = if Refset.mem r !cons_cofix then 
 	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
 	else 
 	  (pp_expr false env [] t) 
@@ -335,7 +335,7 @@ and pp_function env f t =
     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 (long_r r) !cons_cofix) 
+    let (r,_,_) = pv.(0) in not (Refset.mem r !cons_cofix) 
   in					  
   match t' with 
     | MLcase(MLrel 1,pv) when is_not_cofix pv ->
@@ -375,14 +375,13 @@ let pp_val e typ =
 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
+    if is_inline_custom rv.(i) then pp_Dfix init (i+1) fix
     else 
-      let e = pp_global r in
+      let e = pp_global rv.(i) in
       (if init then mt () else fnl2 ()) ++
       pp_val e t.(i) ++
       str (if init then "let rec " else "and ") ++
-      (if is_custom r then e ++ str " = " ++ str (find_custom r)
+      (if is_custom rv.(i) then e ++ str " = " ++ str (find_custom rv.(i))
        else pp_function (empty_env ()) e c.(i)) ++
       pp_Dfix false (i+1) fix 
 	
@@ -419,13 +418,12 @@ let pp_logical_ind packet =
 let pp_singleton kn packet = 
   let l = rename_tvars keywords packet.ip_vars in 
   hov 2 (str "type " ++ pp_parameters l ++
-	 P.pp_global !local_mp (IndRef (kn,0)) ++ str " =" ++ spc () ++
+	 pp_global (IndRef (kn,0)) ++ str " =" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
 	 pp_comment (str "singleton inductive, whose constructor was " ++ 
 		     pr_id packet.ip_consnames.(0)))
 
 let pp_record kn 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 
@@ -469,19 +467,18 @@ let pp_ind co kn ind =
 (*s Pretty-printing of a declaration. *)
 
 let pp_mind kn i = 
-  let kn = long_kn kn in 
-  (match i.ind_info with 
-     | Singleton -> pp_singleton kn i.ind_packets.(0)
-     | 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)); 
-	 pp_ind true kn i
-     | Record -> pp_record kn i.ind_packets.(0)
-     | _ -> pp_ind false kn i)
-
-let pp_decl mp = 
-  local_mp := mp; 
+  match i.ind_info with 
+    | Singleton -> pp_singleton 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 (Dind (kn,i)); 
+	pp_ind true kn i
+    | Record -> pp_record kn i.ind_packets.(0)
+    | _ -> pp_ind false kn i
+
+let pp_decl mpl = 
+  local_mpl := mpl; 
   function
     | Dind (kn,i) as d -> pp_mind kn i
     | Dtype (r, l, t) ->
@@ -512,8 +509,8 @@ let pp_decl mp =
     | Dfix (rv,defs,typs) ->
 	pp_Dfix true 0 (rv,defs,typs)
 
-let pp_spec mp = 
-  local_mp := mp; 
+let pp_spec mpl = 
+  local_mpl := mpl; 
   function 
     | Sind (kn,i) -> pp_mind kn i
     | Sval (r,t) -> 
@@ -537,82 +534,87 @@ let pp_spec mp =
 	  in 
 	  hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ spc () ++ def)
 
-let rec pp_structure_elem mp = function 
-  | (_,SEdecl d) -> pp_decl mp d
+let rec pp_specif mpl = function 
+  | (_,Spec s) -> pp_spec mpl s 
+  | (l,Smodule mt) -> 
+      hov 1 
+	(str "module " ++ 
+	 P.pp_short_module (id_of_label l) ++
+	 str " : " ++ fnl () ++ pp_module_type mpl None (* (Some l) *) mt)
+  | (l,Smodtype mt) -> 
+      hov 1
+	(str "module type " ++
+	 P.pp_short_module (id_of_label l) ++
+	 str " = " ++ fnl () ++ pp_module_type mpl None mt)
+
+and pp_module_type mpl ol = function 
+  | MTident kn -> 
+      let mp,_,l = repr_kn kn in P.pp_long_module mpl (MPdot (mp,l)) 
+  | MTfunsig (mbid, mt, mt') -> 
+      str "functor (" ++ 
+      P.pp_short_module (id_of_mbid mbid) ++
+      str ":" ++
+      pp_module_type mpl None mt ++
+      str ") ->" ++ fnl () ++
+      pp_module_type mpl None mt'
+  | MTsig (msid, sign) ->
+      let mpl = match ol, mpl with 
+	| None, _ -> (MPself msid) :: mpl
+	| Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl
+	| _ -> assert false 
+      in
+      let l = map_succeed (pp_specif mpl) sign in 
+      str "sig " ++ fnl () ++ 
+      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
+      fnl () ++ str "end"
+
+let rec pp_structure_elem mpl = function 
+  | (_,SEdecl d) -> pp_decl mpl d
   | (l,SEmodule m) ->
       hov 1 
 	(str "module " ++ P.pp_short_module (id_of_label l) ++ 
-	 (match m.ml_mod_equiv with 
-	    | None -> 
-		str " :" ++ fnl () ++ 
-		pp_module_type mp m.ml_mod_type ++ fnl () ++
-		str "= " ++ fnl () ++ 
-		(match m.ml_mod_expr with 
-		   | None -> assert false (* see Jacek *)
-		   | Some me -> pp_module_expr mp me)
-	    | Some mp' -> 
-		str " = " ++ P.pp_long_module mp mp'))
+	 str " :" ++ fnl () ++ 
+	 pp_module_type mpl None m.ml_mod_type ++ fnl () ++ 
+	 str "= " ++ fnl () ++ 
+	 pp_module_expr mpl (Some l) m.ml_mod_expr)
   | (l,SEmodtype m) -> 
       hov 1 
 	(str "module type " ++ P.pp_short_module (id_of_label l) ++
-	 str " = " ++ fnl () ++ pp_module_type mp m)
+	 str " = " ++ fnl () ++ pp_module_type mpl None m)
 
-and pp_module_expr mp = function 
-  | MEident mp' -> P.pp_long_module mp mp'
+and pp_module_expr mpl ol = function 
+  | MEident mp' -> P.pp_long_module mpl mp'
   | MEfunctor (mbid, mt, me) -> 
       str "functor (" ++ 
       P.pp_short_module (id_of_mbid mbid) ++
       str ":" ++
-      pp_module_type mp mt ++
+      pp_module_type mpl None mt ++
       str ") ->" ++ fnl () ++
-      pp_module_expr mp me
+      pp_module_expr mpl None me
   | MEapply (me, me') -> 
-      pp_module_expr mp me ++ str "(" ++ pp_module_expr mp me' ++ str ")"
+      pp_module_expr mpl None me ++ str "(" ++ 
+      pp_module_expr mpl None me' ++ str ")"
   | MEstruct (msid, sel) -> 
-      let l = map_succeed (pp_structure_elem (MPself msid)) sel in 
+      let mpl = match ol, mpl with 
+	| None, _ -> (MPself msid) :: mpl
+	| Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl
+	| _ -> assert false
+      in
+      let l = map_succeed (pp_structure_elem mpl) sel in 
       str "struct " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ 
       fnl () ++ str "end" 
 
-and pp_module_type mp = function 
-  | MTident kn -> 
-      let mp',_,l = repr_kn kn in P.pp_long_module mp (MPdot (mp,l)) 
-  | MTfunsig (mbid, mt, mt') -> 
-      str "functor (" ++ 
-      P.pp_short_module (id_of_mbid mbid) ++
-      str ":" ++
-      pp_module_type mp mt ++
-      str ") ->" ++ fnl () ++
-      pp_module_type mp mt'
-  | MTsig (msid, sign) -> 
-      let l = map_succeed (pp_specif (MPself msid)) sign in 
-      str "sig " ++ fnl () ++ 
-      v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
-      fnl () ++ str "end"
-
-and pp_specif mp = function 
-  | (_,Spec s) -> pp_spec mp s 
-  | (l,Smodule mt) -> 
-      hov 1 
-	(str "module " ++ 
-	 P.pp_short_module (id_of_label l) ++
-	 str " : " ++ fnl () ++ pp_module_type mp mt)
-  | (l,Smodtype mt) -> 
-      hov 1
-	(str "module type " ++
-	 P.pp_short_module (id_of_label l) ++
-	 str " = " ++ fnl () ++ pp_module_type mp mt)
-
 let pp_struct s =
-  let pp mp s = pp_structure_elem mp s ++ fnl2 () in 
+  let pp mp s = pp_structure_elem [mp] s ++ fnl2 () in 
   prlist (fun (mp,sel) -> prlist identity (map_succeed (pp mp) sel)) s
 
 let pp_signature s = 
-  let pp mp s = pp_specif mp s ++ fnl2 () in 
+  let pp mp s = pp_specif [mp] s ++ fnl2 () in 
   prlist (fun (mp,sign) -> prlist identity (map_succeed (pp mp) sign)) s
 
-let pp_decl mp d = 
-  try pp_decl mp d with Failure "empty phrase" -> mt () 
+let pp_decl mpl d = 
+  try pp_decl mpl d with Failure "empty phrase" -> mt () 
 
 end
 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index b6d0014ac..a47607fa8 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -47,7 +47,7 @@ let pp_abst st = function
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_global r = P.pp_global initial_path r
+let pp_global r = P.pp_global [initial_path] r
 let empty_env () = [], P.globals()
 
 (*s Pretty-printing of expressions.  *)
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 189bcbbf6..7afc2f9ea 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -20,12 +20,15 @@ open Util
 open Pp
 open Miniml
 
-(*S Utilities concerning [module_path] *)
+(*S Utilities concerning [module_path] and [kernel_names] *)
 
-let current_toplevel () = fst (Lib.current_prefix ())
+let kn_of_r r = match r with 
+    | ConstRef kn -> kn
+    | IndRef (kn,_) -> kn
+    | ConstructRef ((kn,_),_) -> kn
+    | VarRef _ -> assert false
 
-let is_toplevel mp = 
-  mp = initial_path || mp = current_toplevel ()
+let current_toplevel () = fst (Lib.current_prefix ())
 
 let is_something_opened () = 
   try ignore (Lib.what_is_opened ()); true
@@ -35,98 +38,39 @@ 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 is_toplevel mp = 
+  mp = initial_path || mp = current_toplevel ()
 
 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 visible_kn kn = at_toplevel (base_mp (modpath kn))
 
-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 expanding 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*)
-
-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 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 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 
+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 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
+let add_ind kn m = inductives := KNmap.add kn m !inductives
+let lookup_ind kn = KNmap.find kn !inductives
 
 (*s Recursors table. *)
 
@@ -134,7 +78,6 @@ 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 
@@ -146,7 +89,7 @@ let add_recursors env kn =
     mib.mind_packets
 
 let is_recursor = function 
-  | ConstRef kn -> KNset.mem (long_kn kn) !recursors
+  | ConstRef kn -> KNset.mem kn !recursors
   | _ -> false
 
 (*s Record tables. *)
@@ -158,18 +101,18 @@ let projs = ref (Refmap.empty : int Refmap.t)
 let init_projs () = projs := Refmap.empty
 
 let add_record kn n l = 
-  records := KNmap.add (long_kn kn) l !records; 
-  projs := List.fold_right (fun r -> Refmap.add (long_r r) n) l !projs
+  records := KNmap.add kn l !records; 
+  projs := List.fold_right (fun r -> Refmap.add r n) l !projs
 
-let find_projections kn = KNmap.find (long_kn kn) !records
-let is_projection r = Refmap.mem (long_r r) !projs
-let projection_arity r = Refmap.find (long_r r) !projs
+let find_projections kn = KNmap.find kn !records
+let is_projection r = Refmap.mem r !projs
+let projection_arity r = Refmap.find r !projs
 
 (*s Tables synchronization. *)
 
 let reset_tables () = 
   init_terms (); init_types (); init_inductives (); init_recursors (); 
-  init_records (); init_projs (); init_aliases ()
+  init_records (); init_projs ()
 
 (*s Printing. *)
 
@@ -212,12 +155,6 @@ let error_section () =
 let error_constant r = 
   err (Printer.pr_global r ++ str " is not a constant.") 
 
-let error_fixpoint r = 
-  err (str "Fixpoint " ++ Printer.pr_global r ++ str " cannot be inlined.") 
-
-let error_type_scheme r = 
-  err (Printer.pr_global r ++ spc () ++ str "is a type scheme, not a type.")
-
 let error_inductive r = 
   err (Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
 
@@ -229,7 +166,7 @@ let error_module_clash s =
        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.") 
+  err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") 
 
 let error_toplevel () = 
   err (str "Toplevel pseudo-ML language can be used only at Coq toplevel.\n" ++
@@ -308,9 +245,9 @@ let empty_inline_table = (Refset.empty,Refset.empty)
 
 let inline_table = ref empty_inline_table
 
-let to_inline r = Refset.mem (long_r r) (fst !inline_table)
+let to_inline r = Refset.mem r (fst !inline_table)
 
-let to_keep r = Refset.mem (long_r r) (snd !inline_table)
+let to_keep r = Refset.mem r (snd !inline_table)
 
 let add_inline_entries b l = 
   let f b = if b then Refset.add else Refset.remove in 
@@ -319,13 +256,6 @@ let add_inline_entries b l =
      (List.fold_right (f b) l i), 
      (List.fold_right (f (not b)) l k)
 
-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,_) = 
@@ -348,7 +278,6 @@ let extraction_inline b l =
   let refs = List.map Nametab.global l in 
   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))
@@ -382,31 +311,21 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 (*s Extract Constant/Inductive. *)
 
-let ugly_hack_arity_nb_args = ref (fun _ _ -> 0) 
-
-let check_term_or_type r ids = match r with 
-  | ConstRef sp -> 
-      let env = Global.env () in 
-      let typ = Environ.constant_type env sp in 
-      let typ = Reduction.whd_betadeltaiota env typ in
-      if Reduction.is_arity env typ 
-      then 
-	let nargs = !ugly_hack_arity_nb_args env typ in 
-	if List.length ids <> nargs then error_axiom_scheme r nargs
-  | _ -> error_constant r
-	
+(* UGLY HACK: to be defined in [extraction.ml] *)
+let use_type_scheme_nb_args, register_type_scheme_nb_args = 
+  let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r 
+
 let customs = ref Refmap.empty
 
 let add_custom r ids s = customs := Refmap.add r (ids,s) !customs
 
-let is_custom r = Refmap.mem (long_r r) !customs
+let is_custom r = Refmap.mem r !customs
 
-let is_inline_custom r = 
-  let r = long_r r in (is_custom r) && (to_inline r) 
+let is_inline_custom r = (is_custom r) && (to_inline r) 
 
-let find_custom r = snd (Refmap.find (long_r r) !customs)
+let find_custom r = snd (Refmap.find r !customs)
 
-let find_type_custom r = Refmap.find (long_r r) !customs
+let find_type_custom r = Refmap.find r !customs
 
 (* Registration of operations for rollback. *)
 
@@ -428,9 +347,20 @@ let _ = declare_summary "ML extractions"
 let extract_constant_inline inline r ids s =
   if is_something_opened () then error_section (); 
   let g = Nametab.global r in 
-  check_term_or_type g ids;
-  Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
-  Lib.add_anonymous_leaf (in_customs (g,ids,s))
+  match g with 
+    | ConstRef kn -> 
+	let env = Global.env () in 
+	let typ = Environ.constant_type env kn in 
+	let typ = Reduction.whd_betadeltaiota env typ in
+	if Reduction.is_arity env typ 
+	  then begin 
+	    let nargs = use_type_scheme_nb_args env typ in 
+	    if List.length ids <> nargs then error_axiom_scheme g nargs
+	  end; 
+	Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
+	Lib.add_anonymous_leaf (in_customs (g,ids,s))
+    | _ -> error_constant g
+
 
 let extract_inductive r (s,l) =
   if is_something_opened () then error_section (); 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 3fbdbc209..087d7f846 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -21,12 +21,10 @@ 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_unknown_module : qualid -> 'a
 val error_toplevel : unit -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
@@ -34,19 +32,15 @@ val error_unqualified_name : string -> string -> 'a
 
 (*s utilities concerning [module_path]. *)
 
-val current_toplevel : unit -> module_path
+val kn_of_r : global_reference -> kernel_name
 
-val is_toplevel : module_path -> bool 
-val at_toplevel : module_path -> bool
+val current_toplevel : unit -> module_path
+val is_something_opened : unit -> 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
+val is_toplevel : module_path -> bool
+val at_toplevel : module_path -> bool 
+val visible_kn : kernel_name -> bool
 
 (*s Some table-related operations *)
 
@@ -67,11 +61,6 @@ val find_projections : kernel_name -> global_reference list
 val is_projection : global_reference -> bool 
 val projection_arity : global_reference -> int
 
-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 *) 
@@ -94,7 +83,8 @@ val to_keep : global_reference -> bool
 
 (*s Table for user-given custom ML extractions. *)
 
-val ugly_hack_arity_nb_args : (Environ.env -> Term.constr -> int) ref
+(* UGLY HACK: registration of a function defined in [extraction.ml] *)
+val register_type_scheme_nb_args : (Environ.env -> Term.constr -> int) -> unit
 
 val is_custom : global_reference -> bool
 val is_inline_custom : global_reference -> bool
diff --git a/contrib/extraction/test/extract b/contrib/extraction/test/extract
index 2b96f354f..83444be31 100755
--- a/contrib/extraction/test/extract
+++ b/contrib/extraction/test/extract
@@ -4,7 +4,7 @@ vfile=`./ml2v $1`
 d=`dirname $vfile`
 n=`basename $vfile .v`
 if [ -e custom/$n ]; then cat custom/$n > /tmp/extr$$.v; fi  
-echo "Cd \"$d\". Extraction Module $n. " >> /tmp/extr$$.v
+echo "Cd \"$d\". Extraction Library $n. " >> /tmp/extr$$.v
 ../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v 
 out=$?
 rm -f /tmp/extr$$.v
diff --git a/contrib/extraction/test/extract.haskell b/contrib/extraction/test/extract.haskell
index 3f4a59d49..d11bc706e 100755
--- a/contrib/extraction/test/extract.haskell
+++ b/contrib/extraction/test/extract.haskell
@@ -4,7 +4,7 @@ vfile=`./hs2v $1`
 d=`dirname $vfile`
 n=`basename $vfile .v`
 if [ -e custom/$n ]; then cat custom/$n > /tmp/extr$$.v; fi  
-echo "Cd \"$d\". Extraction Language Haskell. Extraction Module $n. " >> /tmp/extr$$.v
+echo "Cd \"$d\". Extraction Language Haskell. Extraction Library $n. " >> /tmp/extr$$.v
 ../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v 
 out=$?
 rm -f /tmp/extr$$.v