Remaniement du pp, suite: vers un renommage modulaire correcte

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

12 files changed, 238 insertions, 269 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 0501f19b4a..abe2394148 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -16,68 +16,109 @@ open Table
 open Mlutil
 open Extraction
 open Ocaml
+open Lib
 open Libnames
 open Util
 open Declare
 open Nametab
 
-(*s Modules considerations *)
 
-let current_module = ref (id_of_string "")
+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 used_modules = ref []
+type updown = { mutable up : Orefset.t ; mutable down : Orefset.t }
 
-let long_module r = 
-  match modpath (kn_of_r r) with 
-    | MPfile d -> d
-    | _ -> anomaly "TODO: extraction not ready for true modules"
+let add_down r o = o.down <- Orefset.add r o.down
+let add_up r o = o.up <- Orefset.add r o.up
+let lang_add_type r o = if lang () = Haskell then add_up r o else add_down r o
 
-let short_module r = List.hd (repr_dirpath (long_module r))
-			    
-let check_ml r d = 
-  if to_inline r then 
-    try 
-      find_ml_extraction r 
-    with Not_found -> d
-  else d
+(*s Get all references used in one [ml_decl] list. *)
 
-(*s Get all modules names used in one [ml_decl] list. *)
+let mltype_get_references o t = 
+  let rec get_rec = function 
+    | Tglob (r,l) -> lang_add_type r o; List.iter get_rec l 
+    | Tarr (a,b) -> get_rec a; get_rec b 
+    | _ -> () 
+  in get_rec t
 
-let ast_get_modules m a = 
+let ast_get_references o a = 
   let rec get_rec a =
     ast_iter get_rec a;
     match a with 
-      | MLglob r -> m := Idset.add (short_module r) !m
-      | MLcons (r,l) as a -> 
-	  m := Idset.add (short_module r) !m; 
-      | MLcase (_,v) as a -> 
-	  let r,_,_ = v.(0) in
-	  m := Idset.add (short_module r) !m;
+      | MLglob r -> add_down r o
+      | MLcons (r,_) -> add_up r o
+      | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> add_up r o) v
+      | MLcast (_,t) -> mltype_get_references o t 
       | _ -> ()
   in get_rec a
 
-let mltype_get_modules m t = 
-  let rec get_rec = function 
-    | Tglob (r,l) -> m := Idset.add (short_module r) !m; List.iter get_rec l
-    | Tarr (a,b) -> get_rec a; get_rec b 
-    | _ -> () 
-  in get_rec t
-
-let decl_get_modules ld = 
-  let m = ref Idset.empty in 
+let decl_get_references ld = 
+  let o = { up = Orefset.empty ; down = Orefset.empty } in 
   let one_decl = function 
     | Dind (l,_) -> 
-	List.iter (fun (_,_,l) -> 
-		     List.iter (fun (_,l) -> 
-				  List.iter (mltype_get_modules m) l) l) l
-    | Dtype (_,_,t) -> mltype_get_modules m t 
-    | Dterm (_,a,t) -> ast_get_modules m a; mltype_get_modules m t
-    | Dfix(_,c,t) -> Array.iter (ast_get_modules m) c; 
-	Array.iter (mltype_get_modules m) t
-    | _ -> ()
+	List.iter (fun (_,r,l) -> 
+		     lang_add_type r o; 
+		     List.iter (fun (r,l) -> 
+				  add_up r o; 
+				  List.iter (mltype_get_references o) l) l) l
+    | Dtype (r,_,t) -> lang_add_type r o; mltype_get_references o t 
+    | Dterm (r,a,t) -> 
+	add_down r o; ast_get_references o a; mltype_get_references o t
+    | Dfix(rv,c,t) -> 
+	Array.iter (fun r -> add_down r o) rv; 
+	Array.iter (ast_get_references o) c; 
+	Array.iter (mltype_get_references o) t
+    | DcustomTerm (r,_) -> add_down r o
+    | DcustomType (r,_) -> lang_add_type r o
   in 
   List.iter one_decl ld; 
-  !m
+  o
+
+(*S Modules considerations. *)
+
+let long_module r = 
+  match modpath (kn_of_r r) with 
+    | MPfile d -> d
+    | _ -> anomaly "TODO: extraction not ready for true modules"
+
+let short_module r = List.hd (repr_dirpath (long_module r))
+
+(*s [extract_module m] returns all the global reference declared 
+  in a module. This is done by traversing the segment of module [m]. 
+  We just keep constants and inductives. *)
+
+let extract_module m =
+  let seg = Declaremods.module_objects (MPfile m) in
+  let get_reference = function
+    | (_,kn), Leaf o ->
+	(match Libobject.object_tag o with
+	   | "CONSTANT" | "PARAMETER" -> ConstRef kn
+	   | "INDUCTIVE" -> IndRef (kn,0)
+	   | _ -> failwith "caught")
+    | _ -> failwith "caught"
+  in
+  Util.map_succeed get_reference seg
+
+(*s The next function finds all names common to at least two used modules. *)
+
+let modules_reference_clashes modules = 
+  let id_of_r r = lowercase_id (id_of_global None r) in
+  let map = 
+    Dirset.fold
+      (fun mod_name map -> 
+	 let rl = List.map id_of_r (extract_module mod_name) in 
+	 List.fold_left (fun m id -> Idmap.add id (Idmap.mem id m) m) map rl)
+      modules Idmap.empty 
+  in Idmap.fold (fun i b s -> if b then Idset.add i s else s) map Idset.empty
+
+(*S Renamings. *)
 
 (*s Tables of global renamings *)
 
@@ -85,104 +126,105 @@ let keywords = ref Idset.empty
 let global_ids = ref Idset.empty
 
 let renamings = Hashtbl.create 97
-
-let cache r f =  
-  try Hashtbl.find renamings r 
-  with Not_found -> let id = f r in Hashtbl.add renamings r id; id 
-    
+let rename r s = Hashtbl.add renamings r s
+let get_renamings r = Hashtbl.find renamings r 
+
+let create_mono_renamings decls =  
+  let { up = u ; down = d } = decl_get_references decls in 
+  let add upper r = 
+    try if not (to_inline r) then raise Not_found; 
+      rename r (find_ml_extraction r)  
+    with Not_found -> 
+      let id = id_of_global None r in 
+      let id = if upper then uppercase_id id else lowercase_id id in
+      let id = rename_id id !global_ids in 
+      global_ids := Idset.add id !global_ids; 
+      rename r (string_of_id id)
+  in 
+  List.iter (add true) (List.rev (Orefset.list u)); 
+  List.iter (add false) (List.rev (Orefset.list d))
+
+let create_modular_renamings current_module decls = 
+  let { up = u ; down = d } = decl_get_references decls in 
+  let modules = 
+    let f r s = Dirset.add (long_module r) s in 
+    Refset.fold f (Orefset.set u) (Refset.fold f (Orefset.set d) Dirset.empty)
+  in 
+  let modular_clashs = modules_reference_clashes modules 
+  in 
+  let clash r id = 
+    exists_cci (make_path (dirpath (sp_of_global None r)) id)
+  in 
+  let prefix upper r id = 
+    let prefix = if upper then "Coq_" else "coq_" in 
+    let id' = if upper then uppercase_id id else lowercase_id id in
+    if (Idset.mem id' !keywords) || (id <> id' && clash r id') then 
+      id_of_string (prefix^(string_of_id id))
+    else id'
+  in
+  let add upper r = 
+    try if not (to_inline r) then raise Not_found; 
+      rename r (find_ml_extraction r)  
+    with Not_found -> 
+      let id = id_of_global None r in 
+      let m = short_module r in 
+      let id' = prefix upper r id in 
+      let qualify = 
+	(m <> current_module) && (Idset.mem (lowercase_id id) modular_clashs) 
+      in 
+      if qualify then 
+	let s = String.capitalize (string_of_id m) ^ "." ^ (string_of_id id') in
+	Hashtbl.add renamings r s
+      else begin
+	global_ids := Idset.add id' !global_ids;
+	Hashtbl.add renamings r (string_of_id id')
+      end
+  in
+  List.iter (add true) (List.rev (Orefset.list u)); 
+  List.iter (add false) (List.rev (Orefset.list d)); 
+  Idset.remove current_module 
+    (Dirset.fold (fun m s -> Idset.add (List.hd (repr_dirpath m)) s) 
+       modules Idset.empty)
+		    
 (*s Renaming issues at toplevel *)
 
 module ToplevelParams = struct
   let globals () = Idset.empty
-  let pp_global r _ _ = Printer.pr_global r
+  let pp_global r = Printer.pr_global r
 end
 
-(*s Renaming issues for a monolithic extraction. *)
-
-module MonoParams = struct
+(*s Renaming issues for a monolithic or modular extraction. *)
 
+module StdParams = struct
   let globals () = !global_ids
-		     
-  let rename_global_id id = 
-    let id' = rename_id id !global_ids in
-    global_ids := Idset.add id' !global_ids; 
-    id'
-
-  let rename_global r upper = 
-    cache r
-      (fun r -> 
-	 let id = id_of_global None r in
-	 rename_global_id (if upper then uppercase_id id else lowercase_id id))
-      
-  let pp_global r upper _ = 
-    str (check_ml r (string_of_id (rename_global r upper)))
-      
-end
-
-
-(*s Renaming issues in a modular extraction. *)
-
-module ModularParams = struct
-
-  let globals () = !global_ids 
-
-  let clash r id = 
-    exists_cci (make_path (dirpath (sp_of_global None r)) id)
-      
-  let rename_global_id r id id' prefix =
-    let id' = 
-      if (Idset.mem id' !keywords) || (id <> id' && clash r id') then 
-	id_of_string (prefix^(string_of_id id))
-      else id'
-    in 
-    if (short_module r) = !current_module then 
-      global_ids := Idset.add id' !global_ids; 
-    id'
-
-  let rename_global r upper =
-    cache r 
-      (fun r -> 
-	 let id = id_of_global None r in 
-	 if upper then
-	   rename_global_id r id (uppercase_id id) "Coq_"
-	 else rename_global_id r id (lowercase_id id) "coq_")
-
-  let qualify m id ctx = 
-    if m = !current_module then false
-    else if ctx = None then true 
-    else if Idset.mem id (out_some ctx) then true 
-    else false 
-      
-  let pp_global r upper ctx = 
-    let id = rename_global r upper in 
-    let m = short_module r in
-    let s = string_of_id id in 
-    let s = 
-      if qualify m id ctx then 
-	String.capitalize (string_of_id m) ^ "." ^ (string_of_id id)
-      else string_of_id id 
-    in str (check_ml r s)
-
+  let pp_global r = str (Hashtbl.find renamings r)
 end
 
 module ToplevelPp = Ocaml.Make(ToplevelParams)
-
-module OcamlMonoPp = Ocaml.Make(MonoParams)
-module OcamlModularPp = Ocaml.Make(ModularParams)
-
-module HaskellMonoPp = Haskell.Make(MonoParams)
-module HaskellModularPp = Haskell.Make(ModularParams)
-
-module SchemeMonoPp = Scheme.Make(MonoParams)
-
-let pp_decl modular = match lang(), modular with 
-    | Ocaml, false -> OcamlMonoPp.pp_decl
-    | Ocaml, _ -> OcamlModularPp.pp_decl
-    | Haskell, false -> HaskellMonoPp.pp_decl    
-    | Haskell, _ -> HaskellModularPp.pp_decl
-    | Scheme, _ -> SchemeMonoPp.pp_decl
-    | Toplevel, _ -> ToplevelPp.pp_decl
-
+module OcamlPp = Ocaml.Make(StdParams)
+module HaskellPp = Haskell.Make(StdParams)
+module SchemePp = Scheme.Make(StdParams)
+
+let pp_decl () = match lang () with 
+  | Ocaml -> OcamlPp.pp_decl
+  | Haskell -> HaskellPp.pp_decl
+  | Scheme -> SchemePp.pp_decl
+  | Toplevel -> ToplevelPp.pp_decl
+
+let set_keywords () =
+  (match lang () with 
+    | Ocaml -> keywords := Ocaml.keywords
+    | Haskell -> keywords := Haskell.keywords
+    | Scheme -> keywords := Scheme.keywords
+    | Toplevel -> keywords := Idset.empty);
+  global_ids := !keywords
+    
+let preamble prm = match lang () with 
+  | Ocaml -> Ocaml.preamble prm   
+  | Haskell -> Haskell.preamble prm
+  | Scheme -> Scheme.preamble prm
+  | Toplevel -> (fun _ _ -> mt ())
+	
 let pp_comment s = match lang () with 
   | Haskell -> str "-- " ++ s ++ fnl () 
   | Scheme -> str ";" ++ s ++ fnl () 
@@ -194,60 +236,42 @@ let pp_logical_ind r =
 let pp_singleton_ind r = 
   pp_comment (Printer.pr_global r ++ str " : singleton inductive constructor")
 
-let set_globals () = match lang () with 
-  | Ocaml -> 
-      keywords := Ocaml.keywords; 
-      global_ids := Ocaml.keywords
-  | Haskell -> 
-      keywords := Haskell.keywords;
-      global_ids := Haskell.keywords
-  | Scheme -> 
-      keywords := Scheme.keywords;
-      global_ids := Scheme.keywords
-  | _ -> ()
-
-(*s Extraction to a file. *)
+(*S Extraction to a file. *)
 
 let extract_to_file f prm decls =
-  set_globals ();
-  let preamble = match lang () with 
-    | Ocaml -> Ocaml.preamble    
-    | Haskell -> Haskell.preamble
-    | Scheme -> Scheme.preamble
-    | _ -> assert false 
-  in 
-  let pp_decl = pp_decl prm.modular in 
-  let print_dummys = 
-    (decl_search MLdummy decls, 
-     decl_type_search Tdummy decls, 
-     decl_type_search Tunknown decls) in 
   cons_cofix := Refset.empty;
-  current_module := prm.mod_name;
-  used_modules := if prm.modular then 
-    let set = (Idset.remove prm.mod_name (decl_get_modules decls))
-    in Idset.fold (fun m l -> m :: l) set [] 
-  else [];
   Hashtbl.clear renamings;
+  set_keywords ();
+  let used_modules = 
+    if lang () = Toplevel then Idset.empty 
+    else if prm.modular then
+      create_modular_renamings prm.mod_name decls
+    else begin create_mono_renamings decls; Idset.empty end
+  in 
+  let pp_decl = pp_decl () in 
   let cout = match f with 
     | None -> stdout
     | Some f -> open_out f in
   let ft = Pp_control.with_output_to cout in
-  pp_with ft (preamble prm !used_modules print_dummys);
-  if not prm.modular then 
+  let print_dummys = 
+    (decl_search MLdummy decls, 
+     decl_type_search Tdummy decls, 
+     decl_type_search Tunknown decls) in 
+  pp_with ft (preamble prm used_modules print_dummys);
+  if not prm.modular then begin 
     List.iter (fun r -> pp_with ft (pp_logical_ind r)) 
       (List.filter decl_is_logical_ind prm.to_appear); 
-  if not prm.modular then 
     List.iter (fun r -> pp_with ft (pp_singleton_ind r)) 
       (List.filter decl_is_singleton prm.to_appear); 
-  begin 
-    try
-      List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
-    with e ->
-      pp_flush_with ft (); if f <> None then close_out cout; raise e
+  end;
+  begin try
+    List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
+  with e ->
+    pp_flush_with ft (); if f <> None then close_out cout; raise e
   end;
   pp_flush_with ft ();
   if f <> None then close_out cout;  
-
+    
 (*i 
   (* DO NOT REMOVE: used when making names resolution *)
   let cout = open_out (f^".ren") in 
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index d831f00b78..1ae1e1a80e 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -16,13 +16,16 @@ open Libnames
 
 val long_module : global_reference -> dir_path
 
-val set_globals : unit -> unit
+val create_mono_renamings : ml_decl list -> unit
+val set_keywords : unit -> unit
 
 val pp_logical_ind : global_reference -> std_ppcmds
 
 val pp_singleton_ind : global_reference -> std_ppcmds
 
-val pp_decl : bool -> ml_decl -> std_ppcmds
+val pp_decl : unit -> ml_decl -> std_ppcmds
+
+val extract_module : dir_path -> global_reference list 
 
 val extract_to_file : 
   string option -> extraction_params -> ml_decl list -> unit
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index f286883e4e..28328fa8c7 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -26,9 +26,6 @@ open Declare
 
 (*s Auxiliary functions dealing with modules. *)
 
-module Dirset =
-  Set.Make(struct type t = dir_path let compare = compare end)
-
 let module_of_id m = 
   try 
     locate_loaded_library (make_short_qualid m) 
@@ -79,22 +76,6 @@ let check_modules m =
 	 let m' = Idmap.find idm !map in clash_error sm m m'
        with Not_found -> map := Idmap.add idm m !map) m
     
-(*s [extract_module m] returns all the global reference declared 
-  in a module. This is done by traversing the segment of module [m]. 
-  We just keep constants and inductives. *)
-
-let extract_module m =
-  let seg = Declaremods.module_objects (MPfile m) in
-  let get_reference = function
-    | (_,kn), Leaf o ->
-	(match Libobject.object_tag o with
-	   | "CONSTANT" | "PARAMETER" -> ConstRef kn
-	   | "INDUCTIVE" -> IndRef (kn,0)
-	   | _ -> failwith "caught")
-    | _ -> failwith "caught"
-  in
-  Util.map_succeed get_reference seg
-
 (*s Recursive computation of the global references to extract. 
     We use a set of functions visiting the extracted objects in
     a depth-first way ([visit_type], [visit_ast] and [visit_decl]).
@@ -225,12 +206,13 @@ let extraction qid =
   else 
     let prm = 
       { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in 
-    set_globals ();
     let decls = optimize prm (decl_of_refs [r]) in 
     let d = list_last decls in
     let d = if (decl_in_r r d) then d 
-    else List.find (decl_in_r r) decls
-    in msgnl (pp_decl false d)
+    else List.find (decl_in_r r) decls in 
+    set_keywords ();
+    create_mono_renamings decls; 
+    msgnl (pp_decl () d)
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
     \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env]
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index aac1374d1c..07e6fdbe2f 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -35,9 +35,8 @@ let preamble prm used_modules (mldummy,tdummy,tunknown) =
   let m = String.capitalize (string_of_id prm.mod_name)   in 
   str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ 
   str "import qualified Prelude" ++ fnl() ++
-  List.fold_right
-    (fun m s -> 
-       str "import qualified " ++ pr_id (uppercase_id m) ++ fnl() ++ s)
+  Idset.fold
+    (fun m s -> str "import qualified " ++ pr_id (uppercase_id m) ++ fnl() ++ s)
     used_modules (mt ()) ++ fnl()
   ++
   (if mldummy then 
@@ -57,9 +56,7 @@ let pr_lower_id id = pr_id (lowercase_id id)
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_global r = P.pp_global r false None
-let pp_global_up r = P.pp_global r true None
-
+let pp_global r = P.pp_global r
 let empty_env () = [], P.globals()
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
@@ -69,10 +66,10 @@ let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ -> assert false 
     | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
-    | Tglob (r,[]) -> pp_global_up r	
+    | Tglob (r,[]) -> pp_global r	
     | Tglob (r,l) -> 
 	pp_par par 
-	  (pp_global_up r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l)
+	  (pp_global r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l)
     | Tarr (t1,t2) ->
 	pp_par par 
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
@@ -121,13 +118,13 @@ let rec pp_expr par env args =
     | MLglob r -> 
 	apply (pp_global r)
     | MLcons (r,[]) ->
-	assert (args=[]); pp_global_up r
+	assert (args=[]); pp_global r
     | MLcons (r,[a]) ->
 	assert (args=[]);
-	pp_par par (pp_global_up r ++ spc () ++ pp_expr true env [] a)
+	pp_par par (pp_global r ++ spc () ++ pp_expr true env [] a)
     | MLcons (r,args') ->
 	assert (args=[]);
-	pp_par par (pp_global_up r ++ spc () ++ 
+	pp_par par (pp_global r ++ spc () ++ 
 		    prlist_with_sep spc (pp_expr true env []) args')
     | MLcase (t, pv) ->
       	apply (pp_par par' 
@@ -148,7 +145,7 @@ and pp_pat env pv =
   let pp_one_pat (name,ids,t) =
     let ids,env' = push_vars (List.rev ids) env in
     let par = expr_needs_par t in
-    hov 2 (pp_global_up name ++
+    hov 2 (pp_global name ++
 	   (match ids with 
 	      | [] -> mt ()
 	      | _  -> (str " " ++ 
@@ -183,7 +180,7 @@ and pp_function env f t =
 let pp_one_inductive (pl,name,cl) =
   let pl = rename_tvars keywords pl in
   let pp_constructor (r,l) =
-    (pp_global_up r ++
+    (pp_global r ++
      match l with
        | [] -> (mt ()) 
        | _  -> (str " " ++
@@ -191,7 +188,7 @@ let pp_one_inductive (pl,name,cl) =
 		  (fun () -> (str " ")) (pp_type true (List.rev pl)) l))
   in
   (str (if cl = [] then "type " else "data ") ++ 
-   pp_global_up name ++ str " " ++
+   pp_global name ++ str " " ++
    prlist_with_sep (fun () -> (str " ")) pr_lower_id pl ++
    (if pl = [] then (mt ()) else (str " ")) ++
    if cl = [] then str "= () -- empty inductive"
@@ -212,7 +209,7 @@ let pp_decl = function
   | Dtype (r, l, t) ->
       let l = rename_tvars keywords l in
       let l' = List.rev l in 
-      hov 0 (str "type " ++ pp_global_up r ++ spc () ++ 
+      hov 0 (str "type " ++ pp_global r ++ spc () ++ 
 	       prlist_with_sep (fun () -> (str " ")) pr_id l ++
 	       (if l <> [] then (str " ") else (mt ())) ++ str "=" ++ spc () ++
 	       pp_type false l' t ++ fnl ())
@@ -226,7 +223,7 @@ let pp_decl = function
   | DcustomTerm (r,s) -> 
       hov 0  (pp_global r ++ str " =" ++ spc () ++ str s ++ fnl ())
   | DcustomType (r,s) -> 
-      hov 0  (str "type " ++ pp_global_up r ++ str " = " ++ str s ++ fnl ())
+      hov 0  (str "type " ++ pp_global r ++ str " = " ++ str s ++ fnl ())
 
 end
 
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 00f09cb145..8a0deeca6c 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -15,7 +15,6 @@ open Miniml
 
 val keywords : Idset.t
 
-val preamble : 
-  extraction_params -> identifier list -> bool * bool * bool -> std_ppcmds
+val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 62960af7cc..63bceae5ef 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -77,9 +77,7 @@ type extraction_params =
 
 module type Mlpp_param = sig
   val globals : unit -> Idset.t
-      (* the bool arg is: should we rename in uppercase or not ? *)
-      (* the identifier set correspond to local bindings to avoid. *)
-  val pp_global : global_reference -> bool -> Idset.t option -> std_ppcmds
+  val pp_global : global_reference -> std_ppcmds
 end
 
 module type Mlpp = sig
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index d5bfd32c45..582dbd2abc 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -22,8 +22,6 @@ open Options
 open Nametab
 open Libnames
 
-let current_module = ref None
-
 let cons_cofix = ref Refset.empty
 
 (*s Some utility functions. *)
@@ -125,11 +123,10 @@ let keywords =
   Idset.empty
 
 let preamble _ used_modules (mldummy,tdummy,tunknown) = 
-  List.fold_right
-    (fun m s -> str "open " ++ pr_id (uppercase_id m) ++ fnl () ++ s)
+  Idset.fold (fun m s -> str "open " ++ pr_id (uppercase_id m) ++ fnl() ++ s)
     used_modules (mt ())
   ++ 
-  (if used_modules = [] then mt () else fnl ())
+  (if Idset.is_empty used_modules then mt () else fnl ())
   ++
   (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() else mt()) 
   ++
@@ -145,15 +142,7 @@ let preamble _ used_modules (mldummy,tdummy,tunknown) =
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_global r = P.pp_global r false None
-
-let pp_global_ctx r env = P.pp_global r false (Some (snd env))
-let pp_global_ctx2 r = P.pp_global r false (Some (P.globals ()))
-
-let pp_global_up r = P.pp_global r true None
-let pp_global_up_ctx r env = P.pp_global r true (Some (snd env))
-
-
+let pp_global r = P.pp_global r
 let empty_env () = [], P.globals()
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
@@ -164,8 +153,8 @@ let rec pp_type par vl t =
     | Tmeta _ | Tvar' _ -> assert false
     | Tvar i -> (try pp_tvar (List.nth vl (pred i)) 
 		 with _ -> (str "'a" ++ int i))
-    | Tglob (r,[]) -> pp_global_ctx2 r
-    | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global_ctx2 r
+    | Tglob (r,[]) -> pp_global r
+    | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global r
     | Tarr (t1,t2) ->
 	pp_par par 
 	  (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
@@ -214,26 +203,24 @@ let rec pp_expr par env args =
 	      spc () ++ hov 0 pp_a2))
     | MLglob r when is_proj r && args <> [] ->
 	let record = List.hd args in 
-	pp_apply (record ++ str "." ++ pp_global_ctx2 r) par (List.tl args)
+	pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
     | MLglob r -> 
-	apply (pp_global_ctx r env )
+	apply (pp_global r)
     | MLcons (r,[]) ->
 	assert (args=[]);
-	let cons = pp_global_up_ctx r env in 
 	if Refset.mem r !cons_cofix then 
-	  pp_par par (str "lazy " ++ cons)
-	else cons 
+	  pp_par par (str "lazy " ++ pp_global r)
+	else pp_global r
     | MLcons (r,args') -> 
 	(try 
 	   let projs = find_proj (kn_of_r r, 0) in 
 	   pp_record (projs, List.map (pp_expr true env []) args')
 	 with Not_found ->
 	   assert (args=[]);
-	   let cons = pp_global_up_ctx r env
-	   and tuple = pp_tuple (pp_expr true env []) args' in 
+	   let tuple = pp_tuple (pp_expr true env []) args' in 
 	   if Refset.mem r !cons_cofix then 
-	     pp_par par (str "lazy (" ++ cons ++ spc () ++ tuple ++ str ")")
-	   else pp_par par (cons ++ spc () ++ tuple))
+	     pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++ str ")")
+	   else pp_par par (pp_global r ++ spc () ++ tuple))
     | MLcase (t, pv) ->
 	let r,_,_ = pv.(0) in 
 	let expr = if Refset.mem r !cons_cofix then 
@@ -276,8 +263,7 @@ let rec pp_expr par env args =
 and pp_record (projs, args) =
    str "{ " ++
    prlist_with_sep (fun () -> str ";" ++ spc ()) 
-     (fun (r,a) -> 
-	pp_global_ctx2 r ++ str " =" ++ spc () ++ a)
+     (fun (r,a) -> pp_global r ++ str " =" ++ spc () ++ a)
      (List.combine projs args) ++
    str " }"
 
@@ -291,7 +277,7 @@ and pp_one_pat env (r,ids,t) =
     let args = 
       if ids = [] then (mt ()) 
       else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in 
-    pp_global_up_ctx r env ++ args, expr
+    pp_global r ++ args, expr
   
 and pp_pat env pv = 
   prvect_with_sep (fun () -> (fnl () ++ str "  | ")) 
@@ -359,7 +345,7 @@ let pp_parameters l =
 let pp_one_ind prefix (pl,name,cl) =
   let pl = rename_tvars keywords pl in
   let pp_constructor (r,l) =
-    (pp_global_up r ++
+    (pp_global r ++
      match l with
        | [] -> (mt ()) 
        | _  -> (str " of " ++
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 1984472967..41b370a503 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -14,10 +14,9 @@ open Pp
 open Miniml
 open Names
 open Term
+open Libnames
 open Nametab
-open Table
 
-val current_module : identifier option ref
 val cons_cofix : Refset.t ref
 
 val pp_par : bool -> std_ppcmds -> std_ppcmds
@@ -39,8 +38,7 @@ val get_db_name : int -> env -> identifier
 
 val keywords : Idset.t
 
-val preamble : 
-  extraction_params -> identifier list -> bool * bool * bool -> std_ppcmds
+val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
 
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some 
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 55a30185da..d74cb22641 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -19,6 +19,7 @@ open Miniml
 open Table
 open Mlutil
 open Options
+open Libnames
 open Nametab
 open Ocaml
 
@@ -49,11 +50,7 @@ let pp_abst st = function
 
 module Make = functor(P : Mlpp_param) -> struct
 
-let pp_global r = P.pp_global r false None
-let pp_global_ctx r env = P.pp_global r false (Some (snd env))
-let pp_global_up r = P.pp_global r true None
-let pp_global_up_ctx r env = P.pp_global r true (Some (snd env))
-
+let pp_global r = P.pp_global r
 let empty_env () = [], P.globals()
 
 (*s Pretty-printing of expressions.  *)
@@ -82,12 +79,12 @@ let rec pp_expr env args =
 			 (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) 
 		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
     | MLglob r -> 
-	apply (pp_global_ctx r env)
+	apply (pp_global r)
     | MLcons (r,args') ->
 	assert (args=[]);
 	let st = 
 	  str "`" ++ 
-	  paren (pp_global_up_ctx r env ++ 
+	  paren (pp_global r ++ 
 		 (if args' = [] then mt () else (spc () ++ str ",")) ++
 		 prlist_with_sep 
 		   (fun () -> spc () ++ str ",") 
@@ -125,7 +122,7 @@ and pp_one_pat env (r,ids,t) =
     if ids = [] then mt () 
     else (str " " ++ prlist_with_sep spc pp_arg (List.rev ids))
   in 
-  (pp_global_up_ctx r env ++ args), (pp_expr env' [] t)
+  (pp_global r ++ args), (pp_expr env' [] t)
   
 and pp_pat env pv = 
   prvect_with_sep fnl  
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index f39afd34f0..51fac4fb72 100644
--- a/contrib/extraction/scheme.mli
+++ b/contrib/extraction/scheme.mli
@@ -17,8 +17,7 @@ open Nametab
 
 val keywords : Idset.t
 
-val preamble : 
-  extraction_params -> identifier list -> bool * bool * bool -> std_ppcmds
+val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index a0dde32b7b..21e4debe40 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -69,15 +69,6 @@ let _ = declare_bool_option
 	   optread = optim; 
 	   optwrite = (:=) optim_ref}
 
-
-(*s Set and Map over global reference *)
-
-module Refset = 
-  Set.Make(struct type t = global_reference let compare = compare end)
-
-module Refmap = 
-  Map.Make(struct type t = global_reference let compare = compare end)
-
 (*s Auxiliary functions *) 
 
 let is_constant r = match r with 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index d8b17f5d56..7afb6782d1 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -29,11 +29,6 @@ val auto_inline : unit -> bool
 
 val optim :  unit -> bool
 
-(*s Set and Map over global reference *) 
-
-module Refset : Set.S with type elt = global_reference
-module Refmap : Map.S with type key = global_reference
-
 (*s Target language. *)
 
 type lang = Ocaml | Haskell | Scheme | Toplevel