 +              else modular_rename k idg
 +  in add_global_ids (id_of_string s)
 +   ; s::l
-+
-+(* Cached version of the last function *)
-+
-+let ref_renaming =
-+  let add,get,_ = mktable_ref true in
-+  fun ((k,r) as x) ->
-+    try if is_mp_bound (base_mp (modpath_of_r r)) then raise Not_found; get r
-+    with Not_found -> let y = ref_renaming_fun x in add r 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 ks = function
-+  | [] -> false
-+  | mp :: _ when mp = mp0 -> false
-+  | 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 rec params_lookup mp0 ks = function
-+  | [] -> false
-+  | param :: _ when mp0 = param -> true
-+  | param :: params ->
-+      if ks = (Mod, List.hd (mp_renaming param)) then params_ren_add param;
-+      params_lookup mp0 ks params
-+
-+let visible_clash mp0 ks =
-+  let rec clash = function
-+    | [] -> false
-+    | v :: _ when v.mp = mp0 -> false
-+    | v :: vis ->
-+	let b = Hashtbl.mem v.content ks in
-+	if b && not (is_mp_bound mp0) then true
-+	else begin
-+	  if b then params_ren_add mp0;
-+	  if params_lookup mp0 ks v.params then false
-+	  else clash vis
-+	end
-+  in clash (get_visible ())
-+
-+(* Same, but with verbose output (and mp0 shouldn't be a MPbound) *)
-+
-+let visible_clash_dbg mp0 ks =
-+  let rec clash = function
-+    | [] -> None
-+    | v :: _ when v.mp = mp0 -> None
-+    | v :: vis ->
-+	try Some (v.mp,Hashtbl.find v.content ks)
-+	with Not_found ->
-+	  if params_lookup mp0 ks v.params then None
-+	  else 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_files = mpfiles_list () in
-+    let used_ks = List.map (fun mp -> Mod,string_of_modfile mp) used_files in
-+    (* By default, we open all used files. Ambiguities will be resolved later
-+       by using qualified names. Nonetheless, we don't open any file A that
-+       contains an immediate submodule A.B hiding another file B : otherwise,
-+       after such an open, there's no unambiguous way to refer to objects of B. *)
-+    let to_open =
-+      List.filter
-+	(fun mp ->
-+	   not (List.exists (Hashtbl.mem (get_mpfiles_content mp)) used_ks))
-+	used_files
-+    in
-+    mpfiles_clear ();
-+    List.iter mpfiles_add to_open;
-+    mpfiles_list ()
-+
-+(*s On-the-fly qualification issues for both monolithic or modular extraction. *)
-+
-+(* [pp_ocaml_gen] below is 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.
-+   [rls] is the string list giving the qualified name, short name at the end. *)
-+
-+(* In Coq, we can qualify [M.t] even if we are inside [M], but in Ocaml we
-+   cannot do that. So, if [t] gets hidden and we need a long name for it,
-+   we duplicate the _definition_ of t in a Coq__XXX module, and similarly
-+   for a sub-module [M.N] *)
-+
-+let pp_duplicate k' prefix mp rls olab =
-+  let rls', lbl =
-+    if k'<>Mod then
-+      (* Here rls=[s], the ref to print is <prefix>.<s>, and olab<>None *)
-+      rls, Option.get olab
-+    else
-+      (* Here rls=s::rls', we search the label for s inside mp *)
-+      List.tl rls, get_nth_label_mp (mp_length mp - mp_length prefix) mp
-+  in
-+  try dottify (check_duplicate prefix lbl :: rls')
-+  with Not_found ->
-+    assert (get_phase () = Pre); (* otherwise it's too late *)
-+    add_duplicate prefix lbl; dottify rls
-+
-+let fstlev_ks k = function
-+  | [] -> assert false
-+  | [s] -> k,s
-+  | s::_ -> Mod,s
-+
-+(* [pp_ocaml_local] : [mp] has something in common with [top_visible ()]
-+   but isn't equal to it *)
-+
-+let pp_ocaml_local k prefix mp rls olab =
-+  (* what is the largest prefix of [mp] that belongs to [visible]? *)
-+  assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
-+  let rls' = list_skipn (mp_length prefix) rls in
-+  let k's = fstlev_ks k rls' in
-+  (* Reference r / module path mp is of the form [<prefix>.s.<...>]. *)
-+  if not (visible_clash prefix k's) then dottify rls'
-+  else pp_duplicate (fst k's) prefix mp rls' olab
-+
-+(* [pp_ocaml_bound] : [mp] starts with a [MPbound], and we are not inside
-+   (i.e. we are not printing the type of the module parameter) *)
-+
-+let pp_ocaml_bound base rls =
-+  (* clash with a MPbound will be detected and fixed by renaming this MPbound *)
-+  if get_phase () = Pre then ignore (visible_clash base (Mod,List.hd rls));
-+  dottify rls
-+
-+(* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *)
-+
-+let pp_ocaml_extern k base rls = match rls with
-+  | [] -> assert false
-+  | base_s :: rls' ->
-+      if (not (modular ())) (* Pseudo qualification with "" *)
-+	|| (rls' = [])  (* Case of a file A.v used as a module later *)
-+	|| (not (mpfiles_mem base)) (* Module not opened *)
-+	|| (mpfiles_clash base (fstlev_ks k rls')) (* Conflict in opened files *)
-+	|| (visible_clash base (fstlev_ks k rls')) (* Local conflict *)
-+      then
-+	(* We need to fully qualify. Last clash situation is unsupported *)
-+	match visible_clash_dbg base (Mod,base_s) with
-+	  | None -> dottify rls
-+	  | Some (mp,l) -> error_module_clash base (MPdot (mp,l))
-+      else
-+	(* Standard situation : object in an opened file *)
-+	dottify rls'
-+
-+(* [pp_ocaml_gen] : choosing between [pp_ocaml_extern] or [pp_ocaml_extern] *)
-+
-+let pp_ocaml_gen k mp rls olab =
-+  match common_prefix_from_list mp (get_visible_mps ()) with
-+    | Some prefix -> pp_ocaml_local k prefix mp rls olab
-+    | None ->
-+	let base = base_mp mp in
-+	if is_mp_bound base then pp_ocaml_bound base rls
-+	else pp_ocaml_extern k base rls
-+
-+(* For Haskell, things are simplier: we have removed (almost) all structures *)
-+
-+let pp_haskell_gen k mp rls = match rls with
-+  | [] -> assert false
-+  | s::rls' ->
-+    let str = pseudo_qualify rls' in
-+    let str = if is_upper str && not (upperkind k) then ("_"^str) else str in
-+    let prf = if base_mp mp <> top_visible_mp () then s ^ "." else "" in
-+    prf ^ str
-+
+ 
+ (* 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

+           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
+      | 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"
+      | 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
@@ -0,0 +1,1324 @@
+open Pp
+open Util

diff -aurN coq-8.4pl2/ide/coq_lex.mll coq-8.4pl2-new/ide/coq_lex.mll
--- coq-8.4pl2/ide/coq_lex.mll	2012-08-08 11:54:37.000000000 -0700
+++ coq-8.4pl2-new/ide/coq_lex.mll	2013-07-21 08:18:44.062892481 -0700
@@ -101,7 +101,7 @@
 | "Tactic" space+ "Notation"
 | "Implicit" space+ "Type" "s"?
 | "Combined" space+ "Scheme"
-| "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"|"Toplevel"))|
+| "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")
diff -aurN coq-8.4pl2/plugins/extraction/common.ml coq-8.4pl2-new/plugins/extraction/common.ml
--- coq-8.4pl2/plugins/extraction/common.ml	2012-08-08 11:54:37.000000000 -0700
+++ coq-8.4pl2-new/plugins/extraction/common.ml	2013-07-21 08:18:44.062892481 -0700
@@ -309,11 +309,13 @@
 let modular_rename k id =
   let s = string_of_id id in
   let prefix,is_ok =
-    if upperkind k then "Coq_",is_upper else "coq_",is_lower
+    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)
+     (Idset.mem id (get_keywords ())) ||
+     (String.length s >= 4 && String.sub s 0 4 = prefix)
   then prefix ^ s
   else s
 
@@ -371,17 +373,14 @@
   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
-      let id = next_ident_away (kindcase_id k idg) globs in
-      string_of_id id
-    else modular_rename k idg
-  in
-  add_global_ids (id_of_string s);
-  s::l
+  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
