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

18 files changed, 21 insertions, 3 deletions

diff --git a/checker/check.ml b/checker/check.ml
index bb42b949d0..6f01107f5c 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 
diff --git a/checker/check.mllib b/checker/check.mllib
index 08dd78bcb7..99b952a389 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -1,10 +1,11 @@
 Coq_config
 Pp_control
-Pp
 Compat
 Flags
+Pp
 Segmenttree
 Unicodetable
+Errors
 Util
 Option
 Hashcons
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 5f28269ee7..cdb0ade744 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open System
 open Flags
diff --git a/checker/checker.ml b/checker/checker.ml
index 34ba7b0101..4da4d14e13 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -8,6 +8,7 @@
 
 open Compat
 open Pp
+open Errors
 open Util
 open System
 open Flags
diff --git a/checker/closure.ml b/checker/closure.ml
index 033e2bd731..069b820176 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Term
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 890996d105..ba56c243fb 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -1,3 +1,4 @@
+open Errors
 open Util
 open Names
 open Term
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 90beb326bf..56a77571e7 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -1,3 +1,4 @@
+open Errors
 open Util
 open Names
 open Term
diff --git a/checker/environ.ml b/checker/environ.ml
index 99b3645794..d0b0b4ce95 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -1,3 +1,4 @@
+open Errors
 open Util
 open Names
 open Univ
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 1e773df65c..e48fdb6ef0 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Univ
diff --git a/checker/inductive.ml b/checker/inductive.ml
index 7a04cbfa3b..67f61f161c 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Univ
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 9942816d12..cc9ca90310 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -1,5 +1,6 @@
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/checker/modops.ml b/checker/modops.ml
index 2dc5d062cf..4212a93615 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Errors
 open Util
 open Pp
 open Names
diff --git a/checker/modops.mli b/checker/modops.mli
index 5ed7b0ce2e..5ac2fde502 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Errors
 open Util
 open Names
 open Univ
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 3aeaa10232..c1eadcd64a 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index bc067dc5f3..57a9011cfd 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Declarations
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 0c97254b56..8fb4eb34ba 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Errors
 open Util
 open Names
 open Univ
@@ -261,7 +262,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
 		let c2 = force_constr lc2 in
 		check_conv conv env c1 c2))
       | IndType ((kn,i),mind1) ->
-	  ignore (Util.error (
+	  ignore (Errors.error (
 		    "The kernel does not recognize yet that a parameter can be " ^
 		      "instantiated by an inductive type. Hint: you can rename the " ^
 		      "inductive type and give a definition to map the old name to the new " ^
@@ -272,7 +273,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
       let typ2 = Typeops.type_of_constant_type env cb2.const_type in
        check_conv conv_leq env arity1 typ2
    | IndConstr (((kn,i),j) as cstr,mind1) ->
-      ignore (Util.error (
+      ignore (Errors.error (
        "The kernel does not recognize yet that a parameter can be " ^
        "instantiated by a constructor. Hint: you can rename the " ^
        "constructor and give a definition to map the old name to the new " ^
diff --git a/checker/term.ml b/checker/term.ml
index ab40b6fa75..db4b6599bf 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -8,6 +8,7 @@
 
 (* This module instantiates the structure of generic deBruijn terms to Coq *)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 5226db5349..b904e0b688 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Univ