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

19 files changed, 34 insertions, 16 deletions

diff --git a/plugins/subtac/eterm.ml b/plugins/subtac/eterm.ml
index f4d8b769cf..0bde8dca9c 100644
--- a/plugins/subtac/eterm.ml
+++ b/plugins/subtac/eterm.ml
@@ -11,6 +11,7 @@ open Names
 open Evd
 open List
 open Pp
+open Errors
 open Util
 open Subtac_utils
 open Proof_type
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index 03d76f29a6..4812fe0a6b 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.mli
@@ -11,6 +11,7 @@ open Tacmach
 open Term
 open Evd
 open Names
+open Pp
 open Util
 open Tacinterp
 
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index c37f0db5ad..27de89f673 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.ml4
@@ -14,7 +14,8 @@
 
 
 open Flags
-open Util
+open Errors
+open Pp
 open Names
 open Nameops
 open Vernacentries
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 710149ae4f..cccb12e418 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -9,6 +9,7 @@
 open Compat
 open Global
 open Pp
+open Errors
 open Util
 open Names
 open Sign
diff --git a/plugins/subtac/subtac.mli b/plugins/subtac/subtac.mli
index b51150aa0e..32d4840912 100644
--- a/plugins/subtac/subtac.mli
+++ b/plugins/subtac/subtac.mli
@@ -1,2 +1,2 @@
 val require_library : string -> unit
-val subtac : Util.loc * Vernacexpr.vernac_expr -> unit
+val subtac : Pp.loc * Vernacexpr.vernac_expr -> unit
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 16d4e21ee5..d60841e72a 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Cases
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli
index 77537d33a3..11a8115971 100644
--- a/plugins/subtac/subtac_cases.mli
+++ b/plugins/subtac/subtac_cases.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index cac0988c01..a81243f73f 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -22,6 +22,7 @@ open Typeclasses
 open Typeclasses_errors
 open Decl_kinds
 open Entries
+open Errors
 open Util
 
 module SPretyping = Subtac_pretyping.Pretyping
@@ -71,8 +72,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 		let t =
 		  if b then
 		    let _k = class_info cl in
-		      CHole (Util.dummy_loc, Some Evd.InternalHole)
-		  else CHole (Util.dummy_loc, None)
+		      CHole (Pp.dummy_loc, Some Evd.InternalHole)
+		  else CHole (Pp.dummy_loc, None)
 		in t, avoid
 	    | None -> failwith ("new instance: under-applied typeclass"))
 	  cl
@@ -149,7 +150,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
 		      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/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index 5b5c02037a..5b8636a126 100644
--- a/plugins/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_classes.mli
@@ -16,6 +16,7 @@ open Environ
 open Nametab
 open Mod_subst
 open Topconstr
+open Errors
 open Util
 open Typeclasses
 open Implicit_quantifiers
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index eb29bd045a..3cbf9fcabe 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -5,6 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index ecae6759f0..e5d93ace26 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -9,6 +9,7 @@ open Pp
 open Glob_term
 open Sign
 open Tacred
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/plugins/subtac/subtac_errors.ml b/plugins/subtac/subtac_errors.ml
index 067da150ec..f07bbeb436 100644
--- a/plugins/subtac/subtac_errors.ml
+++ b/plugins/subtac/subtac_errors.ml
@@ -1,3 +1,4 @@
+open Errors
 open Util
 open Pp
 open Printer
diff --git a/plugins/subtac/subtac_errors.mli b/plugins/subtac/subtac_errors.mli
index 8d75b9c017..c65203075a 100644
--- a/plugins/subtac/subtac_errors.mli
+++ b/plugins/subtac/subtac_errors.mli
@@ -1,13 +1,13 @@
 type term_pp = Pp.std_ppcmds
 type subtyping_error =
-    UncoercibleInferType of Util.loc * term_pp * term_pp
-  | UncoercibleInferTerm of Util.loc * term_pp * term_pp * term_pp * term_pp
+    UncoercibleInferType of Pp.loc * term_pp * term_pp
+  | UncoercibleInferTerm of Pp.loc * term_pp * term_pp * term_pp * term_pp
   | UncoercibleRewrite of term_pp * term_pp
 type typing_error =
-    NonFunctionalApp of Util.loc * term_pp * term_pp * term_pp
-  | NonConvertible of Util.loc * term_pp * term_pp
-  | NonSigma of Util.loc * term_pp
-  | IllSorted of Util.loc * term_pp
+    NonFunctionalApp of Pp.loc * term_pp * term_pp * term_pp
+  | NonConvertible of Pp.loc * term_pp * term_pp
+  | NonSigma of Pp.loc * term_pp
+  | IllSorted of Pp.loc * term_pp
 exception Subtyping_error of subtyping_error
 exception Typing_error of typing_error
 exception Debug_msg of string
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 6a5878b3e8..527c5e0847 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -11,6 +11,7 @@ open Summary
 open Libobject
 open Entries
 open Decl_kinds
+open Errors
 open Util
 open Evd
 open Declare
@@ -18,7 +19,7 @@ open Proof_type
 open Compat
 
 let ppwarn cmd = Pp.warn (str"Program:" ++ cmd)
-let pperror cmd = Util.errorlabstrm "Program" cmd
+let pperror cmd = Errors.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
 let reduce c =
@@ -551,7 +552,7 @@ and solve_obligation_by_tac prg obls i tac =
 	| Loc.Exc_located(_, Refiner.FailError (_, s))
 	| Refiner.FailError (_, s) ->
 	    user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
-	| Util.Anomaly _ as e -> raise e
+	| Errors.Anomaly _ as e -> raise e
 	| e -> false
 
 and solve_prg_obligations prg ?oblset tac =
diff --git a/plugins/subtac/subtac_obligations.mli b/plugins/subtac/subtac_obligations.mli
index c1d665aaca..284e975dbd 100644
--- a/plugins/subtac/subtac_obligations.mli
+++ b/plugins/subtac/subtac_obligations.mli
@@ -1,4 +1,5 @@
 open Names
+open Pp
 open Util
 open Libnames
 open Evd
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 7c0d123259..c8acf7e0bb 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.ml
@@ -8,6 +8,7 @@
 
 open Global
 open Pp
+open Errors
 open Util
 open Names
 open Sign
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 528a2e6832..fbeed381d3 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -8,6 +8,7 @@
 
 open Pp
 open Compat
+open Errors
 open Util
 open Names
 open Sign
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 28bbdd35e9..0ed78a23b6 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -5,6 +5,8 @@ open Libnames
 open Coqlib
 open Term
 open Names
+open Errors
+open Pp
 open Util
 
 let ($) f x = f x
@@ -426,7 +428,7 @@ let pr_meta_map evd =
   in
   prlist pr_meta_binding ml
 
-let pr_idl idl = prlist_with_sep pr_spc pr_id idl
+let pr_idl idl = pr_sequence pr_id idl
 
 let pr_evar_info evi =
   let phyps =
@@ -443,14 +445,14 @@ let pr_evar_info evi =
 
 let pr_evar_map sigma =
   h 0
-    (prlist_with_sep pr_fnl
+    (prlist_with_sep fnl
       (fun (ev,evi) ->
         h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
       (to_list sigma))
 
 let pr_constraints pbs =
   h 0
-    (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
+    (prlist_with_sep fnl (fun (pbty,t1,t2) ->
       Termops.print_constr t1 ++ spc() ++
       str (match pbty with
 	| Reduction.CONV -> "=="
diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli
index de96cc602e..70ad0bcc82 100644
--- a/plugins/subtac/subtac_utils.mli
+++ b/plugins/subtac/subtac_utils.mli
@@ -7,6 +7,7 @@ open Evd
 open Decl_kinds
 open Topconstr
 open Glob_term
+open Errors
 open Util
 open Evarutil
 open Names