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

24 files changed, 29 insertions, 6 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index adc7f8edc..e047b62a6 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -14,6 +14,7 @@
 (* Initial author: Arnaud Spiwack
    Module-traversing code: Pierre Letouzey *)
 
+open Errors
 open Util
 open Names
 open Sign
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index ba40f98c0..e8734cbaa 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Libnames
 
diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli
index 88ef763c9..5b81d54ee 100644
--- a/library/decl_kinds.mli
+++ b/library/decl_kinds.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Libnames
 
diff --git a/library/declare.ml b/library/declare.ml
index 288580850..fd3139cf6 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -9,6 +9,7 @@
 (** This module is about the low-level declaration of logical objects *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Libnames
@@ -277,7 +278,7 @@ let declare_mind isrecord mie =
 
 (* Declaration messages *)
 
-let pr_rank i = str (ordinal (i+1))
+let pr_rank i = pr_nth (i+1)
 
 let fixpoint_message indexes l =
   Flags.if_verbose msgnl (match l with
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 90d4245a4..122404e22 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Declarations
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 9d44ba973..4027d9fad 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Pp
+open Errors
 open Util
 open Names
 open Entries
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index ec92f679a..cd79e598d 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Libnames
 open Names
diff --git a/library/global.ml b/library/global.ml
index ab70bb7c3..926284f91 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Term
diff --git a/library/goptions.ml b/library/goptions.ml
index 5af186899..30804fa5f 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -9,6 +9,7 @@
 (* This module manages customization parameters at the vernacular level     *)
 
 open Pp
+open Errors
 open Util
 open Libobject
 open Names
diff --git a/library/goptions.mli b/library/goptions.mli
index d25c1202f..979bca2d2 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -44,6 +44,7 @@
    (synchronous = consistent with the resetting commands)                   *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/library/heads.ml b/library/heads.ml
index 9f9f1ca25..327b883ee 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/library/impargs.ml b/library/impargs.ml
index ef7f59216..b7dbd05fd 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/library/lib.ml b/library/lib.ml
index 7554fd0bb..b98ad4110 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Libnames
 open Nameops
diff --git a/library/lib.mli b/library/lib.mli
index 0d6eb34b8..0a445f076 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -154,9 +154,9 @@ val close_section : unit -> unit
 (** {6 Backtracking (undo). } *)
 
 val reset_to : Libnames.object_name -> unit
-val reset_name : Names.identifier Util.located -> unit
-val remove_name : Names.identifier Util.located -> unit
-val reset_mod : Names.identifier Util.located -> unit
+val reset_name : Names.identifier Pp.located -> unit
+val remove_name : Names.identifier Pp.located -> unit
+val reset_mod : Names.identifier Pp.located -> unit
 
 (** [back n] resets to the place corresponding to the {% $ %}n{% $ %}-th call of
    [mark_end_of_command] (counting backwards) *)
diff --git a/library/libnames.ml b/library/libnames.ml
index b91d24bd6..24f083887 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
diff --git a/library/libnames.mli b/library/libnames.mli
index 18b6ac49a..d3eed0364 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 open Term
diff --git a/library/libobject.ml b/library/libobject.ml
index bc62913d9..b201c63a3 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Names
 open Libnames
diff --git a/library/library.ml b/library/library.ml
index 376228748..e2adb3fb9 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 
 open Names
diff --git a/library/library.mli b/library/library.mli
index ed17ed15b..c569ff485 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -6,7 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
+open Errors
+open Pp
 open Names
 open Libnames
 open Libobject
diff --git a/library/nameops.ml b/library/nameops.ml
index 799b8ebe1..ac163d3ef 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 open Names
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 6dbd927d8..42edb156f 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Compat
 open Pp
diff --git a/library/nametab.mli b/library/nametab.mli
index c5b55f2ca..5183abbe8 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Errors
 open Util
 open Pp
 open Names
diff --git a/library/states.ml b/library/states.ml
index c88858f7e..82146f6b1 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -22,7 +22,7 @@ let (extern_state,intern_state) =
     extern_intern Coq_config.state_magic_number ".coq" in
   (fun s ->
     if !Flags.load_proofs <> Flags.Force then
-      Util.error "Write State only works with option -force-load-proofs";
+      Errors.error "Write State only works with option -force-load-proofs";
     raw_extern s (freeze())),
   (fun s ->
     unfreeze
diff --git a/library/summary.ml b/library/summary.ml
index 697f57e8e..d2168540b 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 open Pp
+open Errors
 open Util
 
 type 'a summary_declaration = {