1 files changed, 32 insertions, 23 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 3c5f6cb7..f235bb89 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -1,14 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Pp
 open Util
 open Names
+open ModPath
 open Namegen
 open Nameops
 open Libnames
@@ -44,7 +47,7 @@ let pp_apply2 st par args =
 
 let pr_binding = function
   | [] -> mt ()
-  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
+  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") Id.print l
 
 let pp_tuple_light f = function
   | [] -> mt ()
@@ -67,7 +70,9 @@ let pp_boxed_tuple f = function
     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 ()
+(* EG: This looks quite suspicious... but beware of bugs *)
+(* let fnl () = stras (1000000,"") ++ fnl () *)
+let fnl () = fnl ()
 
 let fnl2 () = fnl () ++ fnl ()
 
@@ -91,10 +96,7 @@ let begins_with_CoqXX s =
 
 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
+  else String.map (fun c -> if c == '\'' then '~' else c) s
 
 let rec qualify delim = function
   | [] -> assert false
@@ -110,12 +112,17 @@ let pseudo_qualify = qualify "__"
 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 (ascii_of_id id))
+[@@@ocaml.warning "-3"]       (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+let uncapitalize = String.uncapitalize
+[@@@ocaml.warning "+3"]
+
+let lowercase_id id = Id.of_string (uncapitalize (ascii_of_id id))
 let uppercase_id id =
   let s = ascii_of_id id in
   assert (not (String.is_empty s));
   if s.[0] == '_' then Id.of_string ("Coq_"^s)
-  else Id.of_string (String.capitalize s)
+  else Id.of_string (capitalize s)
 
 type kind = Term | Type | Cons | Mod
 
@@ -145,7 +152,7 @@ type env = Id.t list * Id.Set.t
 (*s Generic renaming issues for local variable names. *)
 
 let rec rename_id id avoid =
-  if Id.Set.mem id avoid then rename_id (lift_subscript id) avoid else id
+  if Id.Set.mem id avoid then rename_id (increment_subscript id) avoid else id
 
 let rec rename_vars avoid = function
   | [] ->
@@ -269,8 +276,8 @@ let params_ren_add, params_ren_mem =
   seen at this level.
 *)
 
-type visible_layer = { mp : module_path;
-		       params : module_path list;
+type visible_layer = { mp : ModPath.t;
+		       params : ModPath.t list;
 		       mutable content : Label.t KMap.t; }
 
 let pop_visible, push_visible, get_visible =
@@ -308,15 +315,16 @@ end
 
 module DupMap = Map.Make(DupOrd)
 
-let add_duplicate, check_duplicate =
+let add_duplicate, get_duplicate =
   let index = ref 0 and dups = ref DupMap.empty in
   register_cleanup (fun () -> index := 0; dups := DupMap.empty);
   let add mp l =
      incr index;
      let ren = "Coq__" ^ string_of_int !index in
      dups := DupMap.add (mp,l) ren !dups
-  and check mp l = DupMap.find (mp, l) !dups
-  in (add,check)
+  and get mp l =
+    try Some (DupMap.find (mp, l) !dups) with Not_found -> None
+  in (add,get)
 
 type reset_kind = AllButExternal | Everything
 
@@ -399,7 +407,7 @@ let ref_renaming_fun (k,r) =
     let idg = safe_basename_of_global r in
     match l with
     | [""] -> (* this happens only at toplevel of the monolithic case *)
-      let globs = Id.Set.elements (get_global_ids ()) in
+      let globs = get_global_ids () in
       let id = next_ident_away (kindcase_id k idg) globs in
       Id.to_string id
     | _ -> modular_rename k idg
@@ -510,10 +518,11 @@ let pp_duplicate k' prefix mp rls olab =
       (* 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
+  match get_duplicate prefix lbl with
+  | Some ren -> dottify (ren :: rls')
+  | None ->
+     assert (get_phase () == Pre); (* otherwise it's too late *)
+     add_duplicate prefix lbl; dottify rls
 
 let fstlev_ks k = function
   | [] -> assert false