1 files changed, 283 insertions, 327 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
+