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

11 files changed, 12 insertions, 1 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 0bd5b8434..1b443f753 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 73062328b..7c517dd9b 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -11,6 +11,7 @@ open Declarations
 open Names
 open Libnames
 open Pp
+open Errors
 open Util
 open Miniml
 open Table
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 219b3913f..d9ee92c05 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 96731ed27..fe249cd65 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -9,6 +9,7 @@
 (*s Production of Haskell syntax. *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 5a19cc3f5..a5b57a474 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -9,6 +9,7 @@
 (*s Target language for extraction: a core ML called MiniML. *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index c244e046d..f03170948 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -8,6 +8,7 @@
 
 (*i*)
 open Pp
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 029e8cf46..630db6f06 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 9e8dd8286..123edd4c3 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -10,6 +10,7 @@ open Names
 open Declarations
 open Environ
 open Libnames
+open Errors
 open Util
 open Miniml
 open Table
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index ed69ec457..d99bca6f4 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -9,6 +9,7 @@
 (*s Production of Ocaml syntax. *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 215076555..157788ece 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -9,6 +9,7 @@
 (*s Production of Scheme syntax. *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 238befd25..667182480 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -15,6 +15,7 @@ open Summary
 open Libobject
 open Goptions
 open Libnames
+open Errors
 open Util
 open Pp
 open Miniml
@@ -337,7 +338,7 @@ let warning_both_mod_and_cst q mp r =
 
 let error_axiom_scheme r i =
   err (str "The type scheme axiom " ++ spc () ++
-       safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++
+       safe_pr_global r ++ spc () ++ str "needs " ++ int i ++
        str " type variable(s).")
 
 let check_inside_module () =