diff options
| author | Pierre Letouzey | 2014-03-05 14:59:16 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-03-05 15:41:21 +0100 |
| commit | adfd437f8ae6aaf893119fa4730edecf067dede7 (patch) | |
| tree | a395e5f9e50f5cde1419c1fbdb0870d9efdc09b8 | |
| parent | 3080dd5e27ee20ba0b3537c7882e7ad8af414325 (diff) | |
Remove many superfluous 'open' indicated by ocamlc -w +33
With ocaml 4.01, the 'unused open' warning also checks the mli :-)
Beware: some open are reported as useless when compiling with camlp5,
but are necessary for compatibility with camlp4. These open are now
marked with a comment.
222 files changed, 14 insertions, 504 deletions
diff --git a/checker/closure.mli b/checker/closure.mli index bee6b1bb84..13bc0c07e0 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -7,7 +7,6 @@ (************************************************************************) (*i*) -open Pp open Names open Cic open Esubst diff --git a/checker/environ.mli b/checker/environ.mli index 847af52318..a4162d67f2 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -1,6 +1,5 @@ open Names open Cic -open Term (* Environments *) diff --git a/checker/indtypes.mli b/checker/indtypes.mli index 0029eb652b..d757f237d2 100644 --- a/checker/indtypes.mli +++ b/checker/indtypes.mli @@ -8,9 +8,7 @@ (*i*) open Names -open Univ open Cic -open Typeops open Environ (*i*) diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index c2016ba1bf..ec0014175a 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -1,6 +1,5 @@ open Pp -open Errors open Util open Names open Cic diff --git a/checker/modops.ml b/checker/modops.ml index 89ffcb50b3..2d20dd0f30 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -12,7 +12,6 @@ open Util open Pp open Names open Cic -open Term open Declarations (*i*) diff --git a/checker/modops.mli b/checker/modops.mli index 396eb8e7cf..78626eb00d 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -8,7 +8,6 @@ (*i*) open Names -open Univ open Cic open Environ (*i*) diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index b3060c153d..7fcd749f59 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -11,7 +11,6 @@ open Errors open Util open Cic open Names -open Declarations open Environ (************************************************************************) diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index 9f9afe922f..59d95c36d6 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -7,7 +7,6 @@ (************************************************************************) (*i*) -open Names open Cic open Environ (*i*) diff --git a/checker/type_errors.ml b/checker/type_errors.ml index 6cf814dce1..e800ee3ef2 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -8,7 +8,6 @@ open Names open Cic -open Term open Environ type unsafe_judgment = constr * constr diff --git a/checker/typeops.ml b/checker/typeops.ml index f22649eb52..95753769df 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -14,7 +14,6 @@ open Cic open Term open Reduction open Type_errors -open Declarations open Inductive open Environ diff --git a/checker/typeops.mli b/checker/typeops.mli index 3c56c15efa..92535606f9 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -7,9 +7,7 @@ (************************************************************************) (*i*) -open Names open Cic -open Term open Environ (*i*) diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 093a561d6e..98843a40ff 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -232,7 +232,7 @@ let declare_vernac_argument loc s pr cl = open Pcoq open Pcaml -open PcamlSig +open PcamlSig (* necessary for camlp4 *) EXTEND GLOBAL: str_item; diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4 index bfc38feb8b..a731ade686 100644 --- a/grammar/q_constr.ml4 +++ b/grammar/q_constr.ml4 @@ -11,7 +11,7 @@ open Q_util open Compat open Pcaml -open PcamlSig +open PcamlSig (* necessary for camlp4 *) let loc = CompatLoc.ghost let dloc = <:expr< Loc.ghost >> diff --git a/grammar/q_util.mli b/grammar/q_util.mli index 527cc6b2fc..5d9097f38d 100644 --- a/grammar/q_util.mli +++ b/grammar/q_util.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat +open Compat (* necessary for camlp4 *) val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index f96b67f5e9..b5ab3a87bb 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -186,7 +186,7 @@ let declare_tactic loc s c cl = ] open Pcaml -open PcamlSig +open PcamlSig (* necessary for camlp4 *) EXTEND GLOBAL: str_item; diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index ad8929657a..4337793022 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -113,7 +113,7 @@ let declare_command loc s c nt cl = } >> ] open Pcaml -open PcamlSig +open PcamlSig (* necessary for camlp4 *) EXTEND GLOBAL: str_item; diff --git a/ide/gtk_parsing.ml b/ide/gtk_parsing.ml index 05b638a941..f3bb2a2ed4 100644 --- a/ide/gtk_parsing.ml +++ b/ide/gtk_parsing.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Ideutils - let underscore = Glib.Utf8.to_unichar "_" ~pos:(ref 0) let arobase = Glib.Utf8.to_unichar "@" ~pos:(ref 0) let prime = Glib.Utf8.to_unichar "'" ~pos:(ref 0) diff --git a/ide/preferences.ml b/ide/preferences.ml index d9a9d0e3a2..585dce21f4 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -7,7 +7,6 @@ (************************************************************************) open Configwin -open Printf let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc" let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys" diff --git a/ide/utils/editable_cells.ml b/ide/utils/editable_cells.ml index 1ab107c778..33968b8dd0 100644 --- a/ide/utils/editable_cells.ml +++ b/ide/utils/editable_cells.ml @@ -1,4 +1,3 @@ -open GTree open Gobject let create l = diff --git a/ide/wg_ScriptView.ml b/ide/wg_ScriptView.ml index de378c074e..a1a429789d 100644 --- a/ide/wg_ScriptView.ml +++ b/ide/wg_ScriptView.ml @@ -6,10 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Ideutils -open GText -open Gtk_parsing - type insert_action = { ins_val : string; ins_off : int; diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 846fb5b934..37e627a6d4 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -7,16 +7,7 @@ (************************************************************************) open Loc -open Pp -open Names -open Term -open Libnames -open Globnames -open Glob_term -open Genredexpr open Tacexpr -open Pattern -open Constrexpr open Term open Misctypes open Genarg diff --git a/interp/constrarg.mli b/interp/constrarg.mli index c49b61ce78..5faef378a6 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -14,7 +14,6 @@ open Names open Term open Libnames open Globnames -open Glob_term open Genredexpr open Pattern open Constrexpr diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 687f5cb9e5..25194acc93 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -7,12 +7,9 @@ (************************************************************************) open Loc -open Pp open Names open Libnames open Misctypes -open Term -open Mod_subst open Constrexpr (** Constrexpr_ops: utilities on [constr_expr] *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a3410544ef..6a893bde64 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -26,7 +26,6 @@ open Glob_ops open Pattern open Nametab open Notation -open Reserve open Detyping open Misctypes open Decl_kinds diff --git a/interp/constrextern.mli b/interp/constrextern.mli index a98182fb87..e1acb45021 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term open Context @@ -14,7 +13,6 @@ open Termops open Environ open Libnames open Globnames -open Nametab open Glob_term open Pattern open Constrexpr diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 5b5775d1a3..a1faf95e21 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -9,7 +9,6 @@ open Pp open Errors open Util -open Flags open Names open Nameops open Namegen diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 90c3779fc6..a0bcdc4f4e 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -17,7 +17,6 @@ open Glob_term open Pattern open Constrexpr open Notation_term -open Termops open Pretyping open Misctypes open Decl_kinds diff --git a/interp/coqlib.mli b/interp/coqlib.mli index 9e0cfadae9..9b0f8deb9c 100644 --- a/interp/coqlib.mli +++ b/interp/coqlib.mli @@ -9,9 +9,7 @@ open Names open Libnames open Globnames -open Nametab open Term -open Pattern open Util (** This module collects the global references, constructions and diff --git a/interp/genintern.ml b/interp/genintern.ml index bc41c834a8..a8f82d9984 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Util open Names open Mod_subst open Genarg diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 4d4fe91173..2d55a6b63b 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -14,7 +14,6 @@ open Util open Glob_term open Constrexpr open Libnames -open Globnames open Typeclasses open Typeclasses_errors open Pp diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index df29d05926..50c2cfee02 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -8,19 +8,10 @@ open Loc open Names -open Decl_kinds -open Term -open Context -open Evd -open Environ -open Nametab -open Mod_subst open Glob_term open Constrexpr -open Pp open Libnames open Globnames -open Typeclasses val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit diff --git a/interp/modintern.ml b/interp/modintern.ml index 8f8e2df93e..81d0a0f644 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -7,7 +7,6 @@ (************************************************************************) open Declarations -open Entries open Libnames open Constrexpr open Constrintern diff --git a/interp/modintern.mli b/interp/modintern.mli index b6128918c1..a3998cf833 100644 --- a/interp/modintern.mli +++ b/interp/modintern.mli @@ -6,13 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc -open Declarations open Environ open Entries -open Pp -open Libnames -open Names open Constrexpr open Misctypes diff --git a/interp/notation.mli b/interp/notation.mli index a4ca3ffaab..95e176064c 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -9,7 +9,6 @@ open Pp open Bigint open Names -open Nametab open Libnames open Globnames open Constrexpr diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 4f84af5fe3..fd442cdb4e 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -8,7 +8,6 @@ open Names open Notation_term -open Misctypes open Glob_term (** Utilities about [notation_constr] *) diff --git a/interp/ppextend.mli b/interp/ppextend.mli index cae644ab5b..d1bcb0cf18 100644 --- a/interp/ppextend.mli +++ b/interp/ppextend.mli @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Names (** {6 Pretty-print. } *) diff --git a/interp/reserve.ml b/interp/reserve.ml index 6674a8323a..c104d0d155 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -123,8 +123,6 @@ let revert_reserved_type t = let _ = Namegen.set_reserved_typed_name revert_reserved_type -open Glob_term - let default_env () = { ninterp_var_type = Id.Map.empty; ninterp_rec_vars = Id.Map.empty; diff --git a/interp/reserve.mli b/interp/reserve.mli index 8ae55d0961..81590bd1c6 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -7,9 +7,7 @@ (************************************************************************) open Loc -open Pp open Names -open Glob_term open Notation_term val declare_reserved_type : Id.t located list -> notation_constr -> unit diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 5f772c5915..86aa69681d 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -7,7 +7,6 @@ (************************************************************************) open Loc -open Pp open Names open Libnames open Globnames diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 6f2ff6ec48..0f4e8a5885 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Genarg let wit_unit : unit uniform_genarg_type = diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index f3c4a61e62..065cbe3ec4 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -8,9 +8,6 @@ open Names open Notation_term -open Glob_term -open Nametab -open Libnames (** Syntactic definitions. *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index f042de00ff..c85d516675 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -8,11 +8,7 @@ open Loc open Names -open Libnames -open Misctypes -open Decl_kinds open Constrexpr -open Notation_term (** Topconstr *) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 87af636b44..16b1dc5eb1 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -18,7 +18,6 @@ open Pattern open Decl_kinds open Misctypes open Locus -open Pp type 'a or_metaid = AI of 'a | MetaId of Loc.t * string diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index d12204fec0..6a3c1165fe 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -7,8 +7,6 @@ (************************************************************************) open Loc -open Pp -open Util open Names open Tacexpr open Misctypes diff --git a/kernel/closure.mli b/kernel/closure.mli index 161de91cfa..19baedf276 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term open Environ diff --git a/kernel/constr.ml b/kernel/constr.ml index 826c7f6437..cf05fe0139 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -23,12 +23,8 @@ Inductive Constructions (CIC) terms together with constructors, destructors, iterators and basic functions *) -open Errors open Util -open Pp open Names -open Univ -open Esubst type existential_key = Evar.t diff --git a/kernel/cooking.ml b/kernel/cooking.ml index f8724180e4..31e86e8540 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -17,7 +17,6 @@ open Errors open Util open Names open Term -open Context open Declarations open Environ diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 8493b81d82..030e888294 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -6,11 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Declarations open Environ -open Univ (** {6 Cooking the constants. } *) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index ce789b00eb..016a1a5b55 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -7,12 +7,10 @@ (************************************************************************) open Names -open Univ open Term open Declarations open Environ open Entries -open Typeops (** Inductive type checking and errors *) diff --git a/kernel/modops.ml b/kernel/modops.ml index 2bd421bb3c..188bff626d 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -15,7 +15,6 @@ (* This file provides with various operations on modules and module types *) -open Errors open Util open Names open Term diff --git a/kernel/modops.mli b/kernel/modops.mli index f50dcfd637..a71e28d6e4 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Univ open Term open Environ open Declarations diff --git a/kernel/names.ml b/kernel/names.ml index 047d8a88d6..3de12b1bc3 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -19,7 +19,6 @@ Élie Soubiran, ... *) open Pp -open Errors open Util (** {6 Identifiers } *) @@ -485,8 +484,6 @@ module KerPair = struct the same user part implies having the same canonical part (invariant of the system). *) - open Hashset.Combine - let hash = function | Same kn -> KerName.hash kn | Dual (kn, _) -> KerName.hash kn diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 3435e1d753..82786df64c 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -7,15 +7,11 @@ (************************************************************************) open Errors open Names -open Term open Univ -open Pre_env open Nativelib open Reduction -open Declarations open Util open Nativevalues -open Nativelambda open Nativecode (** This module implements the conversion test by compiling to OCaml code *) diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 2481300763..69b9d22ec7 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Term -open Univ -open Environ open Reduction open Nativelambda diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 860283e065..98314348ab 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -5,11 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Names -open Esubst open Term -open Declarations open Pre_env open Nativevalues diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index f8c39b4dce..a69b9d472d 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -5,13 +5,9 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Term open Util open Nativevalues -open Declarations open Nativecode -open Pre_env open Errors open Envars diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 0cbe4ccd5e..9ef8c06a31 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -5,11 +5,7 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Term -open Nativevalues open Nativecode -open Pre_env (** This file provides facilities to access OCaml compiler and dynamic linker, used by the native compiler. *) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 2d117cc96c..7c0607cc4d 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -9,7 +9,6 @@ open Term open Context open Environ -open Closure (*********************************************************************** s Reduction functions *) diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 6b76e616aa..ea2b3de24f 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term type retroknowledge diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 4168e50160..96ab5adecb 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Environ open Reduction diff --git a/kernel/vm.mli b/kernel/vm.mli index cbc68c4884..fa88418cef 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -1,7 +1,6 @@ open Names open Term open Cbytecodes -open Cemitcodes (** Efficient Virtual Machine *) diff --git a/lib/future.ml b/lib/future.ml index 5645352682..1e878ac32c 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -40,8 +40,6 @@ module UUID = struct let equal = (==) end -open UUID - type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation] (* Val is not necessarily a final state, so the diff --git a/lib/pp.mli b/lib/pp.mli index 811dd46581..635a149e88 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp_control - (** Modify pretty printing functions behavior for emacs ouput (special chars inserted at some places). This function should called once in module [Options], that's all. *) diff --git a/library/assumptions.mli b/library/assumptions.mli index cd08caf73c..2e58109356 100644 --- a/library/assumptions.mli +++ b/library/assumptions.mli @@ -9,7 +9,6 @@ open Util open Names open Term -open Environ (** A few declarations for the "Print Assumption" command @author spiwack *) diff --git a/library/declare.mli b/library/declare.mli index f33077ddb2..663d240dcd 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -9,12 +9,7 @@ open Names open Libnames open Term -open Context -open Declarations open Entries -open Indtypes -open Safe_typing -open Nametab open Decl_kinds (** This module provides the official functions to declare new variables, @@ -24,8 +19,6 @@ open Decl_kinds reset works properly --- and will fill some global tables such as [Nametab] and [Impargs]. *) -open Nametab - (** Declaration of local constructions (Variable/Hypothesis/Local) *) type section_variable_entry = diff --git a/library/decls.mli b/library/decls.mli index 001d060e84..f45e4f1217 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Context open Libnames open Decl_kinds diff --git a/library/dischargedhypsmap.mli b/library/dischargedhypsmap.mli index f2173bf49c..884ba6a781 100644 --- a/library/dischargedhypsmap.mli +++ b/library/dischargedhypsmap.mli @@ -7,9 +7,6 @@ (************************************************************************) open Libnames -open Term -open Environ -open Nametab type discharged_hyps = full_path list diff --git a/library/globnames.mli b/library/globnames.mli index 4bf21cf0a1..7afe801504 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -7,7 +7,6 @@ (************************************************************************) open Util -open Pp open Names open Term open Mod_subst diff --git a/library/goptions.mli b/library/goptions.mli index 6f23cf5ea7..6251b8d2d2 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -44,10 +44,7 @@ (synchronous = consistent with the resetting commands) *) open Pp -open Names open Libnames -open Term -open Nametab open Mod_subst type option_name = Interface.option_name diff --git a/library/impargs.mli b/library/impargs.mli index 4fb056986a..e70cff8382 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -10,7 +10,6 @@ open Names open Globnames open Term open Environ -open Nametab (** {6 Implicit Arguments } *) (** Here we store the implicit arguments. Notice that we diff --git a/library/libobject.ml b/library/libobject.ml index 3bbb1e90ef..9c46b886d3 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -6,10 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util -open Errors open Libnames -open Mod_subst (* The relax flag is used to make it possible to load files while ignoring failures to incorporate some objects. This can be useful when one @@ -32,11 +29,11 @@ type 'a object_declaration = { load_function : int -> object_name * 'a -> unit; open_function : int -> object_name * 'a -> unit; classify_function : 'a -> 'a substitutivity; - subst_function : substitution * 'a -> 'a; + subst_function : Mod_subst.substitution * 'a -> 'a; discharge_function : object_name * 'a -> 'a option; rebuild_function : 'a -> 'a } -let yell s = anomaly (Pp.str s) +let yell s = Errors.anomaly (Pp.str s) let default_object s = { object_name = s; @@ -69,7 +66,7 @@ type dynamic_object_declaration = { dyn_cache_function : object_name * obj -> unit; dyn_load_function : int -> object_name * obj -> unit; dyn_open_function : int -> object_name * obj -> unit; - dyn_subst_function : substitution * obj -> obj; + dyn_subst_function : Mod_subst.substitution * obj -> obj; dyn_classify_function : obj -> obj substitutivity; dyn_discharge_function : object_name * obj -> obj option; dyn_rebuild_function : obj -> obj } diff --git a/library/libobject.mli b/library/libobject.mli index 3986b3d3f4..3dfc1e5ef7 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Libnames open Mod_subst diff --git a/library/library.mli b/library/library.mli index 69fd5e9400..afcce7f6c0 100644 --- a/library/library.mli +++ b/library/library.mli @@ -7,10 +7,8 @@ (************************************************************************) open Loc -open Pp open Names open Libnames -open Libobject (** This module provides functions to load, open and save libraries. Libraries correspond to the subclass of modules that diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 9aa417a094..3245c642fa 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -11,7 +11,6 @@ open Errors open Util open Pcoq open Extend -open Ppextend open Constrexpr open Notation_term open Libnames diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 19e8ee8f60..ee6ed4a9ed 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -6,15 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Compat -open Pp open Names open Constrexpr open Notation_term open Pcoq open Extend -open Vernacexpr -open Ppextend open Genarg open Egramml diff --git a/parsing/egramml.ml b/parsing/egramml.ml index dc558e8416..f26ff817b2 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -10,7 +10,6 @@ open Compat open Names open Pcoq open Genarg -open Tacexpr open Vernacexpr (** Making generic actions in type generic_argument *) diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index c2dbd1d63e..58def67b68 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -13,7 +13,7 @@ open Tacexpr open Misctypes open Genarg open Genredexpr -open Tok +open Tok (* necessary for camlp4 *) open Pcoq open Pcoq.Prim diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index f30ebfb7c0..d41fcb7aea 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -9,7 +9,7 @@ open Compat open Names open Libnames -open Tok +open Tok (* necessary for camlp4 *) open Pcoq open Pcoq.Prim diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index dc545c691f..e95aecca83 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -9,7 +9,6 @@ open Compat open Constrexpr open Vernacexpr -open Locality open Misctypes open Tok diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 371dae6c81..b52dcdbd60 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -8,7 +8,6 @@ open Pp open Compat -open Tok open Errors open Util open Names @@ -16,10 +15,9 @@ open Constrexpr open Constrexpr_ops open Extend open Vernacexpr -open Locality open Decl_kinds -open Declaremods open Misctypes +open Tok (* necessary for camlp4 *) open Pcoq open Pcoq.Tactic diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index a32a40f9dc..820d44392b 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -16,13 +16,11 @@ open Glob_term open Tacexpr open Libnames open Globnames - -open Nametab open Detyping -open Tok open Misctypes open Decl_kinds open Genredexpr +open Tok (* necessary for camlp4 *) (* Generic xml parser without raw data *) diff --git a/parsing/lexer.mli b/parsing/lexer.mli index 8eef2f63c3..dd811acfe9 100644 --- a/parsing/lexer.mli +++ b/parsing/lexer.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp - val add_keyword : string -> unit val remove_keyword : string -> unit val is_keyword : string -> bool diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 6dee6cf160..6fac3da965 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -8,14 +8,13 @@ open Pp open Compat -open Tok open Errors open Util open Extend open Genarg open Stdarg open Constrarg -open Tacexpr +open Tok (* necessary for camlp4 *) (** The parser of Coq *) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 5dcfa844a4..3fb647a96c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -7,9 +7,7 @@ (************************************************************************) open Loc -open Pp open Names -open Glob_term open Extend open Vernacexpr open Genarg @@ -211,7 +209,6 @@ module Module : module Tactic : sig - open Glob_term val open_constr : open_constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry @@ -231,7 +228,6 @@ module Tactic : module Vernac_ : sig - open Decl_kinds val gallina : vernac_expr Gram.entry val gallina_ext : vernac_expr Gram.entry val command : vernac_expr Gram.entry diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index 8232604f78..b81821a2e5 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -1,4 +1,3 @@ -open Proofview.Notations let contrib_name = "btauto" diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index b086190f4e..f4f62cb852 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -16,14 +16,12 @@ open Term open Vars open Tacmach open Tactics -open Tacticals open Typing open Ccalgo open Ccproof open Pp open Errors open Util -open Proofview.Notations let constant dir s = lazy (Coqlib.gen_constant "CC" dir s) diff --git a/plugins/decl_mode/decl_expr.mli b/plugins/decl_mode/decl_expr.mli index 7548c338a0..982fb47ad2 100644 --- a/plugins/decl_mode/decl_expr.mli +++ b/plugins/decl_mode/decl_expr.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Pp open Tacexpr type 'it statement = diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index a722daca52..505d7dba5c 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -11,7 +11,6 @@ open Util open Names open Constrexpr open Tacintern -open Tacinterp open Decl_expr open Decl_mode open Pretyping diff --git a/plugins/decl_mode/decl_interp.mli b/plugins/decl_mode/decl_interp.mli index 88fb9653ae..6fbf5d25c9 100644 --- a/plugins/decl_mode/decl_interp.mli +++ b/plugins/decl_mode/decl_interp.mli @@ -8,7 +8,6 @@ open Tacintern open Decl_expr -open Mod_subst val intern_proof_instr : glob_sign -> raw_proof_instr -> glob_proof_instr diff --git a/plugins/decl_mode/decl_mode.mli b/plugins/decl_mode/decl_mode.mli index 8e691f508f..1ed1abaf75 100644 --- a/plugins/decl_mode/decl_mode.mli +++ b/plugins/decl_mode/decl_mode.mli @@ -9,7 +9,6 @@ open Names open Term open Evd -open Tacmach val set_daimon_flag : unit -> unit val clear_daimon_flag : unit -> unit diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 45ffb450f6..de57330ecf 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -13,7 +13,6 @@ open Evd open Tacmach open Tacintern -open Tacinterp open Decl_expr open Decl_mode open Decl_interp diff --git a/plugins/decl_mode/decl_proof_instr.mli b/plugins/decl_mode/decl_proof_instr.mli index d78ca84d12..458318264e 100644 --- a/plugins/decl_mode/decl_proof_instr.mli +++ b/plugins/decl_mode/decl_proof_instr.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Refiner open Names open Term open Tacmach diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index fe75d17f6a..7c9ef3c2a8 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -11,11 +11,11 @@ open Util open Compat open Pp -open Tok open Decl_expr open Names open Pcoq open Vernacexpr +open Tok (* necessary for camlp4 *) open Pcoq.Constr open Pcoq.Tactic diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 0fd3e7bb7b..3058b91b66 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -9,7 +9,6 @@ open Names open Globnames open Miniml -open Mlutil open Pp (** By default, in module Format, you can do horizontal placing of blocks diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 89db50e630..8d3cf76fdd 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -12,7 +12,6 @@ open Names open Term open Declarations open Environ -open Libnames open Miniml val extract_constant : env -> constant -> constant_body -> ml_decl diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 1a4cfb45fa..9b72c3e9fd 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -1363,7 +1363,6 @@ let is_not_strict t = restriction for the moment. *) -open Declarations open Declareops let inline_test r t = diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index f25f0bb89d..ff5dee31f8 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Globnames open Miniml open Table diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 52805bc87f..42c8b11f3f 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -7,11 +7,8 @@ (************************************************************************) open Names -open Declarations -open Environ open Globnames open Miniml -open Mod_subst (*s Functions upon ML modules. *) diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 5133801ee7..6c1709140b 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -11,7 +11,6 @@ open Sequent open Rules open Instances open Term -open Vars open Tacmach open Tacticals diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli index 753f2d76e1..66c42e1e64 100644 --- a/plugins/firstorder/instances.mli +++ b/plugins/firstorder/instances.mli @@ -6,9 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term -open Tacmach -open Names open Globnames open Rules diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 0e5223d6bd..536ee7cc34 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -9,7 +9,6 @@ open Term open Formula open Tacmach -open Names open Globnames module OrderedConstr: Set.OrderedType with type t=constr diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 2a5e81ec0d..aeb07fc3a2 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -15,7 +15,6 @@ des inéquations et équations sont entiers. En attendant la tactique Field. open Term open Tactics open Names -open Libnames open Globnames open Tacticals open Tacmach diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 56b1a3f1cb..d6f21fb86b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -6,7 +6,6 @@ open Vars open Context open Namegen open Names -open Declarations open Declareops open Pp open Entries diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index cc9ae912dc..2dd78d8908 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -18,7 +18,6 @@ open Indfun open Genarg open Tacticals open Misctypes -open Miscops let pr_binding prc = function | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c) diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 56fc9bd2cd..91a5ddf826 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,10 +1,3 @@ -open Names -open Term -open Pp -open Indfun_common -open Libnames -open Glob_term -open Declarations open Misctypes val do_generate_principle : diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f951debfde..ca0a432d6a 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -10,7 +10,6 @@ open Term open Vars open Namegen open Environ -open Declarations open Declareops open Entries open Pp @@ -24,7 +23,6 @@ open Tacticals open Tacmach open Tactics open Nametab -open Decls open Declare open Decl_kinds open Tacred diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 74f1ba713f..de20756b3c 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -27,7 +27,6 @@ open Globnames open Nametab open Contradiction open Misctypes -open Proofview.Notations module OmegaSolver = Omega.MakeOmegaSolver (Bigint) open OmegaSolver diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 0aad364c16..b384478ae2 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -16,7 +16,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Coq_omega -open Refiner let omega_tactic l = let tacs = List.map diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index affe31d790..9ee16a5827 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -109,7 +109,6 @@ open Pattern open Patternops open ConstrMatching open Tacmach -open Proofview.Notations (*i*) (*s First, we need to access some Coq constants diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index efe11b99cb..c07825f8cd 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -9,7 +9,6 @@ (*i camlp4deps: "grammar/grammar.cma" i*) open Refl_omega -open Refiner let romega_tactic l = let tacs = List.map diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index b8507041f3..0cb9d4460f 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -22,7 +22,6 @@ open Glob_term open Tacticals open Tacexpr open Coqlib -open Tacmach open Mod_subst open Tacinterp open Libobject @@ -797,8 +796,6 @@ let ltac_ring_structure e = [req;sth;ext;morph;th;cst_tac;pow_tac; lemma1;lemma2;pretac;posttac] -open Proofview.Notations - let ring_lookup (f:glob_tactic_expr) lH rl t = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 9809d4d099..b5bb27da96 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term open Context diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 58265208b7..886e00e835 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -18,7 +18,6 @@ open Environ open Libobject open Term open Termops -open Decl_kinds open Mod_subst (* usage qque peu general: utilise aussi dans record *) diff --git a/pretyping/classops.mli b/pretyping/classops.mli index d0c7793ae6..7bde9e910e 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -7,11 +7,9 @@ (************************************************************************) open Names -open Decl_kinds open Term open Evd open Environ -open Nametab open Mod_subst (** {6 This is the type of class kinds } *) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index f5c548cc43..c1b114c913 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -6,13 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Evd open Names open Term -open Context open Environ -open Evarutil open Glob_term (** {6 Coercions. } *) diff --git a/pretyping/constrMatching.mli b/pretyping/constrMatching.mli index b82f115251..19cf348775 100644 --- a/pretyping/constrMatching.mli +++ b/pretyping/constrMatching.mli @@ -12,7 +12,6 @@ open Names open Term open Environ open Pattern -open Termops (** [PatternMatchingFailure] is the exception raised when pattern matching fails *) diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 8a10b7ed5e..2cca25fd25 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Pp open Names open Term open Context diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 89993189f1..3a8e4fab5a 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -8,9 +8,7 @@ open Names open Term -open Context open Environ -open Termops open Reductionops open Evd open Locus diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 20a4a3f9e3..bdc4bc0ae1 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Util open Errors open Names diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f4636cdaa4..49ce29fdfb 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -20,7 +20,6 @@ open Environ open Evd open Reductionops open Pretype_errors -open Retyping (****************************************************) (* Expanding/testing/exposing existential variables *) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 7e1f7df88b..f41f1ec862 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,15 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Util open Names -open Glob_term open Term open Context open Evd open Environ -open Reductionops (** {5 This modules provides useful functions for unification modulo evars } *) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 2b0e9ca684..8f423c7881 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -8,14 +8,11 @@ open Util open Loc -open Pp open Names open Term open Context open Environ -open Libnames open Mod_subst -open Termops (** {5 Existential variables and unification states} diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 1785c87be8..9e0aac909f 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -6,15 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names -open Context -open Term -open Libnames -open Nametab -open Decl_kinds -open Misctypes -open Locus open Glob_term (** Equalities *) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 610a7bf39b..6bcfac20ed 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -8,8 +8,6 @@ open Names open Term -open Declarations -open Inductiveops open Environ open Evd diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index ddf615033e..a086a6f58f 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Misctypes open Locus (** Utilities on occurrences *) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index cc2054d100..af7a99320b 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -16,10 +16,7 @@ open Declarations open Names open Inductive open Util -open Unix open Nativecode -open Inductiveops -open Closure open Nativevalues open Nativelambda diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli index a589846b9a..8f65ddb2f6 100644 --- a/pretyping/nativenorm.mli +++ b/pretyping/nativenorm.mli @@ -5,10 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Environ -open Reduction open Evd open Nativelambda diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 5cc4049ba2..cfe71510a1 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -6,13 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Names open Context open Term -open Environ open Globnames -open Nametab open Glob_term open Mod_subst open Misctypes diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 404f5b4012..8ffd53055e 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -9,9 +9,6 @@ open Util open Names open Term -open Vars -open Termops -open Namegen open Environ open Type_errors diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 996b751465..8e98f63076 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -6,13 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term -open Context open Environ -open Glob_term -open Inductiveops open Type_errors (** {6 The type of errors raised by the pretyper } *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 6994723ac6..ec8aae1403 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -13,7 +13,6 @@ implicit arguments. *) open Names -open Context open Term open Environ open Evd diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 88199c4349..42663c0144 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -7,10 +7,8 @@ (************************************************************************) open Names -open Nametab open Term open Globnames -open Libobject (** Operations concerning records and canonical structures *) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index aff65d53a3..5ba0d74eca 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -12,7 +12,6 @@ open Context open Univ open Evd open Environ -open Closure (** Reduction Functions. *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 963d61ca2d..bb3ffa4116 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Evd open Environ diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 4b03c935f5..dd7542fc7f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -16,7 +16,6 @@ open Libnames open Globnames open Termops open Namegen -open Libobject open Environ open Closure open Reductionops diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index be92be51a0..34aca3e332 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -11,9 +11,6 @@ open Term open Environ open Evd open Reductionops -open Closure -open Glob_term -open Termops open Pattern open Globnames open Locus diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli index 2560ae080a..7825ebdf1a 100644 --- a/pretyping/term_dnet.mli +++ b/pretyping/term_dnet.mli @@ -7,8 +7,6 @@ (************************************************************************) open Term -open Context -open Libnames open Mod_subst (** Dnets on constr terms. diff --git a/pretyping/termops.mli b/pretyping/termops.mli index d9213fc133..d0d3fd767e 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Pp open Names open Term diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 0fe22bcce3..c362935253 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -8,14 +8,10 @@ open Names open Globnames -open Decl_kinds open Term open Context open Evd open Environ -open Nametab -open Mod_subst -open Topconstr type direction = Forward | Backward diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 94bbfce00e..b3cfb37fa0 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -8,15 +8,11 @@ open Loc open Names -open Decl_kinds open Term open Context open Evd open Environ -open Nametab -open Mod_subst open Constrexpr -open Pp open Globnames type contexts = Parameters | Properties diff --git a/pretyping/typing.ml b/pretyping/typing.ml index bbcc5727b4..0cd9099e35 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -14,7 +14,6 @@ open Vars open Environ open Reductionops open Type_errors -open Pretype_errors open Inductive open Inductiveops open Typeops diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index ca370b559d..9731e3590b 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.mli @@ -6,10 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term open Environ -open Reduction (** {6 Reduction functions } *) val cbv_vm : env -> constr -> types -> constr diff --git a/printing/genprint.ml b/printing/genprint.ml index dcd357d5c9..02f2dd63b2 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Util open Genarg type ('raw, 'glb, 'top) printer = { diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 95498b8d80..79399094d7 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -8,8 +8,6 @@ open Loc open Pp -open Environ -open Term open Libnames open Constrexpr open Names diff --git a/printing/pptactic.mli b/printing/pptactic.mli index 47640afa60..e20e3ae014 100644 --- a/printing/pptactic.mli +++ b/printing/pptactic.mli @@ -11,7 +11,6 @@ open Genarg open Names open Constrexpr open Tacexpr -open Proof_type open Ppextend open Environ open Pattern diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 1bf8c6ab3c..0cbb7a86c4 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -8,13 +8,11 @@ open Pp open Names -open Context open Term open Environ open Reductionops open Libnames open Globnames -open Nametab open Misctypes (** A Pretty-Printer for the Calculus of Inductive Constructions. *) diff --git a/printing/printer.ml b/printing/printer.ml index 9143d1c5b3..ad154ec554 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -12,7 +12,6 @@ open Util open Names open Term open Vars -open Context open Environ open Globnames open Nametab diff --git a/printing/printer.mli b/printing/printer.mli index 2d7f0a5d33..6ca55b16b5 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -8,19 +8,14 @@ open Pp open Names -open Libnames open Globnames open Term open Context open Environ -open Glob_term open Pattern -open Nametab -open Termops open Evd open Proof_type open Glob_term -open Tacexpr (** These are the entry points for printing terms, context, tac, ... *) diff --git a/printing/printmod.ml b/printing/printmod.ml index 34224d7b50..112abeec9c 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Errors open Names open Declarations open Nameops diff --git a/proofs/clenv.mli b/proofs/clenv.mli index c8b63ea0fd..7731c4ca27 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -6,14 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term -open Context open Environ open Evd -open Evarutil open Mod_subst -open Glob_term open Unification open Misctypes diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index f852995a08..29211c71ad 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -83,7 +83,6 @@ let elim_res_pf_THEN_i clenv tac gls = let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls -open Proofview.Notations let new_elim_res_pf_THEN_i clenv tac = Proofview.Goal.enter begin fun gl -> let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags:elim_flags clenv) gl in diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index d172d5c36b..86d567ef2f 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -6,10 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term -open Context -open Evd open Clenv open Proof_type open Tacexpr diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 6eee974d97..d5b80398a3 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -6,13 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Term -open Environ open Evd -open Refiner open Pretyping -open Glob_term (** Refinement of existential variables. *) diff --git a/proofs/logic.mli b/proofs/logic.mli index 69c10812ab..da54ef0a86 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -8,9 +8,7 @@ open Names open Term -open Context open Evd -open Environ open Proof_type (** This suppresses check done in [prim_refiner] for the tactic given in diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index f0ea695330..ca760c456d 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -12,7 +12,6 @@ open Names open Entries open Environ open Evd -open Refiner let refining = Proof_global.there_are_pending_proofs let check_no_pending_proofs = Proof_global.check_no_pending_proof diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index c3d0c90538..fea1b701ed 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -7,14 +7,10 @@ (************************************************************************) open Loc -open Pp open Names open Term -open Context open Environ open Decl_kinds -open Tacmach -open Tacexpr (** Several proofs can be opened simultaneously but at most one is focused at some time. The following functions work by side-effect diff --git a/proofs/proof.mli b/proofs/proof.mli index c535fa914f..ac922ac50d 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -29,8 +29,6 @@ [give_up] was run and solve the goal there. *) -open Term - (* Type of a proof. *) type proof diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index bbe8ad5316..f5431daaaf 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -17,7 +17,6 @@ open Util open Pp open Names -open Util (*** Proof Modes ***) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 4394aeff1d..3ee7c87f77 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -14,7 +14,6 @@ open Context open Tacexpr open Glob_term open Nametab -open Pattern open Misctypes (*i*) diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 4abd6f7762..85ecfdd8a2 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -6,18 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Environ open Evd open Names -open Libnames open Term open Context -open Pp open Tacexpr open Glob_term -open Genarg open Nametab -open Pattern open Misctypes (** This module defines the structure of proof tree and the tactic type. So, it diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index 31affc2807..7554976155 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -8,11 +8,9 @@ open Names open Term -open Closure open Pattern open Genredexpr open Reductionops -open Termops open Locus type red_expr = diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 8fc9e9e179..db2c081d1b 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -6,12 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Context open Evd open Proof_type -open Tacexpr -open Logic (** The refiner (handles primitive rules and high-level tactics). *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index de73f7720d..9a03df0417 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Util open Names open Namegen @@ -205,7 +204,6 @@ let pr_glls glls = (* Variants of [Tacmach] functions built with the new proof engine *) module New = struct - open Proofview.Notations let pf_apply f gl = f (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 48c4f8d48b..10f6be1d5d 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -11,12 +11,8 @@ open Term open Context open Environ open Evd -open Reduction open Proof_type -open Refiner open Redexpr -open Tacexpr -open Glob_term open Pattern open Locus open Misctypes @@ -134,8 +130,6 @@ val pr_glls : goal list sigma -> Pp.std_ppcmds (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig - open Proofview - val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a val pf_global : identifier -> Proofview.Goal.t -> constr val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 1ae1a3905c..bf85073606 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.mli @@ -8,8 +8,6 @@ open Environ open Pattern -open Evd -open Proof_type open Names open Tacexpr open Term diff --git a/tactics/auto.ml b/tactics/auto.ml index 9bb55977ec..795582f278 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -30,13 +30,11 @@ open Tacticals open Clenv open Libnames open Globnames -open Nametab open Smartlocate open Libobject open Printer open Tacexpr open Mod_subst -open Misctypes open Locus open Proofview.Notations diff --git a/tactics/auto.mli b/tactics/auto.mli index 7ce351f434..2d27208805 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -32,8 +32,6 @@ type 'a auto_tactic = | Unfold_nth of evaluable_global_reference (** Hint Unfold *) | Extern of Tacexpr.glob_tactic_expr (** Hint Extern *) -open Glob_term - type hints_path_atom = | PathHints of global_reference list | PathAny diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index c5017ac75b..ba36761459 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -9,7 +9,6 @@ open Equality open Names open Pp -open Proof_type open Tacticals open Tactics open Term @@ -19,7 +18,6 @@ open Util open Tacexpr open Mod_subst open Locus -open Proofview.Notations (* Rewriting rules *) type rew_rule = { rew_lemma: constr; diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 69ab9c55f2..198fa36f59 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -8,7 +8,6 @@ open Term open Tacexpr -open Tacmach open Equality (** Rewriting rules before tactic interpretation *) diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c6fb0d12aa..13c188c79e 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -15,7 +15,6 @@ open Tactics open Coqlib open Reductionops open Misctypes -open Proofview.Notations (* Absurd *) diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index e3dabfe983..8ec6de88a0 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Term -open Proof_type open Misctypes val absurd : constr -> unit Proofview.tactic diff --git a/tactics/eauto.mli b/tactics/eauto.mli index ba35433f19..e2da23aaaf 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -8,12 +8,8 @@ open Term open Proof_type -open Tacexpr open Auto -open Topconstr open Evd -open Environ -open Explore val hintbases : hint_db_name list option Pcoq.Gram.entry diff --git a/tactics/elim.ml b/tactics/elim.ml index 06f84ecd1e..5d5b592ad4 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Util open Names open Term diff --git a/tactics/elim.mli b/tactics/elim.mli index 35b7b26025..b83a97bccb 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -8,9 +8,6 @@ open Names open Term -open Proof_type -open Tacmach -open Genarg open Tacticals open Misctypes diff --git a/tactics/equality.mli b/tactics/equality.mli index 24c9095813..e8b142d89c 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -7,22 +7,13 @@ (************************************************************************) (*i*) -open Pp open Names open Term open Context open Evd open Environ -open Proof_type open Tacmach -open Hipattern -open Pattern -open Tacticals -open Tactics open Tacexpr -open Termops -open Glob_term -open Genarg open Ind_tables open Locus open Misctypes diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 20f72b3d56..83a98745af 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -7,7 +7,6 @@ (************************************************************************) open Util -open Names open Errors open Evar_refiner open Tacmach @@ -50,7 +49,6 @@ let instantiate n (ist,rawc) ido gl = tclNORMEVAR gl -open Proofview.Notations let let_evar name typ = let src = (Loc.ghost,Evar_kinds.GoalEvar) in Proofview.Goal.enter begin fun gl -> diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index dfc14bddf3..16c236b822 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -7,11 +7,8 @@ (************************************************************************) open Tacexpr -open Term open Names -open Proof_type open Constrexpr -open Termops open Glob_term open Misctypes diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 2b28a65471..69ef3b4ddb 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Proof_type - val discrHyp : Names.Id.t -> unit Proofview.tactic val injHyp : Names.Id.t -> unit Proofview.tactic diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4 index c7867a83c8..6012088f7b 100644 --- a/tactics/g_class.ml4 +++ b/tactics/g_class.ml4 @@ -17,8 +17,6 @@ END (** Options: depth, debug and transparency settings. *) -open Goptions - let set_transparency cl b = List.iter (fun r -> let gr = Smartlocate.global_with_alias r in diff --git a/tactics/g_rewrite.ml4 b/tactics/g_rewrite.ml4 index 03bbc4b046..954892e81d 100644 --- a/tactics/g_rewrite.ml4 +++ b/tactics/g_rewrite.ml4 @@ -11,19 +11,14 @@ (* Syntax for rewriting with strategies *) open Names -open Term -open Vars open Misctypes open Locus -open Locusops open Constrexpr open Glob_term -open Patternops open Geninterp open Extraargs open Tacmach open Tacticals -open Tactics open Rewrite type constr_expr_with_bindings = constr_expr with_bindings diff --git a/tactics/geninterp.ml b/tactics/geninterp.ml index e9d3f42925..4a49ae287f 100644 --- a/tactics/geninterp.ml +++ b/tactics/geninterp.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Util open Names open Genarg diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index b38eb654be..4735b26b32 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -8,9 +8,7 @@ open Names open Term -open Context open Evd -open Pattern open Coqlib (** High-order patterns *) diff --git a/tactics/inv.mli b/tactics/inv.mli index 9491b7d7b9..f5820c33cb 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -7,13 +7,10 @@ (************************************************************************) open Loc -open Pp open Names open Term -open Tacmach open Misctypes open Tacexpr -open Glob_term type inversion_status = Dep of constr option | NoDep diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 7af7fcb025..ac56e6688b 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -28,7 +28,6 @@ open Declare open Tacticals open Tactics open Decl_kinds -open Proofview.Notations let no_inductive_inconstr env constr = (str "Cannot recognize an inductive predicate in " ++ diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 16695fcd7d..36aa5e67f2 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -7,11 +7,8 @@ (************************************************************************) open Loc -open Pp open Names open Term -open Glob_term -open Proof_type open Constrexpr open Misctypes diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index 853215a5ab..79a1a41c8d 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -8,34 +8,28 @@ (*i camlp4deps: "grammar/grammar.cma" i*) -open Pp open Errors open Util -open Names open Nameops open Namegen open Term open Vars -open Termops open Reduction open Tacticals open Tacmach open Tactics open Patternops open Clenv -open Glob_term open Typeclasses open Typeclasses_errors open Classes open Constrexpr -open Libnames open Globnames open Evd open Misctypes open Locus open Locusops open Decl_kinds -open Tacinterp open Elimschemes open Goal open Environ @@ -43,8 +37,6 @@ open Pp open Names open Tacinterp open Termops -open Genarg -open Extraargs open Entries open Libnames @@ -1345,8 +1337,6 @@ let occurrences_of = function error "Illegal negative occurrence number."; (true,nl) -open Extraargs - let apply_glob_constr c l2r occs = fun () env avoid t ty cstr evars -> let evd, c = (Pretyping.understand_tcc (goalevars evars) env c) in apply_lemma l2r (general_rewrite_unif_flags ()) (c, NoBindings) diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml index aa254c2f86..2c1de14ea9 100644 --- a/tactics/taccoerce.ml +++ b/tactics/taccoerce.ml @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Util -open Errors open Names open Term open Pattern diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index c787ebbda8..9b50cc1c02 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Libobject open Pattern open Pp open Genredexpr @@ -21,12 +20,10 @@ open Globnames open Nametab open Smartlocate open Constrexpr -open Constrexpr_ops open Termops open Tacexpr open Genarg open Constrarg -open Mod_subst open Misctypes open Locus diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli index 8473f585bd..22588fcf16 100644 --- a/tactics/tacintern.mli +++ b/tactics/tacintern.mli @@ -8,15 +8,9 @@ open Pp open Names -open Proof_type -open Tacmach -open Tactic_debug -open Term open Tacexpr open Genarg open Constrexpr -open Mod_subst -open Redexpr open Misctypes open Nametab diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0e802f8a9c..60564dbdb7 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -7,7 +7,6 @@ (************************************************************************) open Constrintern -open Pattern open Patternops open Pp open Genredexpr @@ -37,7 +36,6 @@ open Printer open Pretyping open Evd open Misctypes -open Miscops open Locus open Tacintern open Taccoerce diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 0c89eb3a28..49d40db240 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -6,16 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names -open Proof_type -open Tacmach open Tactic_debug open Term open Tacexpr open Genarg -open Constrexpr -open Mod_subst open Redexpr open Misctypes diff --git a/tactics/tactic_option.mli b/tactics/tactic_option.mli index be36b3f82d..db437ce0c9 100644 --- a/tactics/tactic_option.mli +++ b/tactics/tactic_option.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Proof_type open Tacexpr open Vernacexpr diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 310023e544..3e6e64ecb5 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -14,12 +14,7 @@ open Context open Tacmach open Proof_type open Clenv -open Reduction -open Pattern -open Genarg open Tacexpr -open Termops -open Glob_term open Locus open Misctypes diff --git a/tactics/tactics.ml b/tactics/tactics.ml index a5f88c9291..fda84e6f59 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -26,7 +26,6 @@ open Pfedit open Tacred open Genredexpr open Tacmach -open Proof_type open Logic open Clenv open Clenvtac @@ -43,7 +42,6 @@ open Unification open Locus open Locusops open Misctypes -open Miscops open Proofview.Notations exception Bound diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b181dc5348..9f4f0e9ce1 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -7,26 +7,17 @@ (************************************************************************) open Loc -open Pp open Names open Term open Context open Environ -open Tacmach open Proof_type -open Reduction open Evd -open Evar_refiner open Clenv open Redexpr -open Tacticals open Globnames -open Genarg open Tacexpr -open Nametab -open Glob_term open Pattern -open Termops open Unification open Misctypes open Locus diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 05a08c8253..2a35e32d97 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -15,7 +15,6 @@ open Globnames open Pp open Genarg open Stdarg -open Tacticals open Tacinterp open Tactics open Errors diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli index adc49ed408..1e2c430f89 100644 --- a/tools/coqdoc/cpretty.mli +++ b/tools/coqdoc/cpretty.mli @@ -6,7 +6,5 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Index - val coq_file : string -> Cdglobals.coq_module -> unit val detect_subtitle : string -> Cdglobals.coq_module -> string option diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index b79d774431..94447f0d04 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -21,7 +21,6 @@ open Names open Globnames open Inductiveops open Tactics -open Tacticals open Ind_tables open Misctypes open Proofview.Notations diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli index 660f6f7e72..6509a7d3b8 100644 --- a/toplevel/auto_ind_decl.mli +++ b/toplevel/auto_ind_decl.mli @@ -8,10 +8,6 @@ open Term open Names -open Libnames -open Mod_subst -open Context -open Proof_type open Ind_tables (** This file is about the automatic generation of schemes about diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli index ebaaee12d0..bfc9bcff27 100644 --- a/toplevel/autoinstance.mli +++ b/toplevel/autoinstance.mli @@ -8,8 +8,6 @@ open Term open Globnames -open Typeclasses -open Names open Evd open Context diff --git a/toplevel/class.mli b/toplevel/class.mli index 0d39ee1709..8bb3eb7ce8 100644 --- a/toplevel/class.mli +++ b/toplevel/class.mli @@ -7,12 +7,8 @@ (************************************************************************) open Names -open Term open Classops -open Declare open Globnames -open Decl_kinds -open Nametab (** Classes and coercions. *) diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 220e0e0506..4d8a6d5d78 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -10,8 +10,6 @@ open Names open Term open Vars -open Context -open Evd open Environ open Nametab open Errors @@ -26,7 +24,6 @@ open Constrexpr open Decl_kinds open Entries -open Misctypes let typeclasses_db = "typeclass_instances" diff --git a/toplevel/classes.mli b/toplevel/classes.mli index a8e611928e..de62ff369e 100644 --- a/toplevel/classes.mli +++ b/toplevel/classes.mli @@ -7,18 +7,12 @@ (************************************************************************) open Names -open Decl_kinds -open Term open Context open Evd open Environ -open Nametab -open Mod_subst open Constrexpr open Typeclasses -open Implicit_quantifiers open Libnames -open Globnames (** Errors *) diff --git a/toplevel/command.mli b/toplevel/command.mli index fe6a0a4003..d2ebdc5611 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term open Entries @@ -17,7 +16,6 @@ open Vernacexpr open Constrexpr open Decl_kinds open Redexpr -open Constrintern open Pfedit (** This file is about the interpretation of raw commands into typed diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 1375f33619..4aedaa0352 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Pcoq (** The Coq toplevel loop. *) diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli index 6f696f27a0..6cef31c8a8 100644 --- a/toplevel/discharge.mli +++ b/toplevel/discharge.mli @@ -7,7 +7,6 @@ (************************************************************************) open Context -open Cooking open Declarations open Entries open Opaqueproof diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 5d024d31c5..303b3f8d65 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -14,7 +14,6 @@ open Namegen open Term open Termops open Indtypes -open Context open Environ open Pretype_errors open Type_errors @@ -24,9 +23,6 @@ open Cases open Logic open Printer open Evd -open Libnames -open Globnames -open Declarations (* This simplifies the typing context of Cases clauses *) (* hope it does not disturb other typing contexts *) diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli index 9ec3444059..bdc3eb7070 100644 --- a/toplevel/himsg.mli +++ b/toplevel/himsg.mli @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Names open Indtypes open Environ open Type_errors diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli index c5e82e2e2f..d57f1556d7 100644 --- a/toplevel/ind_tables.mli +++ b/toplevel/ind_tables.mli @@ -8,10 +8,6 @@ open Term open Names -open Libnames -open Mod_subst -open Context -open Declarations (** This module provides support for registering inductive scheme builders, declaring schemes and generating schemes on demand *) diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli index be49f41e54..7abae933dd 100644 --- a/toplevel/indschemes.mli +++ b/toplevel/indschemes.mli @@ -7,15 +7,10 @@ (************************************************************************) open Loc -open Pp open Names open Term open Environ -open Libnames -open Glob_term -open Genarg open Vernacexpr -open Ind_tables open Misctypes (** See also Auto_ind_decl, Indrec, Eqscheme, Ind_tables, ... *) diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index f6cf147ab0..fd606a6b88 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -27,12 +27,10 @@ open Declare open Pretyping open Termops open Namegen -open Evarutil open Reductionops open Constrexpr open Constrintern open Impargs -open Tacticals (* Support for mutually proved theorems *) diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli index aea5c95cf5..bbe383a857 100644 --- a/toplevel/lemmas.mli +++ b/toplevel/lemmas.mli @@ -12,7 +12,6 @@ open Decl_kinds open Constrexpr open Tacexpr open Vernacexpr -open Proof_type open Pfedit (** A hook start_proof calls on the type of the definition being started *) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 93752b3bcf..20326c9c8d 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Libnames open Tacexpr open Vernacexpr open Notation diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 6536796f4e..d772af3c18 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -20,7 +20,6 @@ open Evd open Pp open Errors open Util -open Proof_type let declare_fix_ref = ref (fun _ _ _ _ _ -> assert false) let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) @@ -143,9 +142,6 @@ let etype_of_evar evs hyps concl = subst_vars acc 0 t', s, trans in aux [] 0 (List.rev hyps) - -open Tacticals - let trunc_named_context n ctx = let len = List.length ctx in List.firstn (len - n) ctx diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 04292422cc..746b4ed14d 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -7,15 +7,11 @@ (************************************************************************) open Environ -open Tacmach open Term open Evd open Names open Pp -open Util -open Tacinterp open Globnames -open Proof_type open Vernacexpr open Decl_kinds open Tacexpr diff --git a/toplevel/search.ml b/toplevel/search.ml index 78fa3a325d..72528675c9 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Errors open Util open Names open Term diff --git a/toplevel/search.mli b/toplevel/search.mli index c139c71cd8..c06a64be17 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -12,7 +12,6 @@ open Term open Environ open Pattern open Globnames -open Nametab (** {6 Search facilities. } *) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b35929fef2..667a600582 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -14,7 +14,6 @@ open Util open Flags open System open Vernacexpr -open Vernacinterp (* The functions in this module may raise (unexplainable!) exceptions. Use the module Coqtoplevel, which catches these exceptions diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cd38510f32..3951190832 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -30,7 +30,6 @@ open Decl_kinds open Constrexpr open Redexpr open Lemmas -open Declaremods open Misctypes open Locality diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli index 3f6d45a049..9b49e57720 100644 --- a/toplevel/vernacentries.mli +++ b/toplevel/vernacentries.mli @@ -6,11 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Term -open Vernacinterp -open Vernacexpr -open Constrexpr open Misctypes val dump_global : Libnames.reference or_by_notation -> unit diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 8f8f5bdd7f..3cbbbf05ee 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Tacexpr - (** Interpretation of extended vernac phrases. *) val vinterp_add : string -> (Genarg.raw_generic_argument list -> unit -> unit) -> unit diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli index fed8332bd8..ab8069ec61 100644 --- a/toplevel/whelp.mli +++ b/toplevel/whelp.mli @@ -11,8 +11,6 @@ open Names open Term -open Topconstr -open Environ type whelp_request = | Locate of string |