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 56a77571e7..7dfe609c35 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 5ac2fde502..53baaef672 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 868d53f33f..1613206267 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 a77b1060ca..8146c47157 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 668d827f5b..7629d86e75 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 9dfc656a0c..dee1203b3f 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 f0a45389a9..d977a728d9 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 482d409ba9..bd9e776c9e 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 9f8a306fa9..eca482a460 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 0d279bc39d..0cb9292cdd 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 4027d9fada..800e2eaa89 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 b41d049706..5728a3ebc2 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 bf894d9c89..a90689dfce 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 0fe6873433..24bdd20489 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 95e4a6eb0e..766e22afad 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 fe59ffad6f..871ed66766 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 3043fd04b2..210e4cd5f2 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 eda9cea49b..95eadfcb67 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 5d12af0548..147c5261d9 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 d530495f88..78dbee3fe8 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 f96447c156..b733ac50f3 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 30f1df45dd..fadceabb2a 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 8a2406e364..9f13e54cf0 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 654d42ee16..bb3071782e 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 d0dd870de0..7add91c161 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 45566e9fbc..b2e41841ee 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 82d154d399..ea0f063fe4 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 ca552a450b..70a18b54af 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 19d003a92c..6a26fe1d43 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 7debe2b0d1..2410fb7ca2 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 e5dc2448bc..d2141c50ed 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 6c97516cad..411651afe5 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 925222766a..a05258de75 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 91bb19a8c6..992b5a7422 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 e0ad1acf9a..fff826a25b 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 a14f261e90..79998cf285 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 9b92893a7d..583e40c00b 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 e341414466..67e4dac97e 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 098e927219..cd04181c02 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 e4ae554091..1a802df829 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 35e0c456ba..d1fe9de115 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 d4cbc6e5b2..3c1beda400 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 7294a319de..2cbefb8178 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 1d686b5dab..75d742ce18 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 d3be9c0160..c22861842f 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 b49455221e..deed9d0359 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