Noise for nothing

Util only depends on Ocaml stdlib and Utf8 tables.
Generic pretty printing and loc functions are in Pp.
Generic errors are in Errors.

+ Training white-spaces, useless open, prlist copies random erasure.
Too many "open Errors" on the contrary.

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

15 files changed, 257 insertions, 257 deletions

diff --git a/lib/dyn.ml b/lib/dyn.ml
index a0109b60e..04f6d431f 100644
--- a/lib/dyn.ml
+++ b/lib/dyn.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 
 (* Dynamics, programmed with DANGER !!! *)
diff --git a/lib/envars.ml b/lib/envars.ml
index e5c938037..611b81a7e 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -38,7 +38,7 @@ let guess_coqlib () =
         in
         if Sys.file_exists (Filename.concat coqlib file)
         then coqlib
-        else Util.error "cannot guess a path for Coq libraries; please use -coqlib option")
+        else Errors.error "cannot guess a path for Coq libraries; please use -coqlib option")
 
 let coqlib () =
   if !Flags.coqlib_spec then !Flags.coqlib else
diff --git a/lib/errors.ml b/lib/errors.ml
index 3b5e67704..1060a8efd 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -6,10 +6,35 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+open Compat
 open Pp
 
-(* spiwack: it might be reasonable to decide and move the declarations
-   of Anomaly and so on to this module so as not to depend on Util. *)
+(* Errors *)
+
+exception Anomaly of string * std_ppcmds  (* System errors *)
+let anomaly string = raise (Anomaly(string, str string))
+let anomalylabstrm string pps = raise (Anomaly(string,pps))
+
+exception UserError of string * std_ppcmds (* User errors *)
+let error string = raise (UserError("_", str string))
+let errorlabstrm l pps = raise (UserError(l,pps))
+
+exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *)
+let alreadydeclared pps = raise (AlreadyDeclared(pps))
+
+let todo s = prerr_string ("TODO: "^s^"\n")
+
+(* raising located exceptions *)
+let anomaly_loc (loc,s,strm) = Loc.raise loc (Anomaly (s,strm))
+let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm))
+let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
+
+(* Like Exc_located, but specifies the outermost file read, the filename
+   associated to the location of the error, and the error itself. *)
+
+exception Error_in_file of string * (bool * string * loc) * exn
+
+exception Timeout
 
 let handle_stack = ref []
 
@@ -38,7 +63,7 @@ let where s =
   if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
 
 let raw_anomaly e = match e with
-  | Util.Anomaly (s,pps) -> where s ++ pps ++ str "."
+  | Anomaly (s,pps) -> where s ++ pps ++ str "."
   | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
   | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
 
@@ -62,7 +87,7 @@ let print_no_anomaly e = print_gen (fun e -> raise e) !handle_stack e
 (** Predefined handlers **)
 
 let _ = register_handler begin function
-  | Util.UserError(s,pps) -> hov 0 (str "Error: " ++ where s ++ pps)
+  | UserError(s,pps) -> hov 0 (str "Error: " ++ where s ++ pps)
   | _ -> raise Unhandled
 end
 
diff --git a/lib/errors.mli b/lib/errors.mli
index eb7fde8e7..a863c5e30 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -6,9 +6,45 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+open Pp
+
 (** This modules implements basic manipulations of errors for use
     throughout Coq's code. *)
 
+(** {6 Generic errors.}
+
+ [Anomaly] is used for system errors and [UserError] for the
+   user's ones. *)
+
+exception Anomaly of string * std_ppcmds
+val anomaly : string -> 'a
+val anomalylabstrm : string -> std_ppcmds -> 'a
+val anomaly_loc : loc * string * std_ppcmds -> 'a
+
+exception UserError of string * std_ppcmds
+val error : string -> 'a
+val errorlabstrm : string -> std_ppcmds -> 'a
+val user_err_loc : loc * string * std_ppcmds -> 'a
+
+exception AlreadyDeclared of std_ppcmds
+val alreadydeclared : std_ppcmds -> 'a
+
+val invalid_arg_loc : loc * string -> 'a
+
+(** [todo] is for running of an incomplete code its implementation is
+   "do nothing" (or print a message), but this function should not be
+   used in a released code *)
+
+val todo : string -> unit
+
+exception Timeout
+
+(** Like [Exc_located], but specifies the outermost file read, the
+   input buffer associated to the location of the error (or the module name
+   if boolean is true), and the error itself. *)
+
+exception Error_in_file of string * (bool * string * loc) * exn
+
 (** [register_handler h] registers [h] as a handler.
     When an expression is printed with [print e], it
     goes through all registered handles (the most
diff --git a/lib/gmapl.ml b/lib/gmapl.ml
index a00407426..01a277c78 100644
--- a/lib/gmapl.ml
+++ b/lib/gmapl.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 
 type ('a,'b) t = ('a,'b list) Gmap.t
diff --git a/lib/lib.mllib b/lib/lib.mllib
index db79b5c24..eb834af78 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -2,13 +2,13 @@ Xml_lexer
 Xml_parser
 Xml_utils
 Pp_control
-Pp
 Compat
 Flags
+Pp
 Segmenttree
 Unicodetable
-Util
 Errors
+Util
 Bigint
 Hashcons
 Dyn
diff --git a/lib/option.ml b/lib/option.ml
index c3fe9ce46..ef7a2e9e5 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -153,6 +153,13 @@ module List =
   let rec flatten = function
     | x::l -> cons x (flatten l)
     | [] -> []
+
+  let rec find f = function
+    |[] -> None
+    |h :: t -> match f h with
+	 |None -> find f t
+	 |x -> x
+
 end
 
 
diff --git a/lib/option.mli b/lib/option.mli
index b9fd7d2f3..217aa6696 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -100,6 +100,8 @@ module List : sig
   (** [List.flatten l] is the list of all the [y]s such that [l] contains
       [Some y] (in the same order). *)
   val flatten : 'a option list -> 'a list
+
+  val find : ('a -> 'b option) -> 'a list -> 'b option
 end
 
 
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index c602b403e..4fc53270c 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -7,12 +7,13 @@
 (************************************************************************)
 
 open Pp_control
+open Compat
 
 (* This should not be used outside of this file. Use
    Flags.print_emacs instead. This one is updated when reading
    command line options. This was the only way to make [Pp] depend on
-   an option without creating a circularity: [Flags. -> [Util] ->
-   [Pp] -> [Flags. *)
+   an option without creating a circularity: [Flags] -> [Util] ->
+   [Pp] -> [Flags] *)
 let print_emacs = ref false
 let make_pp_emacs() = print_emacs:=true
 let make_pp_nonemacs() = print_emacs:=false
@@ -336,3 +337,104 @@ let msg_warning x = msg_warning_with !err_ft x
 let string_of_ppcmds c =
   msg_with Format.str_formatter c;
   Format.flush_str_formatter ()
+
+(* Locations management *)
+type loc = Loc.t
+let dummy_loc = Loc.ghost
+let join_loc = Loc.merge
+let make_loc = make_loc
+let unloc = unloc
+
+type 'a located = loc * 'a
+let located_fold_left f x (_,a) = f x a
+let located_iter2 f (_,a) (_,b) = f a b
+let down_located f (_,a) = f a
+
+
+(* Copy paste from Util *)
+
+let pr_comma () = str "," ++ spc ()
+let pr_semicolon () = str ";" ++ spc ()
+let pr_bar () = str "|" ++ spc ()
+let pr_arg pr x = spc () ++ pr x
+let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
+let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
+
+let pr_nth n =
+  int n ++ str (match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th")
+
+(* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *)
+
+let rec prlist elem l = match l with
+  | []   -> mt ()
+  | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
+
+(* unlike all other functions below, [prlist] works lazily.
+   if a strict behavior is needed, use [prlist_strict] instead.
+   evaluation is done from left to right. *)
+
+let prlist_sep_lastsep no_empty sep lastsep elem =
+  let rec start = function
+    |[] -> mt ()
+    |[e] -> elem e
+    |h::t -> let e = elem h in
+	if no_empty && e = mt () then start t else
+	  let rec aux = function
+	    |[] -> mt ()
+	    |h::t ->
+	       let e = elem h and r = aux t in
+		 if no_empty && e = mt () then r else
+		   if r = mt ()
+		   then let s = lastsep () in s ++ e
+		   else let s = sep () in s ++ e ++ r
+	  in let r = aux t in e ++ r
+  in start
+
+let prlist_strict pr l = prlist_sep_lastsep true mt mt pr l
+(* [prlist_with_sep sep pr [a ; ... ; c]] outputs
+   [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
+let prlist_with_sep sep pr l = prlist_sep_lastsep false sep sep pr l
+(* Print sequence of objects separated by space (unless an element is empty) *)
+let pr_sequence pr l = prlist_sep_lastsep true spc spc pr l
+(* [pr_enum pr [a ; b ; ... ; c]] outputs
+   [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c] *)
+let pr_enum pr l = prlist_sep_lastsep true pr_comma (fun () -> str " and" ++ spc ()) pr l
+
+let pr_vertical_list pr = function
+  | [] -> str "none" ++ fnl ()
+  | l -> fnl () ++ str "  " ++ hov 0 (prlist_with_sep fnl pr l) ++ fnl ()
+
+(* [prvecti_with_sep sep pr [|a0 ; ... ; an|]] outputs
+   [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *)
+
+let prvecti_with_sep sep elem v =
+  let rec pr i =
+    if i = 0 then
+      elem 0 v.(0)
+    else
+      let r = pr (i-1) and s = sep () and e = elem i v.(i) in
+      r ++ s ++ e
+  in
+  let n = Array.length v in
+  if n = 0 then mt () else pr (n - 1)
+
+(* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *)
+
+let prvecti elem v = prvecti_with_sep mt elem v
+
+(* [prvect_with_sep sep pr [|a ; ... ; c|]] outputs
+   [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
+
+let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
+
+(* [prvect pr [|a ; ... ; c|]] outputs [pr a ++ ... ++ pr c] *)
+
+let prvect elem v = prvect_with_sep mt elem v
+
+let pr_located pr (loc,x) =
+  if Flags.do_beautify() && loc<>dummy_loc then
+    let (b,e) = unloc loc in
+    comment b ++ pr x ++ comment e
+  else pr x
+
+let surround p = hov 1 (str"(" ++ p ++ str")")
diff --git a/lib/pp.mli b/lib/pp.mli
index 7070e3f5f..2fd62d55a 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp_control
+open Compat
 
 (** Modify pretty printing functions behavior for emacs ouput (special
    chars inserted at some places). This function should called once in
@@ -114,3 +115,45 @@ val msgerrnl : std_ppcmds -> unit
 val msg_warning : std_ppcmds -> unit
 
 val string_of_ppcmds : std_ppcmds -> string
+
+(** {6 Location management. } *)
+
+type loc = Loc.t
+val unloc : loc -> int * int
+val make_loc : int * int -> loc
+val dummy_loc : loc
+val join_loc : loc -> loc -> loc
+
+type 'a located = loc * 'a
+val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
+val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
+val down_located : ('a -> 'b) -> 'a located -> 'b
+
+(** {6 Util copy/paste. } *)
+
+val pr_comma : unit -> std_ppcmds
+val pr_semicolon : unit -> std_ppcmds
+val pr_bar : unit -> std_ppcmds
+val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
+val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
+val pr_nth : int -> std_ppcmds
+
+val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+
+(** unlike all other functions below, [prlist] works lazily.
+   if a strict behavior is needed, use [prlist_strict] instead. *)
+val prlist_strict :  ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val prlist_with_sep :
+   (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvect_with_sep :
+   (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvecti_with_sep :
+   (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
+val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
+val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val surround : std_ppcmds -> std_ppcmds
diff --git a/lib/rtree.ml b/lib/rtree.ml
index 22d3d72b4..4fccd282f 100644
--- a/lib/rtree.ml
+++ b/lib/rtree.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 
 
@@ -173,11 +174,11 @@ let rec pp_tree prl t =
     | Node(lab,[||]) -> hov 2 (str"("++prl lab++str")")
     | Node(lab,v) ->
         hov 2 (str"("++prl lab++str","++brk(1,0)++
-               Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str")")
+               prvect_with_sep pr_comma (pp_tree prl) v++str")")
     | Rec(i,v) ->
         if Array.length v = 0 then str"Rec{}"
         else if Array.length v = 1 then
           hov 2 (str"Rec{"++pp_tree prl v.(0)++str"}")
         else
           hov 2 (str"Rec{"++int i++str","++brk(1,0)++
-                 Util.prvect_with_sep Util.pr_comma (pp_tree prl) v++str"}")
+                 prvect_with_sep pr_comma (pp_tree prl) v++str"}")
diff --git a/lib/system.ml b/lib/system.ml
index 7d54e2c3a..7e0347530 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -9,6 +9,7 @@
 (* $Id$ *)
 
 open Pp
+open Errors
 open Util
 open Unix
 
@@ -140,7 +141,7 @@ let exclude_search_in_dirname f = skipped_dirnames := f :: !skipped_dirnames
 
 let ok_dirname f =
   f <> "" && f.[0] <> '.' && not (List.mem f !skipped_dirnames) &&
-  try ignore (check_ident f); true with _ -> false
+  match ident_refutation f with |None -> true |_ -> false
 
 let all_subdirs ~unix_path:root =
   let l = ref [] in
diff --git a/lib/util.ml b/lib/util.ml
index 287dd3719..879884283 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -6,47 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-open Pp
-open Compat
-
-(* Errors *)
-
-exception Anomaly of string * std_ppcmds  (* System errors *)
-let anomaly string = raise (Anomaly(string, str string))
-let anomalylabstrm string pps = raise (Anomaly(string,pps))
-
-exception UserError of string * std_ppcmds (* User errors *)
-let error string = raise (UserError("_", str string))
-let errorlabstrm l pps = raise (UserError(l,pps))
-
-exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *)
-let alreadydeclared pps = raise (AlreadyDeclared(pps))
-
-let todo s = prerr_string ("TODO: "^s^"\n")
-
-exception Timeout
-
-type loc = Loc.t
-let dummy_loc = Loc.ghost
-let join_loc = Loc.merge
-let make_loc = make_loc
-let unloc = unloc
-
-(* raising located exceptions *)
-type 'a located = loc * 'a
-let anomaly_loc (loc,s,strm) = Loc.raise loc (Anomaly (s,strm))
-let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm))
-let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
-
-let located_fold_left f x (_,a) = f x a
-let located_iter2 f (_,a) (_,b) = f a b
-let down_located f (_,a) = f a
-
-(* Like Exc_located, but specifies the outermost file read, the filename
-   associated to the location of the error, and the error itself. *)
-
-exception Error_in_file of string * (bool * string * loc) * exn
-
 (* Mapping under pairs *)
 
 let on_fst f (a,b) = (f a,b)
@@ -319,40 +278,39 @@ let next_utf8 s i =
 
 (* Check the well-formedness of an identifier *)
 
-let check_initial handle j n s =
+let initial_refutation j n s =
   match classify_unicode n with
-  | UnicodeLetter -> ()
+  | UnicodeLetter -> None
   | _ ->
       let c = String.sub s 0 j in
-      handle ("Invalid character '"^c^"' at beginning of identifier \""^s^"\".")
+      Some ("Invalid character '"^c^"' at beginning of identifier \""^s^"\".")
 
-let check_trailing handle i j n s =
+let trailing_refutation i j n s =
   match classify_unicode n with
-  | UnicodeLetter | UnicodeIdentPart -> ()
+  | UnicodeLetter | UnicodeIdentPart -> None
   | _ ->
       let c = String.sub s i j in
-      handle ("Invalid character '"^c^"' in identifier \""^s^"\".")
+      Some ("Invalid character '"^c^"' in identifier \""^s^"\".")
 
-let check_ident_gen handle s =
-  let i = ref 0 in
-  if s <> ".." then try
+let ident_refutation s =
+  if s = ".." then None else try
     let j, n = next_utf8 s 0 in
-    check_initial handle j n s;
-    i := !i + j;
-    try
-      while true do
-	let j, n = next_utf8 s !i in
-	check_trailing handle !i j n s;
-	i := !i + j
-      done
-    with End_of_input -> ()
+      match initial_refutation j n s with
+	|None ->
+	   begin try
+	     let rec aux i =
+	       let j, n = next_utf8 s i in
+		 match trailing_refutation i j n s with
+		   |None -> aux (i + j)
+		   |x -> x
+	     in aux j
+	   with End_of_input -> None
+	   end
+	|x -> x
   with
-  | End_of_input -> error "The empty string is not an identifier."
-  | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence.")
-  | Invalid_argument _ -> error (s^": invalid utf8 sequence.")
-
-let check_ident_soft = check_ident_gen warning
-let check_ident = check_ident_gen error
+  | End_of_input -> Some "The empty string is not an identifier."
+  | UnsupportedUtf8 -> Some (s^": unsupported character in utf8 sequence.")
+  | Invalid_argument _ -> Some (s^": invalid utf8 sequence.")
 
 let lowercase_unicode =
   let tree = Segmenttree.make Unicodetable.to_lower in
@@ -1288,102 +1246,6 @@ let map_succeed f =
   in
   map_f
 
-(* Pretty-printing *)
-
-let pr_spc = spc
-let pr_fnl = fnl
-let pr_int = int
-let pr_str = str
-let pr_comma () = str "," ++ spc ()
-let pr_semicolon () = str ";" ++ spc ()
-let pr_bar () = str "|" ++ spc ()
-let pr_arg pr x = spc () ++ pr x
-let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
-let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
-
-let nth n = str (ordinal n)
-
-(* [prlist pr [a ; ... ; c]] outputs [pr a ++ ... ++ pr c] *)
-
-let rec prlist elem l = match l with
-  | []   -> mt ()
-  | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
-
-(* unlike all other functions below, [prlist] works lazily.
-   if a strict behavior is needed, use [prlist_strict] instead.
-   evaluation is done from left to right. *)
-
-let rec prlist_strict elem l = match l with
-  | []   -> mt ()
-  | h::t ->
-      let e = elem h in let r = prlist_strict elem t in e++r
-
-(* [prlist_with_sep sep pr [a ; ... ; c]] outputs
-   [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
-
-let rec prlist_with_sep sep elem l = match l with
-  | []   -> mt ()
-  | [h]  -> elem h
-  | h::t ->
-      let e = elem h and s = sep() and r = prlist_with_sep sep elem t in
-      e ++ s ++ r
-
-(* Print sequence of objects separated by space (unless an element is empty) *)
-
-let rec pr_sequence elem = function
-  | []   -> mt ()
-  | [h]  -> elem h
-  | h::t ->
-      let e = elem h and r = pr_sequence elem t in
-      if e = mt () then r else e ++ spc () ++ r
-
-(* [pr_enum pr [a ; b ; ... ; c]] outputs
-   [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c] *)
-
-let pr_enum pr l =
-  let c,l' = list_sep_last l in
-  prlist_with_sep pr_comma pr l' ++
-  (if l'<>[] then str " and" ++ spc () else mt()) ++ pr c
-
-let pr_vertical_list pr = function
-  | [] -> str "none" ++ fnl ()
-  | l -> fnl () ++ str "  " ++ hov 0 (prlist_with_sep pr_fnl pr l) ++ fnl ()
-
-(* [prvecti_with_sep sep pr [|a0 ; ... ; an|]] outputs
-   [pr 0 a0 ++ sep() ++ ... ++ sep() ++ pr n an] *)
-
-let prvecti_with_sep sep elem v =
-  let rec pr i =
-    if i = 0 then
-      elem 0 v.(0)
-    else
-      let r = pr (i-1) and s = sep () and e = elem i v.(i) in
-      r ++ s ++ e
-  in
-  let n = Array.length v in
-  if n = 0 then mt () else pr (n - 1)
-
-(* [prvecti pr [|a0 ; ... ; an|]] outputs [pr 0 a0 ++ ... ++ pr n an] *)
-
-let prvecti elem v = prvecti_with_sep mt elem v
-
-(* [prvect_with_sep sep pr [|a ; ... ; c|]] outputs
-   [pr a ++ sep() ++ ... ++ sep() ++ pr c] *)
-
-let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
-
-(* [prvect pr [|a ; ... ; c|]] outputs [pr a ++ ... ++ pr c] *)
-
-let prvect elem v = prvect_with_sep mt elem v
-
-let pr_located pr (loc,x) =
-  if Flags.do_beautify() && loc<>dummy_loc then
-    let (b,e) = unloc loc in
-    comment b ++ pr x ++ comment e
-  else pr x
-
-let surround p = hov 1 (str"(" ++ p ++ str")")
-
 (*s Memoization *)
 
 let memo1_eq eq f =
diff --git a/lib/util.mli b/lib/util.mli
index 1fec22954..caf1723b3 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -6,57 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open Compat
-
 (** This module contains numerous utility functions on strings, lists,
    arrays, etc. *)
 
-(** {6 ... } *)
-(** Errors. [Anomaly] is used for system errors and [UserError] for the
-   user's ones. *)
-
-exception Anomaly of string * std_ppcmds
-val anomaly : string -> 'a
-val anomalylabstrm : string -> std_ppcmds -> 'a
-
-exception UserError of string * std_ppcmds
-val error : string -> 'a
-val errorlabstrm : string -> std_ppcmds -> 'a
-
-exception AlreadyDeclared of std_ppcmds
-val alreadydeclared : std_ppcmds -> 'a
-
-(** [todo] is for running of an incomplete code its implementation is
-   "do nothing" (or print a message), but this function should not be
-   used in a released code *)
-
-val todo : string -> unit
-
-exception Timeout
-
-type loc = Loc.t
-
-type 'a located = loc * 'a
-
-val unloc : loc -> int * int
-val make_loc : int * int -> loc
-val dummy_loc : loc
-val join_loc : loc -> loc -> loc
-
-val anomaly_loc : loc * string * std_ppcmds -> 'a
-val user_err_loc : loc * string * std_ppcmds -> 'a
-val invalid_arg_loc : loc * string -> 'a
-val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a
-val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit
-val down_located : ('a -> 'b) -> 'a located -> 'b
-
-(** Like [Exc_located], but specifies the outermost file read, the
-   input buffer associated to the location of the error (or the module name
-   if boolean is true), and the error itself. *)
-
-exception Error_in_file of string * (bool * string * loc) * exn
-
 (** Mapping under pairs *)
 
 val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c
@@ -86,6 +38,7 @@ val is_letter : char -> bool
 val is_digit : char -> bool
 val is_ident_tail : char -> bool
 val is_blank : char -> bool
+val next_utf8 : string -> int -> int * int
 
 (** {6 Strings. } *)
 
@@ -108,9 +61,8 @@ type utf8_status = UnicodeLetter | UnicodeIdentPart | UnicodeSymbol
 
 exception UnsupportedUtf8
 
+val ident_refutation : string -> string option
 val classify_unicode : int -> utf8_status
-val check_ident : string -> unit
-val check_ident_soft : string -> unit
 val lowercase_first_char_utf8 : string -> string
 val ascii_of_ident : string -> string
 
@@ -336,39 +288,6 @@ val interval : int -> int -> int list
 
 val map_succeed : ('a -> 'b) -> 'a list -> 'b list
 
-(** {6 Pretty-printing. } *)
-
-val pr_spc : unit -> std_ppcmds
-val pr_fnl : unit -> std_ppcmds
-val pr_int : int -> std_ppcmds
-val pr_str : string -> std_ppcmds
-val pr_comma : unit -> std_ppcmds
-val pr_semicolon : unit -> std_ppcmds
-val pr_bar : unit -> std_ppcmds
-val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
-val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
-val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
-val nth : int -> std_ppcmds
-
-val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-
-(** unlike all other functions below, [prlist] works lazily.
-   if a strict behavior is needed, use [prlist_strict] instead. *)
-val prlist_strict :  ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-val prlist_with_sep :
-   (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
-val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
-val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
-val prvect_with_sep :
-   (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds
-val prvecti_with_sep :
-   (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
-val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds
-val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds
-val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
-val surround : std_ppcmds -> std_ppcmds
-
 (** {6 Memoization. } *)
 
 (** General comments on memoization:
diff --git a/lib/xml_lexer.mli b/lib/xml_lexer.mli
index a1ca05765..ebb867190 100644
--- a/lib/xml_lexer.mli
+++ b/lib/xml_lexer.mli
@@ -41,4 +41,4 @@ val init : Lexing.lexbuf -> unit
 val close : Lexing.lexbuf -> unit
 val token : Lexing.lexbuf -> token
 val pos : Lexing.lexbuf -> pos
-val restore : pos -> unit
\ No newline at end of file
+val restore : pos -> unit