 +           in prf ^ str
 +
 +
-+(* Main name printing function for a reference *)
-+
-+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,_,l = repr_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_visible (k,s) l; unquote s)
-+  else
-+    let rls = List.rev ls in (* for what come next it's easier this way *)
-+    match lang () with
-+      | Scheme -> unquote s (* no modular Scheme extraction... *)
-+      | Haskell -> if modular () then pp_haskell_gen k mp rls else s
+ (* Main name printing function for a reference *)
+ 
+ let pp_global k r =
+@@ -568,6 +585,7 @@
+     match lang () with
+       | Scheme -> unquote s (* no modular Scheme extraction... *)
+       | Haskell -> if modular () then pp_haskell_gen k mp rls else s
 +      | CoreErlang -> if modular () then pp_coreerlang_gen k mp rls else s
-+      | Ocaml -> pp_ocaml_gen k mp rls (Some l)
-+
-+(* The next function is used only in Ocaml extraction...*)
-+
-+let pp_module mp =
-+  let ls = mp_renaming mp in
-+  match mp with
-+    | MPdot (mp0,l) 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_visible (Mod,s) l; s
-+    | _ -> pp_ocaml_gen Mod mp (List.rev ls) None
-+
-+(** Special hack for constants of type Ascii.ascii : if an
-+    [Extract Inductive ascii => char] has been declared, then
-+    the constants are directly turned into chars *)
-+
-+let mk_ind path s =
-+  make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)
-+
-+let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
-+
-+let check_extract_ascii () =
-+  try
-+    let char_type = match lang () with
-+      | Ocaml -> "char"
-+      | Haskell -> "Char"
+       | Ocaml -> pp_ocaml_gen k mp rls (Some l)
+ 
+ (* The next function is used only in Ocaml extraction...*)
+@@ -596,6 +614,7 @@
+     let char_type = match lang () with
+       | Ocaml -> "char"
+       | Haskell -> "Char"
 +      | CoreErlang -> "char"
-+      | _ -> raise Not_found
-+    in
-+    find_custom (IndRef (ind_ascii,0)) = char_type
-+  with Not_found -> false
-+
-+let is_list_cons l =
-+ List.for_all (function MLcons (_,ConstructRef(_,_),[]) -> true | _ -> false) l
-+
-+let is_native_char = function
-+  | MLcons(_,ConstructRef ((kn,0),1),l) ->
-+    kn = ind_ascii && check_extract_ascii () && is_list_cons l
-+  | _ -> false
-+
-+let pp_native_char c =
-+  let rec cumul = function
-+    | [] -> 0
-+    | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
-+    | _ -> assert false
-+  in
-+  let l = match c with MLcons(_,_,l) -> l | _ -> assert false in
-+  str ("'"^Char.escaped (Char.chr (cumul l))^"'")
-diff -aurN coq-8.4pl2-pristine/plugins/extraction/coreerlang.ml coq-8.4pl2-new/plugins/extraction/coreerlang.ml
---- coq-8.4pl2-pristine/plugins/extraction/coreerlang.ml	1969-12-31 16:00:00.000000000 -0800
-+++ coq-8.4pl2-new/plugins/extraction/coreerlang.ml	2013-07-15 08:44:39.412126738 -0700
+       | _ -> raise Not_found
+     in
+     find_custom (IndRef (ind_ascii,0)) = char_type
+diff -aurN coq-8.4pl2/plugins/extraction/coreerlang.ml coq-8.4pl2-new/plugins/extraction/coreerlang.ml
+--- coq-8.4pl2/plugins/extraction/coreerlang.ml	1969-12-31 16:00:00.000000000 -0800
++++ coq-8.4pl2-new/plugins/extraction/coreerlang.ml	2013-07-21 08:18:44.066225784 -0700
 @@ -0,0 +1,1324 @@
 +open Pp
 +open Util

diff -aurN coq-8.4pl2-pristine/ide/coq_lex.mll coq-8.4pl2-new/ide/coq_lex.mll
--- coq-8.4pl2-pristine/ide/coq_lex.mll	1969-12-31 16:00:00.000000000 -0800
+++ coq-8.4pl2-new/ide/coq_lex.mll	2013-06-03 04:29:10.207721636 -0700
@@ -0,0 +1,195 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+{
+  open Lexing
+
+  type token =
+    | Comment
+    | Keyword
+    | Declaration
+    | ProofDeclaration
+    | Qed
+    | String
+
+  (* Without this table, the automaton would be too big and
+     ocamllex would fail *)
+
+  let tag_of_ident =
+    let one_word_commands =
+      [ "Add" ; "Check"; "Eval"; "Extraction" ;
+	"Load" ; "Undo"; "Goal";
+	"Proof" ; "Print";"Save" ; "Restart";
+	"End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ]
+    in
+    let one_word_declarations =
+      [ (* Definitions *)
+	"Definition" ; "Let" ; "Example" ; "SubClass" ;
+        "Fixpoint" ; "CoFixpoint" ; "Scheme" ; "Function" ;
+        (* Assumptions *)
+	"Hypothesis" ; "Variable" ; "Axiom" ; "Parameter" ; "Conjecture" ;
+	"Hypotheses" ; "Variables" ; "Axioms" ; "Parameters";
+        (* Inductive *)
+        "Inductive" ; "CoInductive" ; "Record" ; "Structure" ;
+        (* Other *)
+	"Ltac" ; "Instance"; "Include"; "Context"; "Class" ;
+	 "Arguments" ]
+    in
+    let proof_declarations =
+      [ "Theorem" ; "Lemma" ; " Fact" ; "Remark" ; "Corollary" ;
+        "Proposition" ; "Property" ]
+    in
+    let proof_ends =
+      [ "Qed" ; "Defined" ; "Admitted"; "Abort" ]
+    in
+    let constr_keywords =
+      [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "for";
+	"end"; "as"; "let"; "in"; "if"; "then"; "else"; "return";
+	"Prop"; "Set"; "Type" ]
+    in
+    let h = Hashtbl.create 97 in (* for vernac *)
+    let h' = Hashtbl.create 97 in (* for constr *)
+    List.iter (fun s -> Hashtbl.add h s Keyword) one_word_commands;
+    List.iter (fun s -> Hashtbl.add h s Declaration) one_word_declarations;
+    List.iter (fun s -> Hashtbl.add h s ProofDeclaration) proof_declarations;
+    List.iter (fun s -> Hashtbl.add h s Qed) proof_ends;
+    List.iter (fun s -> Hashtbl.add h' s Keyword) constr_keywords;
+    (fun initial id -> Hashtbl.find (if initial then h else h') id)
+
+  exception Unterminated
+
+  let here f lexbuf = f (Lexing.lexeme_start lexbuf) (Lexing.lexeme_end lexbuf)
+
+}
+
+let space =
+  [' ' '\n' '\r' '\t' '\012'] (* '\012' is form-feed *)
+
+let firstchar =
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
+let identchar =
+  ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' '\'' '0'-'9']
+let ident = firstchar identchar*
+
+let undotted_sep = [ '{' '}' '-' '+' '*' ]
+
+let dot_sep = '.' (space | eof)
+
+let multiword_declaration =
+  "Module" (space+ "Type")?
+| "Program" space+ ident
+| "Existing" space+ "Instance" "s"?
+| "Canonical" space+ "Structure"
+
+let locality = (space+ "Local")?
+
+let multiword_command =
+  ("Uns" | "S")" et" (space+ ident)*
+| (("Open" | "Close") locality | "Bind" | " Delimit" )
+    space+ "Scope"
+| (("Reserved" space+)? "Notation" | "Infix") locality space+
+| "Next" space+ "Obligation"
+| "Solve" space+ "Obligations"
+| "Require" space+ ("Import"|"Export")?
+| "Hint" locality space+ ident
+| "Reset" (space+ "Initial")?
+| "Tactic" space+ "Notation"
+| "Implicit" space+ "Type" "s"?
+| "Combined" space+ "Scheme"
+| "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"|"CoreErlang"|"Toplevel"))|
+    ("Library"|"Inline"|"NoInline"|"Blacklist"))
+| "Recursive" space+ "Extraction" (space+ "Library")?
+| ("Print"|"Reset") space+ "Extraction" space+ ("Inline"|"Blacklist")
+| "Extract" space+ (("Inlined" space+) "Constant"| "Inductive")
+| "Typeclasses" space+ ("eauto" | "Transparent" | "Opaque")
+| ("Generalizable" space+) ("All" | "No")? "Variable" "s"?
+
+(* At least still missing: "Inline" + decl, variants of "Identity
+  Coercion", variants of Print, Add, ... *)
+
+rule coq_string = parse
+  | "\"\"" { coq_string lexbuf }
+  | "\"" { Lexing.lexeme_end lexbuf }
+  | eof { Lexing.lexeme_end lexbuf }
+  | _ { coq_string lexbuf }
+
+and comment = parse
+  | "(*" { ignore (comment lexbuf); comment lexbuf }
+  | "\"" { ignore (coq_string lexbuf); comment lexbuf }
+  | "*)" { (true, Lexing.lexeme_start lexbuf + 2) }
+  | eof { (false, Lexing.lexeme_end lexbuf) }
+  | _ { comment lexbuf }
+
+and sentence initial stamp = parse
+  | "(*" {
+      let comm_start = Lexing.lexeme_start lexbuf in
+      let trully_terminated,comm_end = comment lexbuf in
+      stamp comm_start comm_end Comment;
+      if not trully_terminated then raise Unterminated;
+      (* A comment alone is a sentence.
+	 A comment in a sentence doesn't terminate the sentence.
+         Note: comm_end is the first position _after_ the comment,
+	 as required when tagging a zone, hence the -1 to locate the
+	 ")" terminating the comment.
+      *)
+      if initial then comm_end - 1 else sentence false stamp lexbuf
+    }
+  | "\"" {
+      let str_start = Lexing.lexeme_start lexbuf in
+      let str_end = coq_string lexbuf in
+      stamp str_start str_end String;
+      sentence false stamp lexbuf
+    }
+  | multiword_declaration {
+      if initial then here stamp lexbuf Declaration;
+      sentence false stamp lexbuf
+    }
+  | multiword_command {
+      if initial then here stamp lexbuf Keyword;
+      sentence false stamp lexbuf
+    }
+  | ident as id {
+      (try here stamp lexbuf (tag_of_ident initial id) with Not_found -> ());
+      sentence false stamp lexbuf }
+  | ".." {
+      (* We must have a particular rule for parsing "..", where no dot
+	 is a terminator, even if we have a blank afterwards
+	 (cf. for instance the syntax for recursive notation).
+	 This rule and the following one also allow to treat the "..."
+	 special case, where the third dot is a terminator. *)
+      sentence false stamp lexbuf
+    }
+  | dot_sep { Lexing.lexeme_start lexbuf } (* The usual "." terminator *)
+  | undotted_sep {
+      (* Separators like { or } and bullets * - + are only active
+	 at the start of a sentence *)
+      if initial then Lexing.lexeme_start lexbuf
+      else sentence false stamp lexbuf
+    }
+  | space+ {
+       (* Parsing spaces is the only situation preserving initiality *)
+       sentence initial stamp lexbuf
+    }
+  | _ {
+      (* Any other characters *)
+      sentence false stamp lexbuf
+    }
+  | eof { raise Unterminated }
+
+{
+
+  (** Parse a sentence in string [slice], tagging relevant parts with
+      function [stamp], and returning the position of the first
+      sentence delimitor (either "." or "{" or "}" or the end of a comment).
+      It will raise [Unterminated] when no end of sentence is found.
+  *)
+
+  let delimit_sentence stamp slice =
+    sentence true stamp (Lexing.from_string slice)
+
+}
diff -aurN coq-8.4pl2-pristine/plugins/extraction/common.ml coq-8.4pl2-new/plugins/extraction/common.ml
--- coq-8.4pl2-pristine/plugins/extraction/common.ml	1969-12-31 16:00:00.000000000 -0800
+++ coq-8.4pl2-new/plugins/extraction/common.ml	2013-07-15 08:44:39.408126738 -0700
@@ -0,0 +1,638 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Pp
+open Util
+open Names
+open Term
+open Declarations
+open Namegen
+open Nameops
+open Libnames
+open Table
+open Miniml
+open Mlutil
+open Modutil
+open Mod_subst
+
+let string_of_id id =
+  let s = Names.string_of_id id in
+  for i = 0 to String.length s - 2 do
+    if s.[i] = '_' && s.[i+1] = '_' then warning_id s
+  done;
+  ascii_of_ident s
+
+let is_mp_bound = function MPbound _ -> true | _ -> false
+
+(*s Some pretty-print utility functions. *)
+
+let pp_par par st = if par then str "(" ++ st ++ str ")" else st
+
+(** [pp_apply] : a head part applied to arguments, possibly with parenthesis *)
+
+let pp_apply st par args = match args with
+  | [] -> st
+  | _  -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
+
+(** Same as [pp_apply], but with also protection of the head by parenthesis *)
+
+let pp_apply2 st par args =
+  let par' = args <> [] || par in
+  pp_apply (pp_par par' st) par args
+
+let pr_binding = function
+  | [] -> mt ()
+  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
+
+let pp_tuple_light f = function
+  | [] -> mt ()
+  | [x] -> f true x
+  | l ->
+      pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l)
+
+let pp_tuple f = function
+  | [] -> mt ()
+  | [x] -> f x
+  | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l)
+
+let pp_boxed_tuple f = function
+  | [] -> mt ()
+  | [x] -> f x
+  | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
+
+(** By default, in module Format, you can do horizontal placing of blocks
+    even if they include newlines, as long as the number of chars in the
+    blocks is less that a line length. To avoid this awkward situation,
+    we attach a big virtual size to [fnl] newlines. *)
+
+let fnl () = stras (1000000,"") ++ fnl ()
+
+let fnl2 () = fnl () ++ fnl ()
+
+let space_if = function true -> str " " | false -> mt ()
+
+let is_digit = function
+  | '0'..'9' -> true
+  | _ -> false
+
+let begins_with_CoqXX s =
+  let n = String.length s in
+  n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' &&
+  let i = ref 3 in
+  try while !i < n do
+    if s.[!i] = '_' then i:=n (*Stop*)
+    else if is_digit s.[!i] then incr i
+    else raise Not_found
+  done; true
+  with Not_found -> false
+
+let unquote s =
+  if lang () <> Scheme then s
+  else
+    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 qualify delim = function
+  | [] -> assert false
+  | [s] -> s
+  | ""::l -> qualify delim l
+  | s::l -> s^delim^(qualify delim l)
+
+let dottify = qualify "."
+let pseudo_qualify = qualify "__"
+
+(*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
+
+let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
+let uppercase_id id =
+  let s = string_of_id id in
+  assert (s<>"");
+  if s.[0] = '_' then id_of_string ("Coq_"^s)
+  else id_of_string (String.capitalize s)
+
+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 *)
+
+type env = identifier list * Idset.t
+
+(*s Generic renaming issues for local variable names. *)
+
+let rec rename_id id avoid =
+  if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id
+
+let rec rename_vars avoid = function
+  | [] ->
+      [], avoid
+  | id :: idl when id == dummy_name ->
+      (* we don't rename dummy binders *)
+      let (idl', avoid') = rename_vars avoid idl in
+      (id :: idl', avoid')
+  | id :: idl ->
+      let (idl, avoid) = rename_vars avoid idl in
+      let id = rename_id (lowercase_id id) avoid in
+      (id :: idl, Idset.add id avoid)
+
+let rename_tvars avoid l =
+  let rec rename avoid = function
+    | [] -> [],avoid
+    | id :: idl ->
+	let id = rename_id (lowercase_id id) avoid in
+	let idl, avoid = rename (Idset.add id avoid) idl in
+	(id :: idl, avoid) in
+  fst (rename avoid l)
+
+let push_vars ids (db,avoid) =
+  let ids',avoid' = rename_vars avoid ids in
+  ids', (ids' @ db, avoid')
+
+let get_db_name n (db,_) =
+  let id = List.nth db (pred n) in
+  if id = dummy_name then id_of_string "__" else id
+
+
+(*S Renamings of global objects. *)
+
+(*s Tables of global renamings *)
+
+let register_cleanup, do_cleanup =
+  let funs = ref [] in
+  (fun f -> funs:=f::!funs), (fun () -> List.iter (fun f -> f ()) !funs)
+
+type phase = Pre | Impl | Intf
+
+let set_phase, get_phase =
+  let ph = ref Impl in ((:=) ph), (fun () -> !ph)
+
+let set_keywords, get_keywords =
+  let k = ref Idset.empty in
+  ((:=) k), (fun () -> !k)
+
+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 empty_env () = [], get_global_ids ()
+
+let mktable autoclean =
+  let h = Hashtbl.create 97 in
+  if autoclean then register_cleanup (fun () -> Hashtbl.clear h);
+  (Hashtbl.replace h, Hashtbl.find h, fun () -> Hashtbl.clear h)
+
+(* We might have built [global_reference] whose canonical part is
+   inaccurate. We must hence compare only the user part,
+   hence using a Hashtbl might be incorrect *)
+
+let mktable_ref autoclean =
+  let m = ref Refmap'.empty in
+  let clear () = m := Refmap'.empty in
+  if autoclean then register_cleanup clear;
+  (fun r v -> m := Refmap'.add r v !m), (fun r -> Refmap'.find r !m), clear
+
+(* A table recording objects in the first level of all MPfile *)
+
+let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
+  mktable false
+
+let get_mpfiles_content mp =
+  try get_mpfiles_content mp
+  with Not_found -> failwith "get_mpfiles_content"
+
+(*s The list of external modules that will be opened initially *)
+
+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)
+
+(*s List of module parameters that we should alpha-rename *)
+
+let params_ren_add, params_ren_mem =
+  let m = ref MPset.empty in
+  let add mp = m:=MPset.add mp !m
+  and mem mp = MPset.mem mp !m
+  and clear () = m:=MPset.empty
+  in
+  register_cleanup clear;
+  (add,mem)
+
+(*s table indicating the visible horizon at a precise moment,
+    i.e. the stack of structures we are inside.
+
+  - The sequence of [mp] parts should have the following form:
+  a [MPfile] at the beginning, and then more and more [MPdot]
+  over this [MPfile], or [MPbound] when inside the type of a
+  module parameter.
+
+  - the [params] are the [MPbound] when [mp] is a functor,
+    the innermost [MPbound] coming first in the list.
+
+  - The [content] part is used to record all the names already
+  seen at this level.
+*)
+
+type visible_layer = { mp : module_path;
+		       params : module_path list;
+		       content : ((kind*string),label) Hashtbl.t }
+
+let pop_visible, push_visible, get_visible =
+  let vis = ref [] in
+  register_cleanup (fun () -> vis := []);
+  let pop () =
+    match !vis with
+      | [] -> assert false
+      | v :: vl ->
+	  vis := vl;
+	  (* 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
+  and push mp mps =
+    vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !vis
+  and get () = !vis
+  in (pop,push,get)
+
+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 l = Hashtbl.add (top_visible ()).content ks l
+
+(* 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 (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 *)
+
+(* This function creates from [id] a correct uppercase/lowercase identifier.
+   This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes
+   with previous [Coq_id] variable, these prefixes are duplicated if already
+   existing. *)
+
+let modular_rename k id =
+  let s = string_of_id id in
+  let prefix,is_ok =
+    if lang () <> CoreErlang
+     then if upperkind k then "Coq_",is_upper else "coq_",is_lower
+     else "_",(fun x -> true)
+  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 For monolithic extraction, first-level modules might have to be renamed
+    with unique numbers *)
+
+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
+  | MPbound mbid ->
+      let s = modular_rename Mod (id_of_mbid mbid) in
+      if not (params_ren_mem mp) then [s]
+      else let i,_,_ = repr_mbid mbid in [s^"__"^string_of_int i]
+  | MPfile _ ->
+      assert (modular ()); (* see [at_toplevel] above *)
+      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 if is_mp_bound (base_mp x) then raise Not_found; 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 = modpath_of_r r in
+  let l = mp_renaming mp in
+  let l = if lang () <> Ocaml && not (modular ()) then [""] else l in
+  let s = let idg = safe_basename_of_global r
+          in if l = [""] (* this happens only at toplevel of the monolithic case *)
+              then let globs = Idset.elements (get_global_ids ()) in

+              else modular_rename k idg
+  in add_global_ids (id_of_string s)
+   ; s::l
 
 (* Cached version of the last function *)
 
@@ -552,6 +551,24 @@
     let prf = if base_mp mp <> top_visible_mp () then s ^ "." else "" in
     prf ^ str
 
+(* For Core Erlang, we guess this will works *)
+let rec dequalify = function
+  | [] -> assert false
