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

31 files changed, 71 insertions, 45 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index f4dab15f04..0357fc8a3c 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -10,6 +10,7 @@
    decidable equality, created by Vincent Siles, Oct 2007 *)
 
 open Tacmach
+open Errors
 open Util
 open Flags
 open Decl_kinds
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 9258a39fcf..1795336f4b 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -53,7 +53,7 @@ let subst_evar_in_evm evar def evm =
 
 let rec safe_define evm ev c =
   if not (closedn (-1) c) then raise Termops.CannotFilter else
-(*  msgnl(str"safe_define "++pr_evar_map evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*)
+(*  msgnl(str"safe_define "++pr_evar_map evm++spc()++str" |- ?"++Pp.int ev++str" := "++pr_constr c);*)
   let evi = (Evd.find evm ev) in
   let define_subst evm sigma =
     Util.Intmap.fold
@@ -99,7 +99,7 @@ module SubstSet : Set.S with type elt = Termops.subst
 let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) =
   let ev_typ = Libtypes.reduce (evar_concl evi) in
   let sort_is_prop = is_Prop (Typing.type_of (Global.env()) evm (evar_concl evi)) in
-(*  msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Util.pr_int ev);*)
+(*  msgnl(str"cherche "++pr_constr ev_typ++str" pour "++Pp.int ev);*)
   let substs = ref SubstSet.empty in
   try List.iter
     ( fun (gr,(pat,_),s) ->
@@ -107,7 +107,7 @@ let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) =
 	let genl = List.map (fun (_,_,t) -> t) genl in
 	let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) genl in
 	let def = applistc (Libnames.constr_of_global gr) argl in
-(*	msgnl(str"essayons  ?"++Util.pr_int ev++spc()++str":="++spc()
+(*	msgnl(str"essayons  ?"++Pp.int ev++spc()++str":="++spc()
 	      ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*)
 	(*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*)
 	try
@@ -145,7 +145,7 @@ let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit
 	let tyl = List.map (fun (_,_,t) -> t) ctx in
 	let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in
 	let def = applistc c argl in
-(*	msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*)
+(*	msgnl(str"trouvé def ?"++Pp.int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*)
 	try
 	  if not (Evd.is_defined evm ev) then
 	    let evm = safe_define evm ev def in
@@ -222,7 +222,7 @@ let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature
     ( fun ctx typ ->
 	List.iter
 	  (fun ((cl,ev,evm),_,_) ->
-(*	     msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*)
+(*	     msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Pp.int ev++str " dans "++pr_evar_map evm);*)
 	     smap := Gmapl.add (cl,evm) (ctx,ev) !smap)
 	  (Recordops.methods_matching typ)
     ) [] deftyp;
@@ -265,7 +265,7 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit)
        then Evd.remove evm ev,gen
        else evm,(ev::gen))
     gen (evm,[]) in
-(*  msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_map evm);*)
+(*  msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Pp.int gen++str"] : "++spc()++pr_evar_map evm);*)
   let ngen = List.length gen in
   let (_,ctx,evm) = List.fold_left
     ( fun (i,ctx,evm) ev ->
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 5f2c3dbbe0..281ae784e7 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -8,6 +8,7 @@
 
 open Compat
 open Pp
+open Errors
 open Util
 open Indtypes
 open Type_errors
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index da9d3590f5..1d686b5dab 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 
 (** Error report. *)
diff --git a/toplevel/class.ml b/toplevel/class.ml
index ebaa19b660..79d7a99fd6 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 1e83e4b81c..b513f2e2e8 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -16,6 +16,8 @@ open Evd
 open Environ
 open Nametab
 open Mod_subst
+open Errors
+open Pp
 open Util
 open Typeclasses_errors
 open Typeclasses
@@ -132,7 +134,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 	  (fun avoid (clname, (id, _, t)) ->
 	    match clname with
 	    | Some (cl, b) ->
-		let t = CHole (Util.dummy_loc, None) in
+		let t = CHole (Pp.dummy_loc, None) in
 		  t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
@@ -224,7 +226,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 			    k.cl_projs;
 			  c :: props, rest'
 		      with Not_found ->
-			(CHole (Util.dummy_loc, None) :: props), rest
+			(CHole (Pp.dummy_loc, None) :: props), rest
 		    else props, rest)
 		  ([], props) k.cl_props
 	      in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 68a93a7428..424645fe88 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -15,6 +15,7 @@ open Environ
 open Nametab
 open Mod_subst
 open Topconstr
+open Errors
 open Util
 open Typeclasses
 open Implicit_quantifiers
diff --git a/toplevel/command.ml b/toplevel/command.ml
index eca53ae711..33a521d6f0 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Flags
 open Term
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8ffdbdec4a..76f6dd0110 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Pp
 open Names
 open Term
 open Entries
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0fc6d02c1a..d17d07300b 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open System
 open Flags
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index bab711ea42..b24ac8e7d3 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Names
+open Errors
 open Util
 open Sign
 open Term
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 22568ee886..4306a96736 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Flags
 open Names
@@ -176,8 +177,8 @@ let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
   let pr,prt = pr_ljudge_env env rator in
   let term_string1 = str (plural nargs "term") in
   let term_string2 =
-    if nargs>1 then str "The " ++ nth n ++ str " term" else str "This term" in
-  let appl = prvect_with_sep pr_fnl
+    if nargs>1 then str "The " ++ pr_nth n ++ str " term" else str "This term" in
+  let appl = prvect_with_sep fnl
 	       (fun c ->
 		  let pc,pct = pr_ljudge_env env c in
 		  hov 2 (pc ++ spc () ++ str ": " ++ pct)) randl
@@ -199,7 +200,7 @@ let explain_cant_apply_not_functional env sigma rator randl =
 (*  let pe = pr_ne_context_of (str "in environment") env in*)
   let pr = pr_lconstr_env env rator.uj_val in
   let prt = pr_lconstr_env env rator.uj_type in
-  let appl = prvect_with_sep pr_fnl
+  let appl = prvect_with_sep fnl
 	       (fun c ->
 		  let pc = pr_lconstr_env env c.uj_val in
 		  let pct = pr_lconstr_env env c.uj_type in
@@ -233,7 +234,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
   let prt_name i =
     match names.(i) with
         Name id -> str "Recursive definition of " ++ pr_id id
-      | Anonymous -> str "The " ++ nth i ++ str " definition" in
+      | Anonymous -> str "The " ++ pr_nth i ++ str " definition" in
 
   let st = match err with
 
@@ -248,18 +249,18 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
       let called =
         match names.(j) with
             Name id -> pr_id id
-          | Anonymous -> str "the " ++ nth i ++ str " definition" in
+          | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in
       let pr_db x = quote (pr_db env x) in
       let vars =
         match (lt,le) with
             ([],[]) -> assert false
           | ([],[x]) -> str "a subterm of " ++ pr_db x
           | ([],_) -> str "a subterm of the following variables: " ++
-              prlist_with_sep pr_spc pr_db le
+              pr_sequence pr_db le
           | ([x],_) -> pr_db x
           | _ ->
               str "one of the following variables: " ++
-              prlist_with_sep pr_spc pr_db lt in
+              pr_sequence pr_db lt in
       str "Recursive call to " ++ called ++ spc () ++
       strbrk "has principal argument equal to" ++ spc () ++
       pr_lconstr_env arg_env arg ++ strbrk " instead of " ++ vars
@@ -268,7 +269,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
       let called =
         match names.(j) with
             Name id -> pr_id id
-          | Anonymous -> str "the " ++ nth i ++ str " definition" in
+          | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in
      str "Recursive call to " ++ called ++ str " has not enough arguments"
 
   (* CoFixpoint guard errors *)
@@ -317,7 +318,7 @@ let explain_ill_typed_rec_body env sigma i names vdefj vargs =
   let pvd,pvdt = pr_ljudge_env env (vdefj.(i)) in
   let pv = pr_lconstr_env env vargs.(i) in
   str "The " ++
-  (if Array.length vdefj = 1 then mt () else nth (i+1) ++ spc ()) ++
+  (if Array.length vdefj = 1 then mt () else pr_nth (i+1) ++ spc ()) ++
   str "recursive definition" ++ spc () ++ pvd ++ spc () ++
   str "has type" ++ spc () ++ pvdt ++ spc () ++
   str "while it should be" ++ spc () ++ pv ++ str "."
@@ -363,7 +364,7 @@ let explain_hole_kind env evi = function
 	      pr_ne_context_of (str " in environment:"++ fnl ()) (mt ()) env)
 	(mt ()) evi
   | TomatchTypeParameter (tyi,n) ->
-      str "the " ++ nth n ++
+      str "the " ++ pr_nth n ++
       str " argument of the inductive type (" ++ pr_inductive env tyi ++
       str ") of this term"
   | GoalEvar ->
@@ -694,7 +695,7 @@ let pr_constr_exprs exprs =
 let explain_no_instance env (_,id) l =
   str "No instance found for class " ++ Nameops.pr_id id ++ spc () ++
   str "applied to arguments" ++ spc () ++
-    prlist_with_sep pr_spc (pr_lconstr_env env) l
+    pr_sequence (pr_lconstr_env env) l
 
 let is_goal_evar evi = match evi.evar_source with (_, GoalEvar) -> true | _ -> false
 
@@ -830,7 +831,7 @@ let error_bad_ind_parameters env c n v1 v2  =
   let pv1 = pr_lconstr_env env v1 in
   let pv2 = pr_lconstr_env env v2 in
   str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
-  str " as " ++ nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "."
+  str " as " ++ pr_nth n ++ str " argument in " ++ brk(1,1) ++ pc ++ str "."
 
 let error_same_names_types id =
   str "The name" ++ spc () ++ pr_id id ++ spc () ++
@@ -944,14 +945,14 @@ let explain_unused_clause env pats =
 (* Without localisation
   let s = if List.length pats > 1 then "s" else "" in
   (str ("Unused clause with pattern"^s) ++ spc () ++
-    hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")")
+    hov 0 (pr_sequence pr_cases_pattern pats) ++ str ")")
 *)
   str "This clause is redundant."
 
 let explain_non_exhaustive env pats =
   str "Non exhaustive pattern-matching: no clause found for " ++
   str (plural (List.length pats) "pattern") ++
-  spc () ++ hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats)
+  spc () ++ hov 0 (pr_sequence pr_cases_pattern pats)
 
 let explain_cannot_infer_predicate env typs =
   let env = make_all_name_different env in
@@ -960,7 +961,7 @@ let explain_cannot_infer_predicate env typs =
     str "For " ++ pr_lconstr_env env cstr ++ str ": " ++ pr_lconstr_env env typ
   in
   str "Unable to unify the types found in the branches:" ++
-  spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs))
+  spc () ++ hov 0 (prlist_with_sep fnl pr_branch (Array.to_list typs))
 
 let explain_pattern_matching_error env = function
   | BadPattern (c,t) ->
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index a763472b93..7607bda42c 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -38,7 +38,7 @@ val explain_reduction_tactic_error :
   Tacred.reduction_tactic_error -> std_ppcmds
 
 val explain_ltac_call_trace :
-  int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Util.loc ->
+  int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Pp.loc ->
   std_ppcmds
 
 val explain_module_error : Modops.module_typing_error -> std_ppcmds
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 1584411906..4f365ebcf3 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.ml
@@ -9,6 +9,7 @@
 open Vernacexpr
 open Names
 open Compat
+open Errors
 open Util
 open Pp
 open Printer
@@ -274,7 +275,7 @@ let compute_reset_info () =
 
 let coqide_cmd_checks (loc,ast) =
   let user_error s =
-    raise (Loc.Exc_located (loc, Util.UserError ("CoqIde", str s)))
+    raise (Loc.Exc_located (loc, Errors.UserError ("CoqIde", str s)))
   in
   if is_vernac_debug_command ast then
     user_error "Debug mode not available within CoqIDE";
@@ -504,7 +505,7 @@ let eval_call c =
       | Vernac.DuringCommandInterp (_,inner) -> handle_exn inner
       | Error_in_file (_,_,inner) -> None, pr_exn inner
       | Loc.Exc_located (loc, inner) when loc = dummy_loc -> None, pr_exn inner
-      | Loc.Exc_located (loc, inner) -> Some (Util.unloc loc), pr_exn inner
+      | Loc.Exc_located (loc, inner) -> Some (Pp.unloc loc), pr_exn inner
       | e -> None, pr_exn e
   in
   let interruptible f x =
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index de3b62f827..d8b503f958 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -18,6 +18,7 @@ open Libobject
 open Nameops
 open Declarations
 open Term
+open Errors
 open Util
 open Declare
 open Entries
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 51eddbae9f..640ef4ab51 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -16,6 +16,7 @@
 
 open Pp
 open Flags
+open Errors
 open Util
 open Names
 open Declarations
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index 87aedc7bea..21e39e0ca4 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Pp
 open Names
 open Term
 open Environ
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 7704449f52..2d46334270 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -9,6 +9,7 @@
 (* Created by Hugo Herbelin from contents related to lemma proofs in
    file command.ml, Aug 2009 *)
 
+open Errors
 open Util
 open Flags
 open Pp
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6a4d72516a..76326f51ff 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -9,6 +9,7 @@
 open Pp
 open Flags
 open Compat
+open Errors
 open Util
 open Names
 open Topconstr
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 4ee1310a00..74a8e0fe9c 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 025c972fe9..da9575ca6e 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Flags
@@ -326,10 +327,10 @@ let declare_ml_modules local l =
 let print_ml_path () =
   let l = !coq_mlpath_copy in
   ppnl (str"ML Load Path:" ++ fnl () ++ str"  " ++
-          hv 0 (prlist_with_sep pr_fnl pr_str l))
+          hv 0 (prlist_with_sep fnl str l))
 
 	  (* Printing of loaded ML modules *)
 
 let print_ml_modules () =
   let l = get_loaded_modules () in
-  pp (str"Loaded ML Modules: " ++ pr_vertical_list pr_str l)
+  pp (str"Loaded ML Modules: " ++ pr_vertical_list str l)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 64942a5d2d..0ddc59c50a 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Libnames
@@ -148,7 +149,7 @@ let subst_projection fid l c =
 	    | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k
 	    | NoProjection Anonymous ->
                 errorlabstrm "" (str "Field " ++ pr_id fid ++
-                  str " depends on the " ++ str (ordinal (k-depth-1)) ++ str
+                  str " depends on the " ++ pr_nth (k-depth-1) ++ str
                   " field which has no name.")
         else
 	  mkRel (k-lv)
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 33e8e51dba..2213d25f9a 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
@@ -170,7 +171,7 @@ let raw_search_rewrite extra_filter display_function pattern =
     display_function gref_eq
 
 let raw_search_by_head extra_filter display_function pattern =
-  Util.todo "raw_search_by_head"
+  Errors.todo "raw_search_by_head"
 
 let name_of_reference ref = string_of_id (basename_of_global ref)
 
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 699fd12f9d..5187b3a28e 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Flags
 open Cerrors
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index cbd95a4fb9..60354f4cf8 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -10,6 +10,7 @@
 
 open Pp
 open Lexer
+open Errors
 open Util
 open Flags
 open System
@@ -22,7 +23,7 @@ open Compat
    Use the module Coqtoplevel, which catches these exceptions
    (the exceptions are explained only at the toplevel). *)
 
-exception DuringCommandInterp of Util.loc * exn
+exception DuringCommandInterp of Pp.loc * exn
 
 exception HasNotFailed
 
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index d89e90d0c6..1cfd94e056 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -12,16 +12,16 @@
    Raises [End_of_file] if EOF (or Ctrl-D) is reached. *)
 
 val parse_sentence : Pcoq.Gram.parsable * in_channel option ->
- Util.loc * Vernacexpr.vernac_expr
+ Pp.loc * Vernacexpr.vernac_expr
 
 (** Reads and executes vernac commands from a stream.
    The boolean [just_parsing] disables interpretation of commands. *)
 
-exception DuringCommandInterp of Util.loc * exn
+exception DuringCommandInterp of Pp.loc * exn
 exception End_of_input
 
 val just_parsing : bool ref
-val eval_expr : Util.loc * Vernacexpr.vernac_expr -> unit
+val eval_expr : Pp.loc * Vernacexpr.vernac_expr -> unit
 val raw_do_vernac : Pcoq.Gram.parsable -> unit
 
 (** Set XML hooks *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f7466d0371..a7b4a175fa 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -9,6 +9,7 @@
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
 open Pp
+open Errors
 open Util
 open Flags
 open Names
@@ -65,7 +66,7 @@ let show_proof () =
   (* spiwack: this would probably be cooler with a bit of polishing. *)
   let p = Proof_global.give_me_the_proof () in
   let pprf = Proof.partial_proof p in
-  msgnl (Util.prlist_with_sep Pp.fnl Printer.pr_constr pprf)
+  msgnl (Pp.prlist_with_sep Pp.fnl Printer.pr_constr pprf)
 
 let show_node () =
   (* spiwack: I'm have little clue what this function used to do. I deactivated it, 
@@ -163,7 +164,7 @@ let print_loadpath dir =
     | Some dir -> List.filter (fun (s,l) -> is_dirpath_prefix_of dir l) l in
   msgnl (Pp.t (str "Logical Path:                 " ++
 		 tab () ++ str "Physical path:" ++ fnl () ++
-		 prlist_with_sep pr_fnl print_path_entry l))
+		 prlist_with_sep fnl print_path_entry l))
 
 let print_modules () =
   let opened = Library.opened_libraries ()
@@ -419,14 +420,14 @@ let vernac_inductive finite infer indl =
 	  (((coe', AssumExpr ((loc, Name id), ce)), None), [])
       in vernac_record (Class true) finite infer id bl c None [f]
   | [ ( id , bl , c , Class true, _), _ ] ->
-      Util.error "Definitional classes must have a single method"
+      Errors.error "Definitional classes must have a single method"
   | [ ( id , bl , c , Class false, Constructors _), _ ] ->
-      Util.error "Inductive classes not supported"
+      Errors.error "Inductive classes not supported"
   | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] ->
-      Util.error "where clause not supported for (co)inductive records"
+      Errors.error "where clause not supported for (co)inductive records"
   | _ -> let unpack = function
       | ( (_, id) , bl , c , _ , Constructors l ) , ntn  -> ( id , bl , c , l ) , ntn
-      | _ -> Util.error "Cannot handle mutually (co)inductive records."
+      | _ -> Errors.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
     do_mutual_inductive indl (recursivity_flag_of_kind finite)
@@ -1416,7 +1417,7 @@ let vernac_show = function
   | ShowExistentials -> show_top_evars ()
   | ShowTree -> show_prooftree ()
   | ShowProofNames ->
-      msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names()))
+      msgnl (pr_sequence pr_id (Pfedit.get_all_proof_names()))
   | ShowIntros all -> show_intro all
   | ShowMatch id -> show_match id
   | ShowThesis -> show_thesis ()
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 8fb6f4668c..2b6a881d49 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -51,7 +51,7 @@ val abort_refine : ('a -> unit) -> 'a -> unit;;
 
 val interp : Vernacexpr.vernac_expr -> unit
 
-val vernac_reset_name : identifier Util.located -> unit
+val vernac_reset_name : identifier Pp.located -> unit
 
 val vernac_backtrack : int -> int -> int -> unit
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 78207f6a24..155feaf623 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -7,6 +7,8 @@
 (************************************************************************)
 
 open Compat
+open Errors
+open Pp
 open Util
 open Names
 open Tacexpr
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 10c5a00f68..c8d6d87ffa 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index aa38e9e9f4..332d30536c 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -10,7 +10,7 @@
 
 open Flags
 open Pp
-open Util
+open Errors
 open System
 open Names
 open Term