remove many excessive open Util & Errors in mli's

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15392 85f007b7-540e-0410-9357-904b9bb8a0f7

46 files changed, 2 insertions, 83 deletions

diff --git a/checker/declarations.mli b/checker/declarations.mli
index 56a77571e..7dfe609c3 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -1,5 +1,3 @@
-open Errors
-open Util
 open Names
 open Term
 
diff --git a/checker/modops.mli b/checker/modops.mli
index 5ac2fde50..53baaef67 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 (*i*)
-open Errors
-open Util
 open Names
 open Univ
 open Term
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 868d53f33..161320626 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Util
 open Names
 open Libnames
 open Misctypes
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index a77b1060c..8146c4715 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -12,7 +12,6 @@ open Globnames
 open Nametab
 open Term
 open Pattern
-open Errors
 open Util
 
 (** This module collects the global references, constructions and
diff --git a/interp/notation.mli b/interp/notation.mli
index 668d827f5..7629d86e7 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Pp
 open Bigint
 open Names
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index 9dfc656a0..dee1203b3 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Names
 open Notation_term
 open Misctypes
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index f0a45389a..d977a728d 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
 open Notation_term
 open Glob_term
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 482d409ba..bd9e776c9 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
 open Names
 open Libnames
 open Glob_term
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 9f8a306fa..eca482a46 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
 open Univ
 open Environ
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 0d279bc39..0cb9292cd 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
 open Sign
 open Univ
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 4027d9fad..800e2eaa8 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
 open Names
 open Entries
 open Environ
diff --git a/library/globnames.mli b/library/globnames.mli
index b41d04970..5728a3ebc 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
 open Names
 open Term
 open Mod_subst
diff --git a/library/goptions.mli b/library/goptions.mli
index bf894d9c8..a90689dfc 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -44,8 +44,6 @@
    (synchronous = consistent with the resetting commands)                   *)
 
 open Pp
-open Errors
-open Util
 open Names
 open Libnames
 open Term
diff --git a/library/libnames.mli b/library/libnames.mli
index 0fe687343..24bdd2048 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
 open Names
 
 (** {6 Dirpaths } *)
diff --git a/library/library.mli b/library/library.mli
index 95e4a6eb0..766e22afa 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Pp
 open Names
 open Libnames
diff --git a/library/nametab.mli b/library/nametab.mli
index fe59ffad6..871ed6676 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Pp
 open Names
 open Libnames
diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli
index 3043fd04b..210e4cd5f 100644
--- a/parsing/extrawit.mli
+++ b/parsing/extrawit.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Genarg
 open Tacexpr
 
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index eda9cea49..95eadfcb6 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
 
 val add_keyword : string -> unit
 val remove_keyword : string -> unit
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 5d12af054..147c5261d 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
 open Names
 open Glob_term
 open Extend
@@ -156,7 +155,6 @@ val create_generic_entry : string -> ('a, rlevel) abstract_argument_type ->
 
 module Prim :
   sig
-    open Util
     open Names
     open Libnames
     val preident : string Gram.entry
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index d530495f8..78dbee3fe 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Util
 open Term
 open Names
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index f96447c15..b733ac50f 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -9,8 +9,6 @@
 (*s Target language for extraction: a core ML called MiniML. *)
 
 open Pp
-open Errors
-open Util
 open Names
 open Globnames
 
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 30f1df45d..fadceabb2 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
 open Term
 open Globnames
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 8a2406e36..9f13e54cf 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Term
-open Errors
-open Util
 open Formula
 open Tacmach
 open Names
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 654d42ee1..bb3071782 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,5 +1,3 @@
-open Errors
-open Util
 open Names
 open Term
 open Pp
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index d0dd870de..7add91c16 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Pp
 open Names
 open Term
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 45566e9fb..b2e41841e 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Pp
 open Evd
 open Names
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 82d154d39..ea0f063fe 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Pp
 open Util
 open Names
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ca552a450..70a18b54a 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
 open Names
 open Term
 open Sign
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 19d003a92..6a26fe1d4 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Pp
-open Util
 open Names
 open Sign
 open Term
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 7debe2b0d..2410fb7ca 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
 open Names
 open Term
 open Sign
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index e5dc2448b..d2141c50e 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
 open Util
 open Pp
 open Names
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 6c97516ca..411651afe 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -16,8 +16,6 @@ open Environ
 open Nametab
 open Mod_subst
 open Topconstr
-open Errors
-open Util
 
 type direction = Forward | Backward
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 925222766..a05258de7 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -15,7 +15,6 @@ open Environ
 open Nametab
 open Mod_subst
 open Constrexpr
-open Errors
 open Pp
 open Globnames
 
diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli
index 91bb19a8c..992b5a742 100644
--- a/printing/ppvernac.mli
+++ b/printing/ppvernac.mli
@@ -12,8 +12,6 @@ open Vernacexpr
 open Names
 open Nameops
 open Nametab
-open Errors
-open Util
 open Ppconstr
 open Pptactic
 open Glob_term
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index e0ad1acf9..fff826a25 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
 open Term
 open Sign
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index a14f261e9..79998cf28 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
 open Term
 open Sign
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 9b92893a7..583e40c00 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Pp
 open Names
 open Term
diff --git a/tactics/auto.mli b/tactics/auto.mli
index e34141446..67e4dac97 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
 open Term
 open Sign
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 098e92721..cd04181c0 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -8,7 +8,6 @@
 
 (*i*)
 open Pp
-open Util
 open Names
 open Term
 open Sign
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index e4ae55409..1a802df82 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
 open Term
 open Sign
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 35e0c456b..d1fe9de11 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
 open Names
 open Proof_type
 open Tacmach
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index d4cbc6e5b..3c1beda40 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -7,8 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Errors
-open Util
 open Names
 open Term
 open Sign
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 7294a319d..2cbefb817 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Pp
-open Util
 open Names
 open Term
 open Environ
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 1d686b5da..75d742ce1 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -6,13 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
-open Errors
-open Util
-
 (** Error report. *)
 
-val print_loc : loc -> std_ppcmds
+val print_loc : Pp.loc -> Pp.std_ppcmds
 
 (** Pre-explain a vernac interpretation error *)
 
@@ -21,5 +17,5 @@ val process_vernac_interp_error : exn -> exn
 (** General explain function. Should not be used directly now,
     see instead function [Errors.print] and variants *)
 
-val explain_exn_default : exn -> std_ppcmds
+val explain_exn_default : exn -> Pp.std_ppcmds
 
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index d3be9c016..c22861842 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -15,8 +15,6 @@ open Environ
 open Nametab
 open Mod_subst
 open Constrexpr
-open Errors
-open Util
 open Typeclasses
 open Implicit_quantifiers
 open Libnames
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index b49455221..deed9d035 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
 open Names
 open Libnames
 open Tacexpr