Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

12 files changed, 697 insertions, 688 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 5ad4a288..02173c1f 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.ml 10596 2008-02-27 15:30:11Z letouzey $ i*)
+(*i $Id: common.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
 
 open Pp
 open Util
@@ -60,14 +60,14 @@ let unquote s =
     let s = String.copy s in 
     for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
     s
-      
-let rec dottify = function 
-  | [] -> assert false 
-  | [s] -> unquote s 
-  | s::[""] -> unquote s 
-  | s::l -> (dottify l)^"."^(unquote s)
 
-(*s Uppercase/lowercase renamings. *) 
+let rec dottify = function
+  | [] -> assert false
+  | [s] -> s
+  | s::[""] -> s
+  | s::l -> (dottify l)^"."^s
+
+(*s Uppercase/lowercase renamings. *)
 
 let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
@@ -75,9 +75,15 @@ let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
 let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
 
-(* [pr_upper_id id] makes 2 String.copy lesser than [pr_id (uppercase_id id)] *)
-let pr_upper_id id = str (String.capitalize (string_of_id id))
+type kind = Term | Type | Cons | Mod
+
+let upperkind = function
+  | Type -> lang () = Haskell
+  | Term -> false
+  | Cons | Mod -> true
 
+let kindcase_id k id =
+  if upperkind k then uppercase_id id else lowercase_id id
 
 (*s de Bruijn environments for programs *)
 
@@ -122,111 +128,109 @@ let get_db_name n (db,_) =
 
 (*s Tables of global renamings *)
 
-let keywords = ref Idset.empty
-let set_keywords kws = keywords := kws
+let register_cleanup, do_cleanup =
+  let funs = ref [] in
+  (fun f -> funs:=f::!funs), (fun () -> List.iter (fun f -> f ()) !funs)
 
-let global_ids = ref Idset.empty
-let add_global_ids s = global_ids := Idset.add s !global_ids
-let global_ids_list () = Idset.elements !global_ids
+type phase = Pre | Impl | Intf
 
-let empty_env () = [], !global_ids
+let set_phase, get_phase =
+  let ph = ref Impl in ((:=) ph), (fun () -> !ph)
 
-let mktable () = 
-  let h = Hashtbl.create 97 in 
-  (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
+let set_keywords, get_keywords =
+  let k = ref Idset.empty in
+  ((:=) k), (fun () -> !k)
 
-let mkset () = 
-  let h = Hashtbl.create 97 in 
-  (fun x -> Hashtbl.add h x ()), (Hashtbl.mem h), (fun () -> Hashtbl.clear h)
+let add_global_ids, get_global_ids =
+  let ids = ref Idset.empty in
+  register_cleanup (fun () -> ids := get_keywords ());
+  let add s = ids := Idset.add s !ids
+  and get () = !ids
+  in (add,get)
 
-let mktriset () = 
+let empty_env () = [], get_global_ids ()
+
+let mktable autoclean =
   let h = Hashtbl.create 97 in
-  (fun x y z -> Hashtbl.add h (x,y,z) ()), 
-  (fun x y z -> Hashtbl.mem h (x,y,z)), 
-  (fun () -> Hashtbl.clear h)
+  if autoclean then register_cleanup (fun () -> Hashtbl.clear h);
+  (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
 
-(* For each [global_reference], this table will contain the different parts 
-   of its renaming, in [string list] form. *)
-let add_renaming, get_renaming, clear_renaming = mktable ()
+(* A table recording objects in the first level of all MPfile *)
 
-(* Idem for [module_path]. *)
-let add_mp_renaming, get_mp_renaming, clear_mp_renaming = mktable ()
+let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
+  mktable false
 
-(* A table for function modfstlev_rename *)
-let add_modfstlev, get_modfstlev, clear_modfstlev = mktable ()
+(*s The list of external modules that will be opened initially *)
 
-(* A set of all external objects that will have to be fully qualified *)
-let add_static_clash, static_clash, clear_static_clash = mkset ()
+let mpfiles_add, mpfiles_mem, mpfiles_list, mpfiles_clear =
+  let m = ref MPset.empty in
+  let add mp = m:=MPset.add mp !m
+  and mem mp = MPset.mem mp !m
+  and list () = MPset.elements !m
+  and clear () = m:=MPset.empty
+  in
+  register_cleanup clear;
+  (add,mem,list,clear)
 
-(* Two tables of triplets [kind * module_path * string]. The first one 
-   will record the first level of all MPfile, not only the current one. 
-   The second table will contains local renamings. *)
+(*s table indicating the visible horizon at a precise moment,
+    i.e. the stack of structures we are inside.
 
-type kind = Term | Type | Cons | Mod
+  - The sequence of [mp] parts should have the following form: 
+  [X.Y; X; A.B.C; A.B; A; ...], i.e. each addition should either 
+  be a [MPdot] over the last entry, or something new, mainly 
+  [MPself], or [MPfile] at the beginning.
 
-let add_ext_mpmem, ext_mpmem, clear_ext_mpmem = mktriset ()
-let add_loc_mpmem, loc_mpmem, clear_loc_mpmem = mktriset ()
-
-(* The list of external modules that will be opened initially *)
-let add_mpfiles, mem_mpfiles, list_mpfiles, clear_mpfiles = 
-  let m = ref MPset.empty in 
-  (fun mp -> m:= MPset.add mp !m), 
-  (fun mp -> MPset.mem mp !m),
-  (fun () -> MPset.elements !m),
-  (fun () -> m:= MPset.empty)
-
-(*s table containing the visible horizon at a precise moment *)
-
-let visible = ref ([] : module_path list)
-let pop_visible () = visible := List.tl !visible
-let push_visible mp = visible := mp :: !visible
-let top_visible_mp () = List.hd !visible
-
-(*s substitutions for printing signatures *)
-
-let substs = ref empty_subst
-let add_subst msid mp = substs := add_msid msid mp !substs
-let subst_mp mp = subst_mp !substs mp
-let subst_kn kn = subst_kn !substs kn
-let subst_con c = fst (subst_con !substs c)
-let subst_ref = function 
-  | ConstRef con -> ConstRef (subst_con con)
-  | IndRef (kn,i) -> IndRef (subst_kn kn,i)
-  | ConstructRef ((kn,i),j) -> ConstructRef ((subst_kn kn,i),j)
-  | _ -> assert false
-
-
-let duplicate_index = ref 0
-let to_duplicate = ref Gmap.empty
-let add_duplicate mp l = 
-  incr duplicate_index; 
-  let ren = "Coq__" ^ string_of_int (!duplicate_index) in 
-  to_duplicate := Gmap.add (mp,l) ren !to_duplicate
-let check_duplicate mp l = 
-  let mp' = subst_mp mp in 
-  Gmap.find (mp',l) !to_duplicate
-
-type reset_kind = OnlyLocal | AllButExternal | Everything
-
-let reset_allbutext () = 
-  clear_loc_mpmem (); 
-  global_ids := !keywords; 
-  clear_renaming (); 
-  clear_mp_renaming (); 
-  clear_modfstlev (); 
-  clear_static_clash (); 
-  clear_mpfiles (); 
-  duplicate_index := 0; 
-  to_duplicate := Gmap.empty; 
-  visible := []; 
-  substs := empty_subst
- 
-let reset_everything () = reset_allbutext (); clear_ext_mpmem ()
-
-let reset_renaming_tables = function 
-  | OnlyLocal -> clear_loc_mpmem ()
-  | AllButExternal -> reset_allbutext ()
-  | Everything -> reset_everything ()
+  - The [content] part is used to recoard all the names already
+  seen at this level.
+  
+  - The [subst] part is here mainly for printing signature
+  (in which names are still short, i.e. relative to a [msid]).
+*)
+
+type visible_layer = { mp : module_path;
+		       content : ((kind*string),unit) Hashtbl.t }
+
+let pop_visible, push_visible, get_visible, subst_mp =
+  let vis = ref [] and sub = ref [empty_subst] in
+  register_cleanup (fun () -> vis := []; sub := [empty_subst]);
+  let pop () =
+    let v = List.hd !vis in
+    (* we save the 1st-level-content of MPfile for later use *)
+    if get_phase () = Impl && modular () && is_modfile v.mp
+    then add_mpfiles_content v.mp v.content;
+    vis := List.tl !vis;
+    sub := List.tl !sub
+  and push mp o =
+    vis := { mp = mp; content = Hashtbl.create 97 } :: !vis;
+    let s = List.hd !sub in
+    let s = match o with None -> s | Some msid -> add_msid msid mp s in
+    sub := s :: !sub
+  and get () = !vis
+  and subst mp = subst_mp (List.hd !sub) mp
+  in (pop,push,get,subst)
+
+let get_visible_mps () = List.map (function v -> v.mp) (get_visible ())
+let top_visible () = match get_visible () with [] -> assert false | v::_ -> v
+let top_visible_mp () = (top_visible ()).mp
+let add_visible ks = Hashtbl.add (top_visible ()).content ks ()
+
+(* table of local module wrappers used to provide non-ambiguous names *)
+
+let add_duplicate, check_duplicate =
+  let index = ref 0 and dups = ref Gmap.empty in
+  register_cleanup (fun () -> index := 0; dups := Gmap.empty);
+  let add mp l =
+     incr index;
+     let ren = "Coq__" ^ string_of_int (!index) in
+     dups := Gmap.add (mp,l) ren !dups
+  and check mp l = Gmap.find (subst_mp mp, l) !dups
+  in (add,check)
+
+type reset_kind = AllButExternal | Everything
+
+let reset_renaming_tables flag =
+  do_cleanup ();
+  if flag = Everything then clear_mpfiles_content ()
 
 (*S Renaming functions *)
 
@@ -235,248 +239,200 @@ let reset_renaming_tables = function
    with previous [Coq_id] variable, these prefixes are duplicated if already 
    existing. *)
 
-let modular_rename up id = 
+let modular_rename k id =
   let s = string_of_id id in
-  let prefix = if up then "Coq_" else "coq_" in 
-  let check = if up then is_upper else is_lower in 
-  if not (check s) ||
-    (Idset.mem id !keywords) ||
-    (String.length s >= 4 && String.sub s 0 4 = prefix) 
+  let prefix,is_ok =
+    if upperkind k then "Coq_",is_upper else "coq_",is_lower
+  in
+  if not (is_ok s) ||
+    (Idset.mem id (get_keywords ())) ||
+    (String.length s >= 4 && String.sub s 0 4 = prefix)
   then prefix ^ s
   else s
 
-(*s [record_contents_fstlev] finds the names of the first-level objects 
-  exported by the ground-level modules in [struc]. *)
-
-let rec record_contents_fstlev struc = 
-  let upper_type = (lang () = Haskell) in 
-  let addtyp mp id = add_ext_mpmem Type mp (modular_rename upper_type id) in
-  let addcons mp id = add_ext_mpmem Cons mp (modular_rename true id) in
-  let addterm mp id = add_ext_mpmem Term mp (modular_rename false id) in
-  let addmod mp id = add_ext_mpmem Mod mp (modular_rename true id) in 
-  let addfix mp r = 
-    add_ext_mpmem Term mp (modular_rename false (id_of_global r))
-  in
-  let f mp = function 
-    | (l,SEdecl (Dind (_,ind))) -> 
-	Array.iter 
-	  (fun ip -> 
-	     addtyp mp ip.ip_typename; Array.iter (addcons mp) ip.ip_consnames)
-	  ind.ind_packets
-    | (l,SEdecl (Dtype _)) -> addtyp mp (id_of_label l)
-    | (l,SEdecl (Dterm _)) -> addterm mp (id_of_label l)
-    | (l,SEdecl (Dfix  (rv,_,_))) -> Array.iter (addfix mp) rv
-    | (l,SEmodule _) -> addmod mp (id_of_label l)
-    | (l,SEmodtype _) -> addmod mp (id_of_label l)
-  in
-  List.iter (fun (mp,sel) -> List.iter (f mp) sel) struc
-
 (*s For monolithic extraction, first-level modules might have to be renamed 
     with unique numbers *)
 
-let modfstlev_rename l =
-  let coqid = id_of_string "Coq" in 
-  let id = id_of_label l in 
-  try 
-    let coqset = get_modfstlev id in 
-    let nextcoq = next_ident_away coqid coqset in 
-    add_modfstlev id (nextcoq::coqset); 
-    (string_of_id nextcoq)^"_"^(string_of_id id) 
-  with Not_found -> 
-    let s = string_of_id id in 
-    if is_lower s || begins_with_CoqXX s then
-      (add_modfstlev id [coqid]; "Coq_"^s)
-    else
-      (add_modfstlev id []; s)
-
-
-(*s Creating renaming for a [module_path] *)
-
-let rec mp_create_renaming mp = 
-  try get_mp_renaming mp 
-  with Not_found -> 
-    let ren = match mp with 
-      | _ when not (modular ()) && at_toplevel mp -> [""]
-      | MPdot (mp,l) -> 
-	  let lmp = mp_create_renaming mp in 
-	  if lmp = [""] then (modfstlev_rename l)::lmp
-	  else (modular_rename true (id_of_label l))::lmp
-      | MPself msid -> [modular_rename true (id_of_msid msid)]
-      | MPbound mbid -> [modular_rename true (id_of_mbid mbid)]
-      | MPfile _ when not (modular ()) -> assert false
-      | MPfile _ -> [string_of_modfile mp]
-    in add_mp_renaming mp ren; ren
-
-(* [clash mp0 s mpl] checks if [mp0-s] can be printed as [s] when 
-   [mpl] is the context of visible modules. More precisely, we check if 
-   there exists a [mp] in [mpl] that contains [s]. 
+let modfstlev_rename =
+  let add_prefixes,get_prefixes,_ = mktable true in
+  fun l ->
+    let coqid = id_of_string "Coq" in
+    let id = id_of_label l in
+    try
+      let coqset = get_prefixes id in
+      let nextcoq = next_ident_away coqid coqset in
+      add_prefixes id (nextcoq::coqset);
+      (string_of_id nextcoq)^"_"^(string_of_id id)
+    with Not_found ->
+      let s = string_of_id id in
+      if is_lower s || begins_with_CoqXX s then
+	(add_prefixes id [coqid]; "Coq_"^s)
+      else
+	(add_prefixes id []; s)
+
+(*s Creating renaming for a [module_path] : first, the real function ... *)
+
+let rec mp_renaming_fun mp = match mp with
+  | _ when not (modular ()) && at_toplevel mp -> [""]
+  | MPdot (mp,l) ->
+      let lmp = mp_renaming mp in
+      if lmp = [""] then (modfstlev_rename l)::lmp
+      else (modular_rename Mod (id_of_label l))::lmp
+  | MPself msid -> [modular_rename Mod (id_of_msid msid)]
+  | MPbound mbid -> [modular_rename Mod (id_of_mbid mbid)]
+  | MPfile _ when not (modular ()) -> assert false (* see [at_toplevel] above *)
+  | MPfile _ ->
+      assert (get_phase () = Pre);
+      let current_mpfile = (list_last (get_visible ())).mp in
+      if mp <> current_mpfile then mpfiles_add mp;
+      [string_of_modfile mp]
+
+(* ... and its version using a cache *)
+
+and mp_renaming =
+  let add,get,_ = mktable true in
+  fun x ->  try get x with Not_found -> let y = mp_renaming_fun x in add x y; y
+
+(*s Renamings creation for a [global_reference]: we build its fully-qualified
+    name in a [string list] form (head is the short name). *)
+
+let ref_renaming_fun (k,r) =
+  let mp = subst_mp (modpath_of_r r) in
+  let l = mp_renaming mp in
+  let s =
+    if l = [""] (* this happens only at toplevel of the monolithic case *)
+    then
+      let globs = Idset.elements (get_global_ids ()) in
+      let id = next_ident_away (kindcase_id k (safe_id_of_global r)) globs in
+      string_of_id id
+    else modular_rename k (safe_id_of_global r)
+  in
+  add_global_ids (id_of_string s);
+  s::l
+
+(* Cached version of the last function *)
+
+let ref_renaming =
+  let add,get,_ = mktable true in
+  fun x -> try get x with Not_found -> let y = ref_renaming_fun x in add x y; y
+
+(* [visible_clash mp0 (k,s)] checks if [mp0-s] of kind [k]
+   can be printed as [s] in the current context of visible
+   modules. More precisely, we check if there exists a 
+   visible [mp] that contains [s]. 
    The verification stops if we encounter [mp=mp0]. *)
 
-let rec clash mem mp0 s = function 
+let rec clash mem mp0 ks = function
   | [] -> false
   | mp :: _ when mp = mp0 -> false
-  | mp :: mpl -> mem mp s || clash mem mp0 s mpl
-    
-(*s Initial renamings creation, for modular extraction. *) 
-
-let create_modular_renamings struc = 
-  let current_module = fst (List.hd struc) in 
-  let { typ = ty ; trm = tr ; cons = co } = struct_get_references_set struc 
-  in 
-  (* 1) creates renamings of objects *)
-  let add upper r = 
-    let mp = modpath_of_r r in 
-    let l = mp_create_renaming mp in 
-    let s = modular_rename upper (id_of_global r) in 
-    add_global_ids (id_of_string s);
-    add_renaming r (s::l); 
-    begin try 
-      let mp = modfile_of_mp mp in if mp <> current_module then add_mpfiles mp
-    with Not_found -> () 
-    end; 
-  in
-  Refset.iter (add (lang () = Haskell)) ty; 
-  Refset.iter (add true) co;
-  Refset.iter (add false) tr;
-  
-  (* 2) determines the opened libraries. *)
-  let used_modules = list_mpfiles () in 
-  let used_modules' = List.rev used_modules in 
-  let str_list = List.map string_of_modfile used_modules' 
-  in
-  let rec check_elsewhere mpl sl = match mpl, sl with
-    | [], [] -> []
-    | mp::mpl, _::sl -> 
-	if List.exists (ext_mpmem Mod mp) sl then
-	  check_elsewhere mpl sl
-	else mp :: (check_elsewhere mpl sl)
-    | _ -> assert false
-  in 
-  let opened_modules = check_elsewhere used_modules' str_list in 
-  clear_mpfiles (); 
-  List.iter add_mpfiles opened_modules; 
-
-  (* 3) determines the potential clashes *)
-  let needs_qualify k r = 
-    let mp = modpath_of_r r in 
-      if (is_modfile mp) && mp <> current_module && 
-	(clash (ext_mpmem k) mp (List.hd (get_renaming r)) opened_modules)
-      then add_static_clash r
-  in
-    Refset.iter (needs_qualify Type) ty;
-    Refset.iter (needs_qualify Term) tr;
-    Refset.iter (needs_qualify Cons) co;
-    List.rev opened_modules
-
-(*s Initial renamings creation, for monolithic extraction. *)
-
-let create_mono_renamings struc = 
-  let { typ = ty ; trm = tr ; cons = co } = struct_get_references_list struc in
-  let add upper r = 
-    let mp = modpath_of_r r in 
-    let l = mp_create_renaming mp in
-    let mycase = if upper then uppercase_id else lowercase_id in 
-    let id = 
-      if l = [""] then 
-	next_ident_away (mycase (id_of_global r)) (global_ids_list ())
-      else id_of_string (modular_rename upper (id_of_global r))
-    in 
-    add_global_ids id; 
-    add_renaming r ((string_of_id id)::l) 
-  in
-  List.iter (add (lang () = Haskell)) (List.rev ty); 
-  List.iter (add false) (List.rev tr);
-  List.iter (add true) (List.rev co);
-  []
-
-let create_renamings struc = 
-  if modular () then create_modular_renamings struc
-  else create_mono_renamings struc
-    
-		    
+  | mp :: _ when mem mp ks -> true
+  | _ :: mpl -> clash mem mp0 ks mpl
+
+let mpfiles_clash mp0 ks =
+  clash (fun mp -> Hashtbl.mem (get_mpfiles_content mp)) mp0 ks
+    (List.rev (mpfiles_list ()))
+
+let visible_clash mp0 ks =
+  let rec clash = function
+    | [] -> false
+    | v :: _ when v.mp = mp0 -> false
+    | v :: _ when Hashtbl.mem v.content ks -> true
+    | _ :: vis -> clash vis
+  in clash (get_visible ())
+
+(* After the 1st pass, we can decide which modules will be opened initially *)
+
+let opened_libraries () =
+  if not (modular ()) then []
+  else
+    let used = mpfiles_list () in
+    let rec check_elsewhere avoid = function
+      | [] -> []
+      | mp :: mpl ->
+	  let clash s = Hashtbl.mem (get_mpfiles_content mp) (Mod,s) in
+	  if List.exists clash avoid
+	  then check_elsewhere avoid mpl
+	  else mp :: check_elsewhere (string_of_modfile mp :: avoid) mpl
+    in
+    let opened = check_elsewhere [] used in
+    mpfiles_clear ();
+    List.iter mpfiles_add opened;
+    opened
+
 (*s On-the-fly qualification issues for both monolithic or modular extraction. *)
 
-let pp_global k r = 
-  let ls = get_renaming r in 
-  assert (List.length ls > 1); 
-  let s = List.hd ls in 
-  let mp = modpath_of_r r in 
-  if mp = top_visible_mp () then 
+(* First, a function that factorize the printing of both [global_reference]
+   and module names for ocaml. When [k=Mod] then [olab=None], otherwise it 
+   contains the label of the reference to print. 
+   Invariant: [List.length ls >= 2], simpler situations are handled elsewhere. *)
+
+let pp_gen k mp ls olab =
+  try (* what is the largest prefix of [mp] that belongs to [visible]? *)
+    let prefix = common_prefix_from_list mp (get_visible_mps ()) in
+    let delta = mp_length mp - mp_length prefix in
+    assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
+    let ls = list_firstn (delta + if k = Mod then 0 else 1) ls in
+    let s,ls' = list_sep_last ls in
+    (* Reference r / module path mp is of the form [<prefix>.s.<List.rev ls'>].
+       Difficulty: in ocaml the prefix part cannot be used for
+       qualification (we are inside it) and the rest of the long
+       name may be hidden. 
+       Solution: we duplicate the _definition_ of r / mp in a Coq__XXX module *)
+    let k' = if ls' = [] then k else Mod in
+    if visible_clash prefix (k',s) then
+      let front = if ls' = [] && k <> Mod then [s] else ls' in
+      let lab = (* label associated with s *)
+	if delta = 0 && k <> Mod then Option.get olab
+	else get_nth_label_mp delta mp
+      in
+      try dottify (front @ [check_duplicate prefix lab])
+      with Not_found ->
+	assert (get_phase () = Pre); (* otherwise it's too late *)
+	add_duplicate prefix lab; dottify ls
+    else dottify ls
+  with Not_found ->
+    (* [mp] belongs to a closed module, not one of [visible]. *)
+    let base = base_mp mp in
+    let base_s,ls1 = list_sep_last ls in
+    let s,ls2 = list_sep_last ls1 in
+    (* [List.rev ls] is [base_s :: s :: List.rev ls2] *)
+    let k' = if ls2 = [] then k else Mod in
+    if modular () && (mpfiles_mem base) &&
+      (not (mpfiles_clash base (k',s))) &&
+      (not (visible_clash base (k',s)))
+    then (* Standard situation of an object in another file: *)
+      (* Thanks to the "open" of this file we remove its name *)
+      dottify ls1
+    else if visible_clash base (Mod,base_s) then
+      error_module_clash base_s
+    else dottify ls
+
+let pp_global k r =
+  let ls = ref_renaming (k,r) in
+  assert (List.length ls > 1);
+  let s = List.hd ls in
+  let mp = subst_mp (modpath_of_r r) in
+  if mp = top_visible_mp () then
     (* simpliest situation: definition of r (or use in the same context) *)
     (* we update the visible environment *)
-    (add_loc_mpmem k mp s; unquote s)
-  else match lang () with 
+    (add_visible (k,s); unquote s)
+  else match lang () with
     | Scheme -> unquote s (* no modular Scheme extraction... *)
-    | Haskell -> 
-	(* for the moment we always qualify in modular Haskell *)
-	if modular () then dottify ls else s
-    | Ocaml -> 
-	try (* has [mp] something in common with one of [!visible] ? *)
-	  let prefix = common_prefix_from_list mp !visible in 
-	  let delta = mp_length mp - mp_length prefix in 
-	  let ls = list_firstn (delta+1) ls in 
-	  (* Difficulty: in ocaml we cannot qualify more than [ls], 
-             but this (not-so-long) name can in fact be hidden. Solution: 
-	     duplication of the _definition_ of r in a Coq__XXX module *)
-	  let s,ls' = list_sep_last ls in 
-	  let k' = if ls' = [] then k else Mod in 
-	  if clash (loc_mpmem k') prefix s !visible then 
-	    let front = if ls' = [] then [s] else ls' in 
-	    let l = get_nth_label delta r in 
-	    try dottify (front @ [check_duplicate prefix l])
-	    with Not_found -> add_duplicate prefix l; dottify ls
-	  else dottify ls 
-	with Not_found -> 
-	  (* [mp] belongs to a closed module, not one of [!visible]. *)
-	  let base = base_mp mp in 
-	  let base_s,ls1 = list_sep_last ls in 
-	  let s,ls2 = list_sep_last ls1 in  
-	  let k' = if ls2 = [] then k else Mod in 
-	  if modular () && (mem_mpfiles base) && 
-	    not (static_clash r) && 
-	    (* k' = Mod can't clash in an opened module, see earlier check *)
-	    not (clash (loc_mpmem k') base s !visible)
-	  then (* Standard situation of an object in another file: *)
-	    (* Thanks to the "open" of this file we remove its name *) 
-	    dottify ls1
-	  else if clash (loc_mpmem Mod) base base_s !visible then 
-	    error_module_clash base_s
-	  else dottify ls 
-	    
+    | Haskell -> if modular () then dottify ls else s
+	(* for the moment we always qualify in modular Haskell... *)
+    | Ocaml -> pp_gen k mp ls (Some (label_of_r r))
+
 (* The next function is used only in Ocaml extraction...*)
-let pp_module mp = 
-  let ls = mp_create_renaming mp in
-  if List.length ls = 1 then dottify ls 
-  else match mp with 
-    | MPdot (mp0,_) when mp0 = top_visible_mp () -> 
+let pp_module mp =
+  let mp = subst_mp mp in
+  let ls = mp_renaming mp in
+  if List.length ls = 1 then dottify ls
+  else match mp with
+    | MPdot (mp0,_) when mp0 = top_visible_mp () ->
 	(* simpliest situation: definition of mp (or use in the same context) *)
 	(* we update the visible environment *)
-	let s = List.hd ls in 
-	add_loc_mpmem Mod mp0 s; s
-    | _ ->
-	try (* has [mp] something in common with one of those in [!visible] ? *)
-	  let prefix = common_prefix_from_list mp !visible in 
-	  assert (mp <> prefix); (* no use of mp as whole module from itself *)
-	  let delta = mp_length mp - mp_length prefix in 
-	  let ls = list_firstn delta ls in
-	  (* Difficulty: in ocaml we cannot qualify more than [ls], 
-	     but this (not-so-long) name can in fact be hidden. Solution: 
-	     duplication of the _definition_ of mp via a Coq__XXX module *)
-	  let s,ls' = list_sep_last ls in 
-	  if clash (loc_mpmem Mod) prefix s !visible then 
-	    let l = get_nth_label_mp delta mp in 
-	    try dottify (ls' @ [check_duplicate prefix l])
-	    with Not_found -> add_duplicate prefix l; dottify ls
-	  else dottify ls
-	with Not_found -> 
-	  (* [mp] belongs to a closed module, not one of [!visible]. *)
-	  let base = base_mp mp in 
-	  let base_s,ls' = list_sep_last ls in 
-	  let s = fst (list_sep_last ls) in 
-	  if modular () && (mem_mpfiles base) &&
-	    not (clash (loc_mpmem Mod) base s !visible)
-	  then dottify ls'
-	  else if clash (loc_mpmem Mod) base base_s !visible then 
-	    error_module_clash base_s
-	  else dottify ls
+	let s = List.hd ls in
+	add_visible (Mod,s); s
+    | _ -> pp_gen Mod mp ls None
+
 
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 5cd26584..b7e70414 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.mli 10232 2007-10-17 12:32:10Z letouzey $ i*)
+(*i $Id: common.mli 11559 2008-11-07 22:03:34Z letouzey $ i*)
 
 open Names
 open Libnames
@@ -24,11 +24,6 @@ val pr_binding : identifier list -> std_ppcmds
 
 val rename_id : identifier -> Idset.t -> identifier
 
-val lowercase_id : identifier -> identifier
-val uppercase_id : identifier -> identifier
-
-val pr_upper_id : identifier -> std_ppcmds
-
 type env = identifier list * Idset.t
 val empty_env : unit -> env
 
@@ -37,9 +32,12 @@ val rename_tvars: Idset.t -> identifier list -> identifier list
 val push_vars : identifier list -> env -> identifier list * env
 val get_db_name : int -> env -> identifier
 
-val record_contents_fstlev : ml_structure -> unit
+type phase = Pre | Impl | Intf
 
-val create_renamings : ml_structure -> module_path list
+val set_phase : phase -> unit
+val get_phase : unit -> phase
+
+val opened_libraries : unit -> module_path list
 
 type kind = Term | Type | Cons | Mod
 
@@ -47,14 +45,12 @@ val pp_global : kind -> global_reference -> string
 val pp_module : module_path -> string
 
 val top_visible_mp : unit -> module_path
-val push_visible : module_path -> unit
+val push_visible : module_path -> mod_self_id option -> unit
 val pop_visible : unit -> unit
 
-val add_subst : mod_self_id -> module_path -> unit
-
 val check_duplicate : module_path -> label -> string
 
-type reset_kind = OnlyLocal | AllButExternal | Everything
+type reset_kind = AllButExternal | Everything
 
 val reset_renaming_tables : reset_kind -> unit
 
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 311b42c0..49a86200 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.ml 10794 2008-04-15 00:12:06Z letouzey $ i*)
+(*i $Id: extract_env.ml 11846 2009-01-22 18:55:10Z letouzey $ i*)
 
 open Term
 open Declarations
@@ -83,8 +83,8 @@ module type VISIT = sig
 end
   
 module Visit : VISIT = struct 
-  (* Thanks to C.S.C, what used to be in a single KNset should now be split 
-     into a KNset (for inductives and modules names) and a Cset for constants 
+  (* What used to be in a single KNset should now be split into a KNset
+     (for inductives and modules names) and a Cset for constants
      (and still the remaining MPset) *)
   type must_visit = 
       { mutable kn : KNset.t; mutable con : Cset.t; mutable mp : MPset.t }
@@ -140,6 +140,30 @@ let factor_fix env l cb msb =
     labels, recd, msb''
   end
 
+let build_mb expr typ_opt =
+  { mod_expr = Some expr;
+    mod_type = typ_opt;
+    mod_constraints = Univ.Constraint.empty;
+    mod_alias = Mod_subst.empty_subst;
+    mod_retroknowledge = [] }
+
+let my_type_of_mb env mb =
+  match mb.mod_type with
+    | Some mtb -> mtb
+    | None -> Modops.eval_struct env (Option.get mb.mod_expr)
+
+(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
+    To check with Elie. *)
+
+let env_for_mtb_with env mtb idl =
+  let msid,sig_b = match Modops.eval_struct env mtb with
+    | SEBstruct(msid,sig_b) -> msid,sig_b
+    | _ -> assert false
+  in
+  let l = label_of_id (List.hd idl) in
+  let before = fst (list_split_at (fun (l',_) -> l=l') sig_b) in
+  Modops.add_signature (MPself msid) before env
+
 (* From a [structure_body] (i.e. a list of [structure_field_body])
    to specifications. *)
 
@@ -151,7 +175,7 @@ let rec extract_sfb_spec env mp = function
       let specs = extract_sfb_spec env mp msig in
       if logical_spec s then specs 
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
-  | (l,SFBmind cb) :: msig -> 
+  | (l,SFBmind _) :: msig -> 
       let kn = make_kn mp empty_dirpath l in 
       let s = Sind (kn, extract_inductive env kn) in 
       let specs = extract_sfb_spec env mp msig in
@@ -159,45 +183,52 @@ let rec extract_sfb_spec env mp = function
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmodule mb) :: msig -> 
       let specs = extract_sfb_spec env mp msig in 
-      let mtb = Modops.type_of_mb env mb in 
-      let spec = extract_seb_spec env (mb.mod_type<>None) mtb in 
+      let spec = extract_seb_spec env (my_type_of_mb env mb) in
       (l,Smodule spec) :: specs
   | (l,SFBmodtype mtb) :: msig -> 
       let specs = extract_sfb_spec env mp msig in
-      (l,Smodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: specs
-  | (l,SFBalias(mp1,_))::msig -> 
-      extract_sfb_spec env mp 
-	((l,SFBmodule {mod_expr = Some (SEBident mp1);
-		      mod_type = None;
-		      mod_constraints = Univ.Constraint.empty;
-		      mod_alias = Mod_subst.empty_subst;
-		      mod_retroknowledge = []})::msig)
+      (l,Smodtype (extract_seb_spec env mtb.typ_expr)) :: specs
+  | (l,SFBalias(mp1,typ_opt,_))::msig -> 
+      let mb = build_mb (SEBident mp1) typ_opt in
+      extract_sfb_spec env mp ((l,SFBmodule mb) :: msig)
 
 (* From [struct_expr_body] to specifications *)
 
+(* Invariant: the [seb] given to [extract_seb_spec] should either come:
+   - from a [mod_type] or [type_expr] field
+   - from the output of [Modops.eval_struct].
+   This way, any encountered [SEBident] should be a true module type.
+   For instance, [my_type_of_mb] ensures this invariant.
+*)
 
-and extract_seb_spec env truetype = function
-  | SEBident kn when truetype -> Visit.add_mp kn; MTident kn 
+and extract_seb_spec env = function
+  | SEBident mp -> Visit.add_mp mp; MTident mp
   | SEBwith(mtb',With_definition_body(idl,cb))->
-      let mtb''= extract_seb_spec env truetype mtb' in
-      (match extract_with_type env cb with (* cb peut contenir des kn  *)
+      let env' = env_for_mtb_with env mtb' idl in
+      let mtb''= extract_seb_spec env mtb' in
+      (match extract_with_type env' cb with (* cb peut contenir des kn  *)
 	 | None ->  mtb''
 	 | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ)))
-  | SEBwith(mtb',With_module_body(idl,mp,_))-> 
+  | SEBwith(mtb',With_module_body(idl,mp,_,_))-> 
       Visit.add_mp mp;
-      MTwith(extract_seb_spec env truetype mtb',
+      MTwith(extract_seb_spec env mtb',
 	     ML_With_module(idl,mp))
+(* TODO: On pourrait peut-etre oter certaines eta-expansion, du genre:
+   | SEBfunctor(mbid,_,SEBapply(m,SEBident (MPbound mbid2),_)) 
+     when mbid = mbid2 -> extract_seb_spec env m 
+   (* faudrait alors ajouter un test de non-apparition de mbid dans mb *)
+*)
   | SEBfunctor (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_seb_spec env true mtb.typ_expr, 
-		  extract_seb_spec env' truetype mtb')
+      MTfunsig (mbid, extract_seb_spec env mtb.typ_expr,
+		extract_seb_spec env' mtb')
   | SEBstruct (msid, msig) -> 
       let mp = MPself msid in 
       let env' = Modops.add_signature mp msig env in 
 	MTsig (msid, extract_sfb_spec env' mp msig) 
-  | (SEBapply _|SEBident _ (*when not truetype*)) as mtb -> 
-      extract_seb_spec env truetype (Modops.eval_struct env mtb)
+  | SEBapply _ as mtb ->
+      extract_seb_spec env (Modops.eval_struct env mtb)
 
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
@@ -248,19 +279,11 @@ let rec extract_sfb env mp all = function
       let ms = extract_sfb env mp all msb in
       let mp = MPdot (mp,l) in
        if all || Visit.needed_mp mp then 
-	(l,SEmodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: ms
-      else ms
-  | (l,SFBalias (mp1,cst)) :: msb -> 
-      let ms = extract_sfb env mp all msb in
-      let mp = MPdot (mp,l) in 
-      if all || Visit.needed_mp mp then 
-	(l,SEmodule (extract_module env mp true 
-		       {mod_expr = Some (SEBident mp1);
-			mod_type = None;
-		        mod_constraints= Univ.Constraint.empty;
-			mod_alias = empty_subst;
-			mod_retroknowledge = []})) :: ms
+	(l,SEmodtype (extract_seb_spec env mtb.typ_expr)) :: ms
       else ms
+  | (l,SFBalias (mp1,typ_opt,_)) :: msb ->
+      let mb = build_mb (SEBident mp1) typ_opt in
+      extract_sfb env mp all ((l,SFBmodule mb) :: msb)
 
 (* From [struct_expr_body] to implementations *)
 
@@ -274,7 +297,7 @@ and extract_seb env mpo all = function
   | SEBfunctor (mbid, mtb, meb) -> 
       let mp = MPbound mbid in 
       let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in 
-      MEfunctor (mbid, extract_seb_spec env true mtb.typ_expr, 
+      MEfunctor (mbid, extract_seb_spec env mtb.typ_expr,
 		 extract_seb env' None true meb)
   | SEBstruct (msid, msb) -> 
       let mp,msb = match mpo with 
@@ -288,17 +311,8 @@ and extract_seb env mpo all = function
 and extract_module env 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 = Option.get mb.mod_expr in
-  let mtb = match mb.mod_type with 
-    | None -> Modops.eval_struct env meb 
-    | 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. *)
-  (* PL 26/02/2008: is this still relevant ?
-  let mtb = replicate_msid meb mtb in *)
-  { ml_mod_expr = extract_seb env (Some mp) all meb;
-    ml_mod_type = extract_seb_spec env (mb.mod_type<>None) mtb }
+  { ml_mod_expr = extract_seb env (Some mp) all (Option.get mb.mod_expr);
+    ml_mod_type = extract_seb_spec env (my_type_of_mb env mb) }
 
 
 let unpack = function MEstruct (_,sel) -> sel | _ -> assert false 
@@ -345,28 +359,38 @@ let mono_filename f =
 
 (* Builds a suitable filename from a module id *)
 
-let module_filename m = 
-  let d = descr () in 
-  let f = if d.capital_file then String.capitalize else String.uncapitalize in 
-  let fn = f (string_of_id m) in
-  Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, m
+let module_filename fc =
+  let d = descr () in
+  let fn = if d.capital_file then fc else String.uncapitalize fc
+  in
+  Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, id_of_string fc
 
 (*s Extraction of one decl to stdout. *)
 
 let print_one_decl struc mp decl =
-  let d = descr () in 
-  reset_renaming_tables AllButExternal; 
-  ignore (create_renamings struc);
-  push_visible mp; 
-  msgnl (d.pp_decl decl); 
+  let d = descr () in
+  reset_renaming_tables AllButExternal;
+  set_phase Pre;
+  ignore (d.pp_struct struc);
+  set_phase Impl;
+  push_visible mp None;
+  msgnl (d.pp_decl decl);
   pop_visible ()
 
 (*s Extraction of a ml struct to a file. *)
 
-let print_structure_to_file (fn,si,mo) struc =
-  let d = descr () in 
-  reset_renaming_tables AllButExternal; 
-  let used_modules = create_renamings struc in 
+let formatter dry file =
+  if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
+  else match file with
+    | None -> !Pp_control.std_ft
+    | Some cout ->
+	let ft = Pp_control.with_output_to cout in
+	Option.iter (Format.pp_set_margin ft) (Pp_control.get_margin ());
+	ft
+
+let print_structure_to_file (fn,si,mo) dry struc =
+  let d = descr () in
+  reset_renaming_tables AllButExternal;
   let unsafe_needs = {
     mldummy = struct_ast_search ((=) MLdummy) struc; 
     tdummy = struct_type_search Mlutil.isDummy struc; 
@@ -375,40 +399,39 @@ let print_structure_to_file (fn,si,mo) struc =
       if lang () <> Haskell then false 
       else struct_ast_search (function MLmagic _ -> true | _ -> false) struc }
   in
-  (* print the implementation *)
-  let cout = Option.map open_out fn in 
-  let ft = match cout with 
-    | None -> !Pp_control.std_ft
-    | Some cout -> Pp_control.with_output_to cout in 
-  begin try 
-    msg_with ft (d.preamble mo used_modules unsafe_needs);
-    if lang () = Ocaml then begin 
-      (* for computing objects to duplicate *)
-      let devnull = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in
-      msg_with devnull (d.pp_struct struc);
-      reset_renaming_tables OnlyLocal; 
-    end; 
+  (* First, a dry run, for computing objects to rename or duplicate *)
+  set_phase Pre;
+  let devnull = formatter true None in
+  msg_with devnull (d.pp_struct struc);
+  let opened = opened_libraries () in
+  (* Print the implementation *)
+  let cout = if dry then None else Option.map open_out fn in
+  let ft = formatter dry cout in
+  begin try
+    (* The real printing of the implementation *)
+    set_phase Impl;
+    msg_with ft (d.preamble mo opened unsafe_needs);
     msg_with ft (d.pp_struct struc);
     Option.iter close_out cout; 
   with e -> 
     Option.iter close_out cout; raise e
   end;
-  Option.iter info_file fn;
-  (* print the signature *)
-  Option.iter 
-    (fun si -> 
+  if not dry then Option.iter info_file fn;
+  (* Now, let's print the signature *)
+  Option.iter
+    (fun si ->
        let cout = open_out si in
-       let ft = Pp_control.with_output_to cout in
-       begin try 
-	 msg_with ft (d.sig_preamble mo used_modules unsafe_needs);
-	 reset_renaming_tables OnlyLocal;
+       let ft = formatter false (Some cout) in
+       begin try
+	 set_phase Intf;
+	 msg_with ft (d.sig_preamble mo opened unsafe_needs);
 	 msg_with ft (d.pp_sig (signature_of_structure struc));
 	 close_out cout;
        with e -> 
 	 close_out cout; raise e 
        end; 
        info_file si)
-    si
+    (if dry then None else si)
 
 
 (*********************************************)
@@ -426,51 +449,56 @@ let init modular =
   reset ();
   if modular && lang () = Scheme then error_scheme ()
 
+(* From a list of [reference], let's retrieve whether they correspond
+   to modules or [global_reference]. Warn the user if both is possible. *)
+
+let rec locate_ref = function
+  | [] -> [],[]
+  | r::l ->
+      let q = snd (qualid_of_reference r) in
+      let mpo = try Some (Nametab.locate_module q) with Not_found -> None
+      and ro = try Some (Nametab.locate q) with Not_found -> None in
+      match mpo, ro with
+	| None, None -> Nametab.error_global_not_found q
+	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
+	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
+	| Some mp, Some r ->
+	    warning_both_mod_and_cst q mp r;
+	    let refs,mps = locate_ref l in refs,mp::mps
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when 
     extracting to a file with the command: 
     \verb!Extraction "file"! [qualid1] ... [qualidn]. *)
 
-let full_extraction f qualids = 
-  init false; 
-  let rec find = function 
-    | [] -> [],[]
-    | q::l -> 
-	let refs,mps = find l in 
-	try 
-	  let mp = Nametab.locate_module (snd (qualid_of_reference q)) in 
-	  if is_modfile mp then error_MPfile_as_mod mp true; 
-	  refs,(mp::mps)
-	with Not_found -> (Nametab.global q)::refs, mps 
-  in  
-  let refs,mps = find qualids in
-  let struc = optimize_struct refs (mono_environment refs mps) in 
-  warning_axioms (); 
-  print_structure_to_file (mono_filename f) struc; 
+let full_extr f (refs,mps) =
+  init false;
+  List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps;
+  let struc = optimize_struct refs (mono_environment refs mps) in
+  warning_axioms ();
+  print_structure_to_file (mono_filename f) false struc;
   reset ()
 
+let full_extraction f lr = full_extr f (locate_ref lr)
+
 
 (*s Simple extraction in the Coq toplevel. The vernacular command 
     is \verb!Extraction! [qualid]. *)
 
-let simple_extraction qid = 
-  init false; 
-  try 
-    let mp = Nametab.locate_module (snd (qualid_of_reference qid)) in 
-    if is_modfile mp then error_MPfile_as_mod mp true; 
-    full_extraction None [qid]
-  with Not_found -> 
-    let r = Nametab.global qid in 
-    if is_custom r then
-      msgnl (str "User defined extraction:" ++ spc () ++ 
-	       str (find_custom r) ++ fnl ()) 
-    else
-      let struc = optimize_struct [r] (mono_environment [r] []) in
-      let d = get_decl_in_structure r struc in 
-      warning_axioms (); 
-      print_one_decl struc (modpath_of_r r) d;
-      reset ()
+let simple_extraction r = match locate_ref [r] with
+  | ([], [mp]) as p -> full_extr None p
+  | [r],[] ->
+      init false;
+      if is_custom r then
+	msgnl (str "User defined extraction:" ++ spc () ++
+		 str (find_custom r) ++ fnl ())
+      else
+	let struc = optimize_struct [r] (mono_environment [r] []) in
+	let d = get_decl_in_structure r struc in
+	warning_axioms ();
+	print_one_decl struc (modpath_of_r r) d;
+	reset ()
+  | _ -> assert false
 
 
 (*s (Recursive) Extraction of a library. The vernacular command is 
@@ -489,19 +517,16 @@ let extraction_library is_rec m =
     if Visit.needed_mp mp 
     then (mp, unpack (extract_seb env (Some mp) true meb)) :: l 
     else l
-  in 
-  let struc = List.fold_left select [] l in 
-  let struc = optimize_struct [] struc in 
-  warning_axioms (); 
-  record_contents_fstlev struc; 
-  let rec print = function 
-    | [] -> () 
-    | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l 
-    | (MPfile dir, sel) as e :: l -> 
-	let short_m = snd (split_dirpath dir) in
-	print_structure_to_file (module_filename short_m) [e]; 
-	print l 
+  in
+  let struc = List.fold_left select [] l in
+  let struc = optimize_struct [] struc in
+  warning_axioms ();
+  let print = function
+    | (MPfile dir as mp, sel) as e ->
+	let dry = not is_rec && dir <> dir_m in
+	let s = string_of_modfile mp in
+	print_structure_to_file (module_filename s) dry [e]
     | _ -> assert false
-  in 
-  print struc; 
+  in
+  List.iter print struc;
   reset ()
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index fdc84a64..fa006c1c 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.ml 10497 2008-02-01 12:18:37Z soubiran $ i*)
+(*i $Id: extraction.ml 11459 2008-10-16 16:29:07Z letouzey $ i*)
 
 (*i*)
 open Util
@@ -876,19 +876,17 @@ let extract_constant_spec env kn cb =
 	let t = snd (record_constant_type env kn (Some typ)) in 
 	Sval (r, type_expunge env t)
 
-let extract_with_type env cb = 
-  let typ = Typeops.type_of_constant_type env cb.const_type in 
-  match flag_of_type env typ with 
-    | (_ , Default) -> None
-    | (Logic, TypeScheme) ->Some ([],Tdummy Ktype)
-    | (Info, TypeScheme) -> 
-	let s,vl = type_sign_vl env typ in 
-	  (match cb.const_body with 
-	  | None -> assert false
-	  | Some body -> 
-	      let db = db_from_sign s in 
-	      let t = extract_type_scheme env db (force body) (List.length s)
-	      in Some ( vl, t) )
+let extract_with_type env cb =
+  let typ = Typeops.type_of_constant_type env cb.const_type in
+  match flag_of_type env typ with
+    | (Info, TypeScheme) ->
+	let s,vl = type_sign_vl env typ in
+	let body = Option.get cb.const_body in
+	let db = db_from_sign s in
+	let t = extract_type_scheme env db (force body) (List.length s) in
+	Some (vl, t)
+    | _ -> None
+
 		   
 let extract_inductive env kn = 
   let ind = extract_ind env kn in 
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index cb95808d..345cb307 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -27,7 +27,13 @@ END
 open Table
 open Extract_env
 
+let pr_language = function
+  | Ocaml -> str "Ocaml" 
+  | Haskell -> str "Haskell"
+  | Scheme -> str "Scheme"
+
 VERNAC ARGUMENT EXTEND language
+PRINTED BY pr_language
 | [ "Ocaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
 | [ "Scheme" ] -> [ Scheme ]
@@ -83,6 +89,23 @@ VERNAC COMMAND EXTEND ResetExtractionInline
   -> [ reset_extraction_inline () ]
 END
 
+VERNAC COMMAND EXTEND ExtractionBlacklist
+(* Force Extraction to not use some filenames *)
+| [ "Extraction" "Blacklist" ne_ident_list(l) ]
+  -> [ extraction_blacklist l ]
+END
+
+VERNAC COMMAND EXTEND PrintExtractionBlacklist
+| [ "Print" "Extraction" "Blacklist" ]
+  -> [ print_extraction_blacklist () ]
+END
+
+VERNAC COMMAND EXTEND ResetExtractionBlacklist
+| [ "Reset" "Extraction" "Blacklist" ]
+  -> [ reset_extraction_blacklist () ]
+END
+
+
 (* Overriding of a Coq object by an ML one *)
 VERNAC COMMAND EXTEND ExtractionConstant
 | [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ]
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 0ef225c0..3f0366e6 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: haskell.ml 10233 2007-10-17 23:29:08Z letouzey $ i*)
+(*i $Id: haskell.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
 
 (*s Production of Haskell syntax. *)
 
@@ -22,6 +22,9 @@ open Common
 
 (*s Haskell renaming issues. *)
 
+let pr_lower_id id = str (String.uncapitalize (string_of_id id))
+let pr_upper_id id = str (String.capitalize (string_of_id id))
+
 let keywords =     
   List.fold_right (fun s -> Idset.add (id_of_string s))
   [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
@@ -62,8 +65,6 @@ let pp_abst = function
              prlist_with_sep (fun () -> (str " ")) pr_id l ++
              str " ->" ++ spc ())
 
-let pr_lower_id id = pr_id (lowercase_id id)
-
 (*s The pretty-printer for haskell syntax *)
 
 let pp_global k r = 
@@ -313,7 +314,7 @@ let pp_structure_elem = function
 
 let pp_struct = 
   let pp_sel (mp,sel) = 
-    push_visible mp; 
+    push_visible mp None; 
     let p = prlist_strict pp_structure_elem sel in 
     pop_visible (); p
   in 
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 0c906712..68adeb81 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modutil.ml 11262 2008-07-24 20:59:29Z letouzey $ i*)
+(*i $Id: modutil.ml 11602 2008-11-18 00:08:33Z letouzey $ i*)
 
 open Names
 open Declarations
@@ -18,23 +18,9 @@ open Table
 open Mlutil
 open Mod_subst
 
-(*S Functions upon modules missing in [Modops]. *) 
-
-(*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 
-  | SEBfunctor (_, _, meb), SEBfunctor (mbid, mtb1, mtb2) -> 
-      let mtb' = replicate_msid meb mtb2 in 
-      if mtb' == mtb2 then mtb else SEBfunctor (mbid, mtb1, mtb')
-  | SEBstruct (msid, _), SEBstruct (msid1, msig) when msid <> msid1 -> 
-      let msig' = Modops.subst_signature_msid msid1 (MPself msid) msig in
-      if msig' == msig then SEBstruct (msid, msig) else SEBstruct (msid, msig')
-  | _ -> mtb
-
 (*S Functions upon ML modules. *)
-let rec  msid_of_mt = function
+
+let rec msid_of_mt = function
   | MTident mp -> begin
       match Modops.eval_struct (Global.env()) (SEBident mp) with
 	| SEBstruct(msid,_) -> MPself msid
@@ -42,12 +28,7 @@ let rec  msid_of_mt = function
     end
   | MTwith(mt,_)-> msid_of_mt mt
   | _ -> anomaly "Extraction:the With operator isn't applied to a name"
-      
-let  make_mp_with mp idl =
-  let idl_rev = List.rev idl in
-  let idl' = List.rev (List.tl idl_rev) in
-    (List.fold_left (fun mp id -> MPdot(mp,label_of_id id))
-       mp idl')
+
 (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a 
    [ml_structure]. *) 
 
@@ -57,13 +38,12 @@ let struct_iter do_decl do_spec s =
     | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
     | MTwith (mt,ML_With_type(idl,l,t))->
 	let mp_mt = msid_of_mt mt in
-      let mp = make_mp_with mp_mt idl in
-      let gr = ConstRef (
-	(make_con mp empty_dirpath
-	  (label_of_id ( 
-	    List.hd (List.rev idl))))) in
-	mt_iter mt;do_decl 
-	  (Dtype(gr,l,t))
+	let l',idl' = list_sep_last idl in
+	let mp_w =
+	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
+	in
+	let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in
+	mt_iter mt; do_decl (Dtype(r,l,t))
     | MTwith (mt,_)->mt_iter mt
     | MTsig (_, sign) -> List.iter spec_iter sign
   and spec_iter = function 
@@ -143,41 +123,6 @@ let spec_iter_references do_term do_cons do_type = function
   | 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 kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a }
-
-let struct_get_references empty add struc = 
-  let o = { typ = empty ; trm = empty ; cons = empty } in 
-  let do_type r = o.typ <- add r o.typ in 
-  let do_term r = o.trm <- add r o.trm in
-  let do_cons r = o.cons <- add r o.cons in 
-  struct_iter_references do_term do_cons do_type struc; o
-
-let struct_get_references_set = struct_get_references Refset.empty Refset.add
-
-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 
-  { typ = Orefset.list o.typ; 
-    trm = Orefset.list o.trm; 
-    cons = Orefset.list o.cons }
-
-
 (*s Searching occurrences of a particular term (no lifting done). *)
 
 exception Found
@@ -411,6 +356,7 @@ let optimize_struct to_appear struc =
   let opt_struc =
     List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
   in
+  let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in
   try
     if modular () then raise NoDepCheck;
     reset_needed ();
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index 85d58a4b..e279261d 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modutil.mli 10620 2008-03-05 10:54:41Z letouzey $ i*)
+(*i $Id: modutil.mli 11602 2008-11-18 00:08:33Z letouzey $ i*)
 
 open Names
 open Declarations
@@ -15,12 +15,6 @@ open Libnames
 open Miniml
 open Mod_subst
 
-(*s Functions upon modules missing in [Modops]. *) 
-
-(* Change a msid in a module type, to follow a module expr. *)
-
-val replicate_msid : struct_expr_body -> struct_expr_body -> struct_expr_body
-
 (*s Functions upon ML modules. *)
 
 val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
@@ -30,15 +24,11 @@ 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 kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a }
-
-val struct_get_references_set : ml_structure -> Refset.t kinds
-val struct_get_references_list : ml_structure -> global_reference list kinds
 
 val signature_of_structure : ml_structure -> ml_signature
 
+val msid_of_mt : ml_module_type -> module_path
+
 val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
 
 (* Some transformations of ML terms. [optimize_struct] simplify
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 64c80a2a..0166d854 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ocaml.ml 10592 2008-02-27 14:16:07Z letouzey $ i*)
+(*i $Id: ocaml.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
 
 (*s Production of Ocaml syntax. *)
 
@@ -25,22 +25,6 @@ open Declarations
 
 (*s Some utility functions. *)
 
-let rec  msid_of_mt = function
-  | MTident mp -> begin
-      match Modops.eval_struct (Global.env()) (SEBident mp) with
-	| SEBstruct(msid,_) -> MPself msid
-	| _ -> anomaly "Extraction:the With can't be applied to a funsig"
-    end
-  | MTwith(mt,_)-> msid_of_mt mt
-  | _ -> anomaly "Extraction:the With operator isn't applied to a name"
-
-let  make_mp_with mp idl =
-  let idl_rev = List.rev idl in
-  let idl' = List.rev (List.tl idl_rev) in
-    (List.fold_left (fun mp id -> MPdot(mp,label_of_id id))
-       mp idl')
-
-
 let pp_tvar id = 
   let s = string_of_id id in 
   if String.length s < 2 || s.[1]<>'\'' 
@@ -107,12 +91,18 @@ let sig_preamble _ used_modules usf =
 
 (*s The pretty-printer for Ocaml syntax*)
 
-let pp_global k r = 
-  if is_inline_custom r then str (find_custom r) 
+(* Beware of the side-effects of [pp_global] and [pp_modname].
+   They are used to update table of content for modules. Many [let] 
+   below should not be altered since they force evaluation order. 
+*)
+
+let pp_global k r =
+  if is_inline_custom r then str (find_custom r)
   else str (Common.pp_global k r)
 
 let pp_modname mp = str (Common.pp_module mp)
 
+
 let is_infix r = 
   is_inline_custom r && 
   (let s = find_custom r in 
@@ -462,7 +452,7 @@ let pp_ind co kn ind =
     if i >= Array.length ind.ind_packets then mt () 
     else 
       let ip = (kn,i) in 
-      let ip_equiv = ind.ind_equiv, 0 in 
+      let ip_equiv = ind.ind_equiv, i in 
       let p = ind.ind_packets.(i) in 
       if is_custom (IndRef ip) then pp (i+1)
       else begin 
@@ -607,52 +597,49 @@ and pp_module_type ol = function
   | MTident kn -> 
       pp_modname kn
   | MTfunsig (mbid, mt, mt') -> 
-      let name = pp_modname (MPbound mbid) in 
       let typ = pp_module_type None mt in 
+      let name = pp_modname (MPbound mbid) in 
       let def = pp_module_type None mt' in 
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MTsig (msid, sign) ->
-      let tvm = top_visible_mp () in 
-      Option.iter (fun l -> add_subst msid (MPdot (tvm, l))) ol; 
-      let mp = MPself msid in
-      push_visible mp; 
+      let tvm = top_visible_mp () in
+      let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
+      (* References in [sign] are in short form (relative to [msid]).
+	 In push_visible, [msid-->mp] is added to the current subst. *)
+      push_visible mp (Some msid);
       let l = map_succeed pp_specif sign in 
       pop_visible (); 
       str "sig " ++ fnl () ++ 
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
 	fnl () ++ str "end"
   | MTwith(mt,ML_With_type(idl,vl,typ)) ->
-      let l = rename_tvars keywords vl in 
-      let ids = pp_parameters l in 
+      let ids = pp_parameters (rename_tvars keywords vl) in
       let mp_mt = msid_of_mt mt in
-      let mp = make_mp_with mp_mt idl in
-      let gr = ConstRef (
-	(make_con mp empty_dirpath
-	  (label_of_id ( 
-	    List.hd (List.rev idl))))) in
-	push_visible mp_mt;
-	let s = pp_module_type None mt ++
-	  str " with type " ++
-	  pp_global Type gr ++
-	  ids in
-	  pop_visible();
-	  s ++ str "=" ++ spc () ++
-	  pp_type false  vl typ
+      let l,idl' = list_sep_last idl in
+      let mp_w =
+	List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
+      in
+      let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l))
+      in
+      push_visible mp_mt None;
+      let s =
+	pp_module_type None mt ++ str " with type " ++
+	  pp_global Type r ++ ids
+      in
+      pop_visible();
+      s ++ str "=" ++ spc () ++ pp_type false vl typ
   | MTwith(mt,ML_With_module(idl,mp)) ->
-      let mp_mt=msid_of_mt mt in
-	push_visible mp_mt;
-	let s = 
-	  pp_module_type None mt ++
-	    str " with module " ++
-	    (pp_modname
-	       (List.fold_left (fun mp id -> MPdot(mp,label_of_id id))
-		  mp_mt idl))
-	  ++ str " = "  
-	in
-	  pop_visible ();
-	  s ++ (pp_modname mp)
-	    
-	    
+      let mp_mt = msid_of_mt mt in
+      let mp_w =
+	List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl
+      in
+      push_visible mp_mt None;
+      let s =
+	pp_module_type None mt ++ str " with module " ++ pp_modname mp_w
+      in
+      pop_visible ();
+      s ++ str " = " ++ pp_modname mp
+
 let is_short = function MEident _ | MEapply _ -> true | _ -> false
   
 let rec pp_structure_elem = function 
@@ -664,10 +651,16 @@ let rec pp_structure_elem = function
 	 pp_alias_decl ren d 
 	with Not_found -> pp_decl d)
   | (l,SEmodule m) ->
+      let typ =
+        (* virtual printing of the type, in order to have a correct mli later*)
+	if Common.get_phase () = Pre then
+	  str ": " ++ pp_module_type (Some l) m.ml_mod_type
+	else mt ()
+      in
       let def = pp_module_expr (Some l) m.ml_mod_expr in 
       let name = pp_modname (MPdot (top_visible_mp (), l)) in 
       hov 1 
-	(str "module " ++ name ++ str " = " ++ 
+	(str "module " ++ name ++ typ ++ str " = " ++ 
 	 (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++ 
       (try 
 	 let ren = Common.check_duplicate (top_visible_mp ()) l in 
@@ -694,33 +687,34 @@ and pp_module_expr ol = function
   | MEstruct (msid, sel) -> 
       let tvm = top_visible_mp () in 
       let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in
-      push_visible mp; 
+      (* No need to update the subst with [Some msid] below : names are
+	 already in long form (see [subst_structure] in [Extract_env]). *)
+      push_visible mp None; 
       let l = map_succeed pp_structure_elem sel in 
       pop_visible (); 
       str "struct " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ 
       fnl () ++ str "end" 
 
-let pp_struct s =
-  let pp mp s = 
-    push_visible mp; 
-    let p = pp_structure_elem s ++ fnl2 () in 
-    pop_visible (); p
+let do_struct f s =
+  let pp s = try f s ++ fnl2 () with Failure "empty phrase" -> mt ()
   in
-  prlist_strict 
-    (fun (mp,sel) -> prlist_strict identity (map_succeed (pp mp) sel)) s
-
-let pp_signature s = 
-  let pp mp s = 
-    push_visible mp; 
-    let p = pp_specif s ++ fnl2 () in 
-    pop_visible (); p
-  in 
-  prlist_strict
-    (fun (mp,sign) -> prlist_strict identity (map_succeed (pp mp) sign)) s
+  let ppl (mp,sel) =
+    push_visible mp None;
+    let p = prlist_strict pp sel in
+    (* for monolithic extraction, we try to simulate the unavailability
+       of [MPfile] in names by artificially nesting these [MPfile] *)
+    (if modular () then pop_visible ()); p
+  in
+  let p = prlist_strict ppl s in
+  (if not (modular ()) then repeat (List.length s) pop_visible ());
+  p
+
+let pp_struct s = do_struct pp_structure_elem s
+
+let pp_signature s = do_struct pp_specif s
 
-let pp_decl d = 
-  try pp_decl d with Failure "empty phrase" -> mt ()
+let pp_decl d = try pp_decl d with Failure "empty phrase" -> mt ()
 
 let ocaml_descr = {
   keywords = keywords;  
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 600f64db..f4941a9c 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: scheme.ml 10233 2007-10-17 23:29:08Z letouzey $ i*)
+(*i $Id: scheme.ml 11559 2008-11-07 22:03:34Z letouzey $ i*)
 
 (*s Production of Scheme syntax. *)
 
@@ -183,7 +183,7 @@ let pp_structure_elem = function
 
 let pp_struct = 
   let pp_sel (mp,sel) = 
-    push_visible mp; 
+    push_visible mp None; 
     let p = prlist_strict pp_structure_elem sel in 
     pop_visible (); p
   in
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 10f669e1..c675a744 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.ml 11262 2008-07-24 20:59:29Z letouzey $ i*)
+(*i $Id: table.ml 11844 2009-01-22 16:45:06Z letouzey $ i*)
 
 open Names
 open Term
@@ -52,7 +52,7 @@ let is_modfile = function
   | MPfile _ -> true 
   | _ -> false
 
-let string_of_modfile = function 
+let raw_string_of_modfile = function
   | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
   | _ -> assert false
 
@@ -76,24 +76,15 @@ let rec prefixes_mp mp = match mp with
   | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp')
   | _ -> MPset.singleton mp 
 
-let rec get_nth_label_mp n mp = match mp with 
-  | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp 
+let rec get_nth_label_mp n = function
+  | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp
   | _ -> failwith "get_nth_label: not enough MPdot"
 
-let get_nth_label n r = 
-  if n=0 then label_of_r r else get_nth_label_mp n (modpath_of_r r)
-
-let rec common_prefix prefixes_mp1 mp2 = 
-  if MPset.mem mp2 prefixes_mp1 then mp2 
-  else match mp2 with 
-    | MPdot (mp,_) -> common_prefix prefixes_mp1 mp 
-    | _ -> raise Not_found
-
 let common_prefix_from_list mp0 mpl = 
-  let prefixes_mp0 = prefixes_mp mp0 in 
+  let prefixes = prefixes_mp mp0 in 
   let rec f = function 
     | [] -> raise Not_found
-    | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l
+    | mp :: l -> if MPset.mem mp prefixes then mp else f l 
   in f mpl
 
 let rec parse_labels ll = function 
@@ -185,39 +176,39 @@ let modular_ref = ref false
 let set_modular b = modular_ref := b
 let modular () = !modular_ref
 
-(*s Tables synchronization. *)
-
-let reset_tables () = 
-  init_terms (); init_types (); init_inductives (); init_recursors (); 
-  init_projs (); init_axioms ()
-
 (*s Printing. *)
 
 (* The following functions work even on objects not in [Global.env ()].
    WARNING: for inductive objects, an extract_inductive must have been 
    done before. *)
 
-let id_of_global = function 
+let safe_id_of_global = function 
   | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
   | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
   | ConstructRef ((kn,i),j) -> 
       (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
   | _ -> assert false
 
-let pr_global r = 
- try Printer.pr_global r 
- with _ -> pr_id (id_of_global r)
+let safe_pr_global r =
+ try Printer.pr_global r
+ with _ -> pr_id (safe_id_of_global r)
 
 (* idem, but with qualification, and only for constants. *)
 
-let pr_long_global r = 
-  try Printer.pr_global r 
+let safe_pr_long_global r =
+  try Printer.pr_global r
   with _ -> match r with
-    | ConstRef kn -> 
-	let mp,_,l = repr_con kn in 
+    | ConstRef kn ->
+	let mp,_,l = repr_con kn in
 	str ((string_of_mp mp)^"."^(string_of_label l))
     | _ -> assert false
 
+let pr_long_mp mp =
+  let lid = repr_dirpath (Nametab.dir_of_mp mp) in
+  str (String.concat "." (List.map string_of_id (List.rev lid)))
+
+let pr_long_global ref = pr_sp (Nametab.sp_of_global ref)
+
 (*S Warning and Error messages. *)
 
 let err s = errorlabstrm "Extraction" s
@@ -229,7 +220,7 @@ let warning_axioms () =
     let s = if List.length info_axioms = 1 then "axiom" else "axioms" in 
     msg_warning 
       (str ("The following "^s^" must be realized in the extracted code:")
-       ++ hov 1 (spc () ++ prlist_with_sep spc pr_global info_axioms) 
+       ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
        ++ str "." ++ fnl ())
   end;
   let log_axioms = Refset.elements !log_axioms in 
@@ -239,15 +230,27 @@ let warning_axioms () =
     in 
     msg_warning
       (str ("The following logical "^s^" encountered:") ++
-       hov 1 (spc () ++ prlist_with_sep spc pr_global log_axioms ++ str ".\n") ++
+       hov 1
+         (spc () ++ prlist_with_sep spc safe_pr_global log_axioms ++ str ".\n")
+       ++
        str "Having invalid logical axiom in the environment when extracting" ++
        spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
        fnl ())
   end
 
+let warning_both_mod_and_cst q mp r =
+ msg_warning
+   (str "The name " ++ pr_qualid q ++ str " is ambiguous, " ++
+    str "do you mean module " ++
+    pr_long_mp mp ++
+    str " or object " ++
+    pr_long_global r ++ str " ?" ++ fnl () ++
+    str "First choice is assumed, for the second one please use " ++
+    str "fully qualified name." ++ fnl ())
+
 let error_axiom_scheme r i = 
   err (str "The type scheme axiom " ++ spc () ++
-       pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ 
+       safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ 
        str " type variable(s).") 
 
 let check_inside_module () = 
@@ -265,10 +268,10 @@ let check_inside_section () =
 	 str "Close it and try again.")
 
 let error_constant r = 
-  err (pr_global r ++ str " is not a constant.") 
+  err (safe_pr_global r ++ str " is not a constant.") 
 
 let error_inductive r = 
-  err (pr_global r ++ spc () ++ str "is not an inductive type.")
+  err (safe_pr_global r ++ spc () ++ str "is not an inductive type.")
 
 let error_nb_cons () = 
   err (str "Not the right number of constructors.")
@@ -284,21 +287,21 @@ let error_scheme () =
   err (str "No Scheme modular extraction available yet.")
 
 let error_not_visible r = 
-  err (pr_global r ++ str " is not directly visible.\n" ++
+  err (safe_pr_global r ++ str " is not directly visible.\n" ++
        str "For example, it may be inside an applied functor." ++
        str "Use Recursive Extraction to get the whole environment.")
 
 let error_MPfile_as_mod mp b = 
   let s1 = if b then "asked" else "required" in 
   let s2 = if b then "extract some objects of this module or\n" else "" in
-  err (str ("Extraction of file "^(string_of_modfile mp)^
+  err (str ("Extraction of file "^(raw_string_of_modfile mp)^
 	    ".v as a module is "^s1^".\n"^
 	    "Monolithic Extraction cannot deal with this situation.\n"^
 	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
-let error_record r = 
-  err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++
-       str "To help extraction, please use an explicit name.") 
+let error_record r =
+  err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
+       fnl () ++ str "To help extraction, please use an explicit name.")
 
 let check_loaded_modfile mp = match base_mp mp with 
   | MPfile dp -> if not (Library.library_is_loaded dp) then 
@@ -481,11 +484,11 @@ let print_extraction_inline () =
     (str "Extraction Inline:" ++ fnl () ++ 
      Refset.fold
        (fun r p -> 
-	  (p ++ str "  " ++ pr_long_global r ++ fnl ())) i' (mt ()) ++
+	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) i' (mt ()) ++
      str "Extraction NoInline:" ++ fnl () ++ 
      Refset.fold
        (fun r p -> 
-	  (p ++ str "  " ++ pr_long_global r ++ fnl ())) n (mt ()))
+	  (p ++ str "  " ++ safe_pr_long_global r ++ fnl ())) n (mt ()))
 
 (* Reset part *)
 
@@ -498,6 +501,73 @@ let (reset_inline,_) =
 
 let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
+(*s Extraction Blacklist of filenames not to use while extracting *)
+
+let blacklist_table = ref Idset.empty
+
+let modfile_ids = ref []
+let modfile_mps = ref MPmap.empty
+
+let reset_modfile () =
+  modfile_ids := Idset.elements !blacklist_table;
+  modfile_mps := MPmap.empty
+
+let string_of_modfile mp =
+  try MPmap.find mp !modfile_mps
+  with Not_found ->
+    let id = id_of_string (raw_string_of_modfile mp) in
+    let id' = next_ident_away id !modfile_ids in
+    let s' = string_of_id id' in
+    modfile_ids := id' :: !modfile_ids;
+    modfile_mps := MPmap.add mp s' !modfile_mps;
+    s'
+
+let add_blacklist_entries l =
+  blacklist_table :=
+    List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s)))
+      l !blacklist_table
+
+(* Registration of operations for rollback. *)
+
+let (blacklist_extraction,_) =
+  declare_object
+    {(default_object "Extraction Blacklist") with
+       cache_function = (fun (_,l) -> add_blacklist_entries l);
+       load_function = (fun _ (_,l) -> add_blacklist_entries l);
+       export_function = (fun x -> Some x);
+       classify_function = (fun (_,o) -> Libobject.Keep o);
+       subst_function = (fun (_,_,x) -> x)
+    }
+
+let _ = declare_summary "Extraction Blacklist"
+	  { freeze_function = (fun () -> !blacklist_table);
+	    unfreeze_function = ((:=) blacklist_table);
+	    init_function = (fun () -> blacklist_table := Idset.empty);
+	    survive_module = true;
+	    survive_section = true }
+
+(* Grammar entries. *)
+
+let extraction_blacklist l =
+  let l = List.rev_map string_of_id l in
+  Lib.add_anonymous_leaf (blacklist_extraction l)
+
+(* Printing part *)
+
+let print_extraction_blacklist () =
+  msgnl
+    (prlist_with_sep fnl pr_id (Idset.elements !blacklist_table))
+
+(* Reset part *)
+
+let (reset_blacklist,_) =
+  declare_object
+    {(default_object "Reset Extraction Blacklist") with
+       cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
+       load_function = (fun _ (_,_)-> blacklist_table := Idset.empty);
+       export_function = (fun x -> Some x)}
+
+let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 
 (*s Extract Constant/Inductive. *)
 
@@ -575,3 +645,9 @@ let extract_inductive r (s,l) =
     | _ -> error_inductive g 
 
 
+
+(*s Tables synchronization. *)
+
+let reset_tables () =
+  init_terms (); init_types (); init_inductives (); init_recursors ();
+  init_projs (); init_axioms (); reset_modfile ()
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 4dbccd08..5ef7139e 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -6,20 +6,20 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.mli 11262 2008-07-24 20:59:29Z letouzey $ i*)
+(*i $Id: table.mli 11844 2009-01-22 16:45:06Z letouzey $ i*)
 
 open Names
 open Libnames
 open Miniml
 open Declarations
 
-val id_of_global : global_reference -> identifier
-val pr_long_global : global_reference -> Pp.std_ppcmds
-
+val safe_id_of_global : global_reference -> identifier
 
 (*s Warning and Error messages. *)
 
 val warning_axioms : unit -> unit
+val warning_both_mod_and_cst :
+ qualid -> module_path -> global_reference -> unit
 val error_axiom_scheme : global_reference -> int -> 'a
 val error_constant : global_reference -> 'a
 val error_inductive : global_reference -> 'a
@@ -55,7 +55,6 @@ val modfile_of_mp : module_path -> module_path
 val common_prefix_from_list : module_path -> module_path list -> module_path
 val add_labels_mp : module_path -> label list -> module_path
 val get_nth_label_mp : int -> module_path -> label
-val get_nth_label : int -> global_reference -> label
 val labels_of_ref : global_reference -> module_path * label list
 
 (*s Some table-related operations *)
@@ -142,6 +141,11 @@ val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
 val extract_inductive : reference -> string * string list -> unit
 
+(*s Table of blacklisted filenames *)
+
+val extraction_blacklist : identifier list -> unit
+val reset_extraction_blacklist : unit -> unit
+val print_extraction_blacklist : unit -> unit