diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-03-05 14:59:16 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 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 bee6b1bb8..13bc0c07e 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 847af5231..a4162d67f 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 0029eb652..d757f237d 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 c2016ba1b..ec0014175 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 89ffcb50b..2d20dd0f3 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 396eb8e7c..78626eb00 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 b3060c153..7fcd749f5 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 9f9afe922..59d95c36d 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 6cf814dce..e800ee3ef 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 f22649eb5..95753769d 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 3c56c15ef..92535606f 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 093a561d6..98843a40f 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 bfc38feb8..a731ade68 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 527cc6b2f..5d9097f38 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 f96b67f5e..b5ab3a87b 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 ad8929657..433779302 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 05b638a94..f3bb2a2ed 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 d9a9d0e3a..585dce21f 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 1ab107c77..33968b8dd 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 de378c074..a1a429789 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 846fb5b93..37e627a6d 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 c49b61ce7..5faef378a 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 687f5cb9e..25194acc9 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 a3410544e..6a893bde6 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 a98182fb8..e1acb4502 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 5b5775d1a..a1faf95e2 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 90c3779fc..a0bcdc4f4 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 9e0cfadae..9b0f8deb9 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 bc41c834a..a8f82d998 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 4d4fe9117..2d55a6b63 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 df29d0592..50c2cfee0 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 8f8e2df93..81d0a0f64 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 b6128918c..a3998cf83 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 a4ca3ffaa..95e176064 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 4f84af5fe..fd442cdb4 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 cae644ab5..d1bcb0cf1 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 6674a8323..c104d0d15 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 8ae55d096..81590bd1c 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 5f772c591..86aa69681 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 6f2ff6ec4..0f4e8a588 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 f3c4a61e6..065cbe3ec 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 f042de00f..c85d51667 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 87af636b4..16b1dc5eb 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 d12204fec..6a3c1165f 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 161de91cf..19baedf27 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 826c7f643..cf05fe013 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 f8724180e..31e86e854 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 8493b81d8..030e88829 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 ce789b00e..016a1a5b5 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 2bd421bb3..188bff626 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 f50dcfd63..a71e28d6e 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 047d8a88d..3de12b1bc 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 3435e1d75..82786df64 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 248130076..69b9d22ec 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 860283e06..98314348a 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 f8c39b4dc..a69b9d472 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 0cbe4ccd5..9ef8c06a3 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 2d117cc96..7c0607cc4 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 6b76e616a..ea2b3de24 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 4168e5016..96ab5adec 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 cbc68c488..fa88418ce 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 564535268..1e878ac32 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 811dd4658..635a149e8 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 cd08caf73..2e5810935 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 f33077ddb..663d240dc 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 001d060e8..f45e4f121 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 f2173bf49..884ba6a78 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 4bf21cf0a..7afe80150 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 6f23cf5ea..6251b8d2d 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 4fb056986..e70cff838 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 3bbb1e90e..9c46b886d 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 3986b3d3f..3dfc1e5ef 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 69fd5e940..afcce7f6c 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 9aa417a09..3245c642f 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 19e8ee8f6..ee6ed4a9e 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 dc558e841..f26ff817b 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 c2dbd1d63..58def67b6 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 f30ebfb7c..d41fcb7ae 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 dc545c691..e95aecca8 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 371dae6c8..b52dcdbd6 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 a32a40f9d..820d44392 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 8eef2f63c..dd811acfe 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 6dee6cf16..6fac3da96 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 5dcfa844a..3fb647a96 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 8232604f7..b81821a2e 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 b086190f4..f4f62cb85 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 7548c338a..982fb47ad 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 a722daca5..505d7dba5 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 88fb9653a..6fbf5d25c 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 8e691f508..1ed1abaf7 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 45ffb450f..de57330ec 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 d78ca84d1..458318264 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 fe75d17f6..7c9ef3c2a 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 0fd3e7bb7..3058b91b6 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 89db50e63..8d3cf76fd 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 1a4cfb45f..9b72c3e9f 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 f25f0bb89..ff5dee31f 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 52805bc87..42c8b11f3 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 5133801ee..6c1709140 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 753f2d76e..66c42e1e6 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 0e5223d6b..536ee7cc3 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 2a5e81ec0..aeb07fc3a 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 56b1a3f1c..d6f21fb86 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 cc9ae912d..2dd78d890 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 56fc9bd2c..91a5ddf82 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 f951debfd..ca0a432d6 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 74f1ba713..de20756b3 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 0aad364c1..b384478ae 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 affe31d79..9ee16a582 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 efe11b99c..c07825f8c 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 b8507041f..0cb9d4460 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 9809d4d09..b5bb27da9 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 58265208b..886e00e83 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 d0c7793ae..7bde9e910 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 f5c548cc4..c1b114c91 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 b82f11525..19cf34877 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 8a10b7ed5..2cca25fd2 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 89993189f..3a8e4fab5 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 20a4a3f9e..bdc4bc0ae 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 f4636cdaa..49ce29fdf 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 7e1f7df88..f41f1ec86 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 2b0e9ca68..8f423c788 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 1785c87be..9e0aac909 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 610a7bf39..6bcfac20e 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 ddf615033..a086a6f58 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 cc2054d10..af7a99320 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 a589846b9..8f65ddb2f 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 5cc4049ba..cfe71510a 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 404f5b401..8ffd53055 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 996b75146..8e98f6307 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 6994723ac..ec8aae140 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 88199c434..42663c014 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 aff65d53a..5ba0d74ec 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 963d61ca2..bb3ffa411 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 4b03c935f..dd7542fc7 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 be92be51a..34aca3e33 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 2560ae080..7825ebdf1 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 d9213fc13..d0d3fd767 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 0fe22bcce..c36293525 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 94bbfce00..b3cfb37fa 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 bbcc5727b..0cd9099e3 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 ca370b559..9731e3590 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 dcd357d5c..02f2dd63b 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 95498b8d8..79399094d 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 47640afa6..e20e3ae01 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 1bf8c6ab3..0cbb7a86c 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 9143d1c5b..ad154ec55 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 2d7f0a5d3..6ca55b16b 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 34224d7b5..112abeec9 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 c8b63ea0f..7731c4ca2 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 f852995a0..29211c71a 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 d172d5c36..86d567ef2 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 6eee974d9..d5b80398a 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 69c10812a..da54ef0a8 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 f0ea69533..ca760c456 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 c3d0c9053..fea1b701e 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 c535fa914..ac922ac50 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 bbe8ad531..f5431daaa 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 4394aeff1..3ee7c87f7 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 4abd6f776..85ecfdd8a 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 31affc280..755497615 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 8fc9e9e17..db2c081d1 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 de73f7720..9a03df041 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 48c4f8d48..10f6be1d5 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 1ae1a3905..bf8507360 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 9bb55977e..795582f27 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 7ce351f43..2d2720880 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 c5017ac75..ba3676145 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 69ab9c55f..198fa36f5 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 c6fb0d12a..13c188c79 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 e3dabfe98..8ec6de88a 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 ba35433f1..e2da23aaa 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 06f84ecd1..5d5b592ad 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 35b7b2602..b83a97bcc 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 24c909581..e8b142d89 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 20f72b3d5..83a98745a 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 dfc14bddf..16c236b82 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 2b28a6547..69ef3b4dd 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 c7867a83c..6012088f7 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 03bbc4b04..954892e81 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 e9d3f4292..4a49ae287 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 b38eb654b..4735b26b3 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 9491b7d7b..f5820c33c 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 7af7fcb02..ac56e6688 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 16695fcd7..36aa5e67f 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 853215a5a..79a1a41c8 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 aa254c2f8..2c1de14ea 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 c787ebbda..9b50cc1c0 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 8473f585b..22588fcf1 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 0e802f8a9..60564dbdb 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 0c89eb3a2..49d40db24 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 be36b3f82..db437ce0c 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 310023e54..3e6e64ecb 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 a5f88c929..fda84e6f5 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 b181dc534..9f4f0e9ce 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 05a08c825..2a35e32d9 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 adc49ed40..1e2c430f8 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 b79d77443..94447f0d0 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 660f6f7e7..6509a7d3b 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 ebaaee12d..bfc9bcff2 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 0d39ee170..8bb3eb7ce 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 220e0e050..4d8a6d5d7 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 a8e611928..de62ff369 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 fe6a0a400..d2ebdc561 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 1375f3361..4aedaa035 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 6f696f27a..6cef31c8a 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 5d024d31c..303b3f8d6 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 9ec344405..bdc3eb707 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 c5e82e2e2..d57f1556d 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 be49f41e5..7abae933d 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 f6cf147ab..fd606a6b8 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 aea5c95cf..bbe383a85 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 93752b3bc..20326c9c8 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 6536796f4..d772af3c1 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 04292422c..746b4ed14 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 78fa3a325..72528675c 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 c139c71cd..c06a64be1 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 b35929fef..667a60058 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 cd38510f3..395119083 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 3f6d45a04..9b49e5772 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 8f8f5bdd7..3cbbbf05e 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 fed8332bd..ab8069ec6 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 |