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 bb42b949d..6f01107f5 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 08dd78bcb..99b952a38 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 5f28269ee..cdb0ade74 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 34ba7b010..4da4d14e1 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 033e2bd73..069b82017 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 890996d10..ba56c243f 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 90beb326b..56a77571e 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 99b364579..d0b0b4ce9 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 1e773df65..e48fdb6ef 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 7a04cbfa3..67f61f161 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 9942816d1..cc9ca9031 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 2dc5d062c..4212a9361 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 5ed7b0ce2..5ac2fde50 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 3aeaa1023..c1eadcd64 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 bc067dc5f..57a9011cf 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 0c97254b5..8fb4eb34b 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 ab40b6fa7..db4b6599b 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 5226db534..b904e0b68 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