From 5105781ae0c92dd1dc83ca209c0312725065e96d Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 29 May 2012 11:09:35 +0000 Subject: 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 --- checker/declarations.mli | 2 -- checker/modops.mli | 2 -- interp/constrexpr_ops.mli | 1 - interp/coqlib.mli | 1 - interp/notation.mli | 2 -- interp/notation_ops.mli | 1 - interp/syntax_def.mli | 2 -- interp/topconstr.mli | 1 - kernel/modops.mli | 2 -- kernel/pre_env.mli | 2 -- library/declaremods.mli | 2 -- library/globnames.mli | 2 -- library/goptions.mli | 2 -- library/libnames.mli | 2 -- library/library.mli | 1 - library/nametab.mli | 2 -- parsing/extrawit.mli | 2 -- parsing/lexer.mli | 2 -- parsing/pcoq.mli | 2 -- plugins/cc/ccalgo.mli | 1 - plugins/extraction/miniml.mli | 2 -- plugins/extraction/mlutil.mli | 2 -- plugins/firstorder/sequent.mli | 2 -- plugins/funind/indfun.mli | 2 -- pretyping/cases.mli | 1 - pretyping/coercion.mli | 1 - pretyping/evarutil.mli | 1 - pretyping/evd.mli | 2 -- pretyping/glob_ops.mli | 2 -- pretyping/pretype_errors.mli | 2 -- pretyping/termops.mli | 1 - pretyping/typeclasses.mli | 2 -- pretyping/typeclasses_errors.mli | 1 - printing/ppvernac.mli | 2 -- proofs/clenv.mli | 2 -- proofs/clenvtac.mli | 2 -- proofs/pfedit.mli | 2 -- tactics/auto.mli | 2 -- tactics/equality.mli | 1 - tactics/hipattern.mli | 2 -- tactics/tacinterp.mli | 2 -- tactics/tacticals.mli | 2 -- tactics/tactics.mli | 1 - toplevel/cerrors.mli | 8 ++------ toplevel/classes.mli | 2 -- toplevel/metasyntax.mli | 2 -- 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 -- cgit v1.2.3