diff options
165 files changed, 0 insertions, 550 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 65ff2a53e..950edc5a3 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -9,12 +9,8 @@ open Pp open Util open Names -open Nameops open Libnames -open Misctypes -open Term open Glob_term -open Mod_subst open Constrexpr open Decl_kinds diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a59345938..272845d07 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -10,21 +10,15 @@ open Pp open Errors open Util -open Univ open Names open Nameops open Term open Termops -open Namegen -open Inductive -open Sign -open Environ open Libnames open Globnames open Impargs open Constrexpr open Constrexpr_ops -open Notation_term open Notation_ops open Topconstr open Glob_term diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d83780fb4..86998c210 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -18,7 +18,6 @@ open Globnames open Impargs open Glob_term open Glob_ops -open Pattern open Patternops open Pretyping open Cases @@ -1766,7 +1765,6 @@ let interp_binder_evars evdref env na t = understand_tcc_evars evdref env IsType t' open Environ -open Term let my_intern_constr sigma env lvar acc c = internalize sigma env acc false lvar c diff --git a/interp/coqlib.ml b/interp/coqlib.ml index d7c415306..94cb91749 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -13,7 +13,6 @@ open Names open Term open Libnames open Globnames -open Pattern open Nametab open Smartlocate diff --git a/interp/genarg.ml b/interp/genarg.ml index cfa968363..9e3528cf4 100644 --- a/interp/genarg.ml +++ b/interp/genarg.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Glob_term open Constrexpr open Misctypes diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 47d4c4af5..3057cef34 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -9,12 +9,6 @@ (*i*) open Names open Decl_kinds -open Term -open Sign -open Evd -open Environ -open Nametab -open Mod_subst open Errors open Util open Glob_term diff --git a/interp/modintern.ml b/interp/modintern.ml index 7974c3709..1e7d84c96 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Errors -open Util open Names open Entries open Libnames diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ae851d8ba..bd3ba4274 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -15,9 +15,7 @@ open Globnames open Misctypes open Glob_term open Glob_ops -open Term open Mod_subst -open Constrexpr open Notation_term open Decl_kinds diff --git a/interp/ppextend.ml b/interp/ppextend.ml index 50379b67e..562764612 100644 --- a/interp/ppextend.ml +++ b/interp/ppextend.ml @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Names (*s Pretty-print. *) diff --git a/interp/reserve.ml b/interp/reserve.ml index b271dab69..259ffa171 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -13,7 +13,6 @@ open Util open Pp open Names open Nameops -open Summary open Libobject open Lib open Notation_term diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 1a59f8ed6..adf611b56 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -14,8 +14,6 @@ (* *) open Pp open Errors -open Util -open Names open Libnames open Globnames open Misctypes diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 202a3d770..830778307 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -7,7 +7,6 @@ (************************************************************************) open Errors -open Util open Pp open Names open Libnames diff --git a/interp/topconstr.ml b/interp/topconstr.ml index f63b46946..e717e1747 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -13,15 +13,9 @@ open Util open Names open Nameops open Libnames -open Glob_term -open Glob_ops -open Term -open Mod_subst open Misctypes -open Decl_kinds open Constrexpr open Constrexpr_ops -open Notation_term (*i*) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 7a40a4029..098da5184 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -10,8 +10,6 @@ machine, Oct 2004 *) (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) -open Errors -open Util open Names open Cbytecodes open Cemitcodes diff --git a/kernel/closure.ml b/kernel/closure.ml index 11b9b4de9..94980b596 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -24,7 +24,6 @@ open Util open Pp open Term open Names -open Declarations open Environ open Esubst diff --git a/kernel/cooking.ml b/kernel/cooking.ml index d016d7f63..a015cdf92 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -13,15 +13,12 @@ (* This module implements kernel-level discharching of local declarations over global constants and inductive types *) -open Pp open Errors -open Util open Names open Term open Sign open Declarations open Environ -open Reduction (*s Cooking the constants. *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 9dec5887c..5f677d056 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -21,7 +21,6 @@ global constants/axioms, mutual inductive definitions and the module system *) -open Errors open Util open Names open Univ diff --git a/kernel/entries.ml b/kernel/entries.ml index f17918a6c..2da2c7899 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -8,7 +8,6 @@ (*i*) open Names -open Univ open Term open Sign (*i*) diff --git a/kernel/esubst.ml b/kernel/esubst.ml index c1311ac90..0bd7c515c 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -10,7 +10,6 @@ (* Support for explicit substitutions *) -open Errors open Util (*********************) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 690d5e686..6c7f4408f 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -13,7 +13,6 @@ open Univ open Term open Declarations open Inductive -open Sign open Environ open Reduction open Typeops diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 748ccf838..58689a926 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -11,7 +11,6 @@ open Util open Names open Univ open Term -open Sign open Declarations open Environ open Reduction diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index a9d4d8832..e7a5227e0 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -14,7 +14,6 @@ substitution in module constructions *) open Pp -open Errors open Util open Names open Term diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 03ee61332..d9f3c3bf0 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -13,13 +13,11 @@ declarations *) open Errors -open Util open Names open Univ open Declarations open Entries open Environ -open Term_typing open Modops open Subtyping open Mod_subst diff --git a/kernel/modops.ml b/kernel/modops.ml index cd3bc1513..5eddb6c84 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -16,10 +16,7 @@ (* This file provides with various operations on modules and module types *) open Errors -open Util -open Pp open Names -open Univ open Term open Declarations open Environ diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 485b1ecaf..3d2f19aac 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -13,8 +13,6 @@ (* This file defines the type of kernel environments *) -open Errors -open Util open Names open Sign open Univ diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 02ffab643..4ce3e7f22 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -20,7 +20,6 @@ open Util open Names open Term open Univ -open Declarations open Environ open Closure open Esubst diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 58bae94d6..4dc01f890 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -14,7 +14,6 @@ for evaluation in the bytecode virtual machine *) open Term -open Names (* Type declarations, these types shouldn't be exported they are accessed through specific functions. As being mutable and all it is wiser *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c154cba40..11d647d9a 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -58,19 +58,12 @@ *) open Errors -open Util open Names open Univ -open Term -open Reduction -open Sign open Declarations -open Inductive open Environ open Entries open Typeops -open Type_errors -open Indtypes open Term_typing open Modops open Subtyping diff --git a/kernel/sign.ml b/kernel/sign.ml index 18ef1bd3f..a654bc04d 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -16,7 +16,6 @@ names-based contexts *) open Names -open Errors open Util open Term diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 961dd652f..5fec0c2c7 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -12,18 +12,15 @@ (* This module checks subtyping of module types *) (*i*) -open Errors open Util open Names open Univ open Term open Declarations -open Environ open Reduction open Inductive open Modops open Mod_subst -open Entries (*i*) (* This local type is used to subtype a constant with a constructor or diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index dbd22e559..aed7615b8 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -17,13 +17,9 @@ open Util open Names open Univ open Term -open Reduction -open Sign open Declarations -open Inductive open Environ open Entries -open Type_errors open Indtypes open Typeops diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 890f0976e..6d4b42026 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -8,7 +8,6 @@ open Names open Term -open Sign open Environ open Reduction diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 608bcc886..3ec08fef4 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -12,7 +12,6 @@ open Names open Univ open Term open Declarations -open Sign open Environ open Entries open Reduction diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 4d0edc689..7044b1372 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -1,5 +1,4 @@ open Names -open Declarations open Term open Environ open Conv_oracle diff --git a/kernel/vm.ml b/kernel/vm.ml index 5e21db214..656e555fc 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -8,7 +8,6 @@ open Names open Term -open Conv_oracle open Cbytecodes external set_drawinstr : unit -> unit = "coq_set_drawinstr" diff --git a/lib/dyn.ml b/lib/dyn.ml index 13d1ec060..de5158b14 100644 --- a/lib/dyn.ml +++ b/lib/dyn.ml @@ -7,7 +7,6 @@ (************************************************************************) open Errors -open Util (* Dynamics, programmed with DANGER !!! *) diff --git a/lib/rtree.ml b/lib/rtree.ml index b7fe9184e..18ba9d0ef 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Util diff --git a/lib/xml_utils.ml b/lib/xml_utils.ml index 0a3b5da47..60efab577 100644 --- a/lib/xml_utils.ml +++ b/lib/xml_utils.ml @@ -17,7 +17,6 @@ * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA *) -open Printf open Serialize exception Not_element of xml diff --git a/library/assumptions.ml b/library/assumptions.ml index 6bab64a7b..2d4b6169d 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -15,10 +15,7 @@ Module-traversing code: Pierre Letouzey *) open Errors -open Util open Names -open Sign -open Univ open Term open Declarations open Mod_subst diff --git a/library/declare.ml b/library/declare.ml index 83f9e12d0..58ad1f00f 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -16,7 +16,6 @@ open Libnames open Globnames open Nameops open Term -open Sign open Declarations open Entries open Libobject diff --git a/library/decls.ml b/library/decls.ml index dd8a702e8..f6fa626b1 100644 --- a/library/decls.ml +++ b/library/decls.ml @@ -10,7 +10,6 @@ associated declarations *) open Names -open Term open Sign open Decl_kinds open Libnames diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml index b8a7da367..c26f652df 100644 --- a/library/dischargedhypsmap.ml +++ b/library/dischargedhypsmap.ml @@ -6,18 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Util open Libnames -open Names -open Term -open Reduction -open Declarations -open Environ -open Inductive -open Libobject -open Lib -open Nametab type discharged_hyps = full_path list diff --git a/library/global.ml b/library/global.ml index e7f37801b..c2bd55128 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,11 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Util open Names open Term -open Sign open Environ open Safe_typing open Summary diff --git a/library/globnames.ml b/library/globnames.ml index c5e668ce3..8d298bc94 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -6,11 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Errors -open Util open Names -open Nameops open Term open Mod_subst open Libnames diff --git a/library/goptions.ml b/library/goptions.ml index 8330ca3d2..861109d3d 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -10,12 +10,8 @@ open Pp open Errors -open Util open Libobject -open Names open Libnames -open Term -open Nametab open Mod_subst open Interface diff --git a/library/heads.ml b/library/heads.ml index 024574844..c86a91cc9 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -7,13 +7,11 @@ (************************************************************************) open Pp -open Errors open Util open Names open Term open Mod_subst open Environ -open Libnames open Globnames open Nameops open Libobject diff --git a/library/impargs.ml b/library/impargs.ml index a7d4bcbfb..cd6365289 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -17,7 +17,6 @@ open Environ open Inductive open Libobject open Lib -open Nametab open Pp open Constrexpr open Termops diff --git a/library/libobject.ml b/library/libobject.ml index da9b58a25..ffd87ce80 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -7,8 +7,6 @@ (************************************************************************) open Errors -open Util -open Names open Libnames open Mod_subst diff --git a/library/library.ml b/library/library.ml index 23bf56758..a82b50481 100644 --- a/library/library.ml +++ b/library/library.ml @@ -16,7 +16,6 @@ open Nameops open Safe_typing open Libobject open Lib -open Nametab (*************************************************************************) (*s Load path. Mapping from physical to logical paths etc.*) diff --git a/library/nameops.ml b/library/nameops.ml index 65d5bb989..01a9a6240 100644 --- a/library/nameops.ml +++ b/library/nameops.ml @@ -7,7 +7,6 @@ (************************************************************************) open Pp -open Errors open Util open Names diff --git a/library/nametab.ml b/library/nametab.ml index 0aac3873a..9c2b9b53d 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -7,13 +7,10 @@ (************************************************************************) open Errors -open Util open Pp open Names open Libnames open Globnames -open Nameops -open Declarations exception GlobalizationError of qualid diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 4cfc730a9..488c425cc 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Compat open Errors open Util @@ -15,11 +14,9 @@ open Extend open Ppextend open Constrexpr open Notation_term -open Genarg open Libnames open Tacexpr open Names -open Vernacexpr open Egramml (**************************************************************************) diff --git a/parsing/egramml.ml b/parsing/egramml.ml index abd1bcd5b..c74f36907 100644 --- a/parsing/egramml.ml +++ b/parsing/egramml.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Compat open Names open Pcoq diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml index 75205c964..e7d9ba4b2 100644 --- a/parsing/extrawit.ml +++ b/parsing/extrawit.ml @@ -7,7 +7,6 @@ (************************************************************************) open Errors -open Util open Genarg (* This file defines extra argument types *) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 0970717ed..8af15a1d5 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -17,7 +17,6 @@ open Names open Term open Tacmach open Evd -open Proof_type let init_size=5 diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml index d5eab32c4..25c01f2bd 100644 --- a/plugins/cc/ccproof.ml +++ b/plugins/cc/ccproof.ml @@ -10,7 +10,6 @@ (* proof-trees that will be transformed into proof-terms in cctac.ml4 *) open Errors -open Util open Names open Term open Ccalgo diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 2042f9b05..53c146bfc 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -9,10 +9,7 @@ (* This file is the interface between the c-c algorithm and Coq *) open Evd -open Proof_type open Names -open Libnames -open Nameops open Inductiveops open Declarations open Term @@ -21,12 +18,10 @@ open Tactics open Tacticals open Typing open Ccalgo -open Tacinterp open Ccproof open Pp open Errors open Util -open Format let constant dir s = lazy (Coqlib.gen_constant "CC" dir s) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index e387b31a5..5e128bc42 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 Tacinterp -open Tacmach open Decl_expr open Decl_mode open Pretyping diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 4fc5862c1..31e15081b 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -11,7 +11,6 @@ open Util open Pp open Evd -open Refiner open Proof_type open Tacmach open Tacinterp diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index b72476a75..01f32e4a3 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -7,7 +7,6 @@ (************************************************************************) open Errors -open Util open Pp open Decl_expr open Names diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 4b6bf39be..b6b7e5833 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -7,11 +7,8 @@ (************************************************************************) open Pp -open Errors open Util open Names -open Term -open Declarations open Namegen open Nameops open Libnames @@ -19,8 +16,6 @@ open Globnames open Table open Miniml open Mlutil -open Modutil -open Mod_subst let string_of_id id = let s = Names.string_of_id id in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index ab0e480f9..0556f6d77 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -7,7 +7,6 @@ (************************************************************************) (*i*) -open Errors open Util open Names open Term @@ -20,9 +19,7 @@ open Termops open Inductiveops open Recordops open Namegen -open Summary open Globnames -open Nametab open Miniml open Table open Mlutil diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index a8c9375b1..3b89386d4 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -7,13 +7,10 @@ (************************************************************************) (*i*) -open Pp -open Errors open Util open Names open Libnames open Globnames -open Nametab open Table open Miniml (*i*) diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index d2e8e4951..1211bbf17 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -7,15 +7,12 @@ (************************************************************************) open Names -open Declarations -open Environ open Globnames open Errors open Util open Miniml open Table open Mlutil -open Mod_subst (*S Functions upon ML modules. *) diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 067c41705..34ae1f9ad 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -19,7 +19,6 @@ open Miniml open Mlutil open Modutil open Common -open Declarations (*s Some utility functions. *) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index 27529258b..ec338b1db 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -12,8 +12,6 @@ open Pp open Errors open Util open Names -open Nameops -open Libnames open Miniml open Mlutil open Table diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml index 5cc7f61d9..7abb4dc52 100644 --- a/plugins/firstorder/formula.ml +++ b/plugins/firstorder/formula.ml @@ -10,13 +10,10 @@ open Hipattern open Names open Term open Termops -open Reductionops open Tacmach -open Errors open Util open Declarations open Globnames -open Inductiveops let qflag=ref true diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 58bef84ea..753fdda72 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -12,9 +12,7 @@ open Rules open Instances open Term open Tacmach -open Tactics open Tacticals -open Libnames let update_flags ()= let predref=ref Names.Cpred.empty in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index ee1c44265..e3367b4c2 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -6,11 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Formula -open Sequent open Unify open Rules -open Pp open Errors open Util open Term @@ -20,7 +17,6 @@ open Tactics open Tacticals open Termops open Reductionops -open Declarations open Formula open Sequent open Names diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml index 32c6030d1..37d9edef8 100644 --- a/plugins/firstorder/rules.ml +++ b/plugins/firstorder/rules.ml @@ -14,7 +14,6 @@ open Tacmach open Tactics open Tacticals open Termops -open Declarations open Formula open Sequent open Globnames diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 7e6f65eaa..6d00e8d9f 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -12,7 +12,6 @@ open Util open Formula open Unify open Tacmach -open Names open Globnames open Pp diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index ab18434de..33ea0ac8a 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -6,12 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Util -open Formula -open Tacmach open Term -open Names open Termops open Reductionops diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index b8887c68f..8ea4be631 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -6,9 +6,7 @@ open Namegen open Names open Declarations open Pp -open Entries open Hiddentac -open Evd open Tacmach open Proof_type open Tacticals diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index cb41de283..e2dc149b0 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -7,11 +7,6 @@ open Names open Declarations open Pp open Entries -open Hiddentac -open Evd -open Tacmach -open Proof_type -open Tacticals open Tactics open Indfun_common open Functional_principles_proofs diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 93e1d105e..d11c01672 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -4,7 +4,6 @@ open Names open Term open Glob_term open Glob_ops -open Libnames open Globnames open Indfun_common open Errors diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index f678b898b..44ae42090 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -1,7 +1,6 @@ open Pp open Glob_term open Errors -open Util open Names open Decl_kinds open Misctypes diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 0ad8bc5e6..52562fb37 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -695,7 +695,6 @@ let do_generate_principle on_error register_built interactive_proof in () -open Topconstr let rec add_args id new_args b = match b with | CRef r -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index ff62a5c38..2817c549d 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -149,7 +149,6 @@ let refl_equal = lazy(coq_constant "eq_refl") (* Copy of the standart save mechanism but without the much too *) (* slow reduction function *) (*****************************************************************) -open Declarations open Entries open Decl_kinds open Declare diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 59090fb42..2f6a6a7d7 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -12,13 +12,11 @@ open Util open Names open Term open Pp -open Libnames open Globnames open Tacticals open Tactics open Indfun_common open Tacmach -open Sign open Hiddentac open Misctypes diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index b848d77a7..4fe22a354 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -8,7 +8,6 @@ (* Merging of induction principles. *) -open Libnames open Globnames open Tactics open Indfun_common @@ -21,7 +20,6 @@ open Names open Term open Termops open Declarations -open Environ open Glob_term open Glob_termops open Decl_kinds diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3176ae34a..14d9b7fcb 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Tacexpr open Term open Namegen open Environ @@ -20,9 +19,7 @@ open Nameops open Errors open Util open Closure -open RedFlags open Tacticals -open Typing open Tacmach open Tactics open Nametab @@ -31,12 +28,9 @@ open Declare open Decl_kinds open Tacred open Proof_type -open Vernacinterp open Pfedit -open Topconstr open Glob_term open Pretyping -open Safe_typing open Constrintern open Hiddentac open Misctypes diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index de9dca939..8f34ec495 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -9,21 +9,11 @@ (* This file defines the printer for natural numbers in [nat] *) (*i*) -open Pcoq -open Pp -open Errors -open Util -open Names -open Coqlib open Glob_term -open Libnames open Bigint open Coqlib -open Notation open Pp open Errors -open Util -open Names (*i*) (**********************************************************************) diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml index 1ff28dd79..7cad42d60 100644 --- a/plugins/syntax/z_syntax.ml +++ b/plugins/syntax/z_syntax.ml @@ -6,13 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pcoq open Pp open Errors -open Util open Names -open Topconstr -open Libnames open Bigint exception Non_closed_number @@ -21,7 +17,6 @@ exception Non_closed_number (* Parsing positive via scopes *) (**********************************************************************) -open Libnames open Globnames open Glob_term diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml index 7e281e056..f9eafd3ec 100644 --- a/pretyping/arguments_renaming.ml +++ b/pretyping/arguments_renaming.ml @@ -9,18 +9,9 @@ (*i*) open Names open Globnames -open Decl_kinds open Term -open Sign -open Evd open Environ -open Nametab -open Mod_subst -open Errors -open Util -open Pp open Libobject -open Nameops (*i*) let empty_name_table = (Refmap.empty : name list list Refmap.t) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 5c3e8fe92..163675dfb 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Errors open Util open Names @@ -17,9 +16,7 @@ open Namegen open Declarations open Inductiveops open Environ -open Sign open Reductionops -open Typeops open Type_errors open Glob_term open Glob_ops diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 6c594ef04..fd88049b2 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -6,15 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors open Util -open Pp open Term open Names -open Environ -open Univ -open Evd -open Conv_oracle open Closure open Esubst diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 765cd4ed1..a1b7e5e9d 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -16,10 +16,8 @@ open Globnames open Nametab open Environ open Libobject -open Library open Term open Termops -open Glob_term open Decl_kinds open Mod_subst diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index bd23501a8..0b48654b6 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -14,7 +14,6 @@ Corbineau, Feb 2008 *) (* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *) -open Pp open Errors open Util open Names @@ -24,10 +23,8 @@ open Environ open Typeops open Pretype_errors open Classops -open Recordops open Evarutil open Evarconv -open Retyping open Evd open Termops diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 6329a62b9..50410ad82 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -9,23 +9,17 @@ open Pp open Errors open Util -open Univ open Names open Term -open Declarations -open Inductive open Inductiveops open Environ -open Sign open Glob_term open Glob_ops -open Nameops open Termops open Namegen open Libnames open Globnames open Nametab -open Evd open Mod_subst open Misctypes open Decl_kinds diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 662cd8304..074006872 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Errors open Util open Names diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 90492d50c..3256afd28 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -10,11 +10,9 @@ open Errors open Util open Pp open Names -open Univ open Term open Termops open Namegen -open Sign open Pre_env open Environ open Evd @@ -1894,7 +1892,6 @@ let check_evars env initial_sigma sigma c = | _ -> iter_constr proc_rec c in proc_rec c -open Glob_term (****************************************) (* Operations on value/type constraints *) diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 66ebb7f78..a73a74f45 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -13,9 +13,7 @@ open Names open Nameops open Term open Termops -open Sign open Environ -open Libnames open Globnames open Mod_subst diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index e85657083..a090094aa 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -6,17 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Pp open Util open Names -open Sign -open Term open Globnames -open Nametab -open Decl_kinds open Misctypes -open Locus open Glob_term (* Untyped intermediate terms, after ASTs and before constr. *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 7ccd62776..025f7f668 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -20,16 +20,11 @@ open Nameops open Term open Namegen open Declarations -open Entries open Inductive open Inductiveops open Environ open Reductionops -open Typeops -open Type_errors -open Safe_typing open Nametab -open Sign type dep_flag = bool diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1c7302fe0..19126f01b 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -13,7 +13,6 @@ open Univ open Term open Termops open Namegen -open Sign open Declarations open Environ open Reductionops diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index c9f60df61..161243587 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Misctypes open Locus (** Utilities on occurrences *) diff --git a/pretyping/matching.ml b/pretyping/matching.ml index a4c16b724..bc9c832ae 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -16,9 +16,6 @@ open Nameops open Termops open Reductionops open Term -open Glob_term -open Sign -open Environ open Pattern open Patternops open Misctypes diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index fc84c8efa..9d5777358 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -12,7 +12,6 @@ (* This file is about generating new or fresh names and dealing with alpha-renaming *) -open Errors open Util open Names open Term diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 68382f15a..c3b03e209 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -14,8 +14,6 @@ open Nameops open Term open Glob_term open Glob_ops -open Environ -open Nametab open Pp open Mod_subst open Misctypes diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 57bb8512e..d9a050c08 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,17 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Util open Names -open Sign open Term open Termops open Namegen open Environ open Type_errors -open Glob_term -open Inductiveops type pretype_error = (* Old Case *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index cbaa98844..511323695 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -33,11 +33,8 @@ open Reductionops open Environ open Type_errors open Typeops -open Libnames open Globnames open Nameops -open Classops -open Recordops open Evarutil open Pretype_errors open Glob_term @@ -55,7 +52,6 @@ type pure_open_constr = evar_map * constr (************************************************************************) (* This concerns Cases *) -open Declarations open Inductive open Inductiveops diff --git a/pretyping/program.ml b/pretyping/program.ml index 06c4a1d74..db821f176 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -6,22 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Errors open Util open Names open Term -open Reductionops -open Environ -open Typeops -open Pretype_errors -open Classops -open Recordops -open Evarutil -open Evarconv -open Retyping -open Evd -open Termops type message = string diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 4f7d06e39..7c128d245 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -20,9 +20,7 @@ open Names open Globnames open Nametab open Term -open Typeops open Libobject -open Library open Mod_subst open Reductionops diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index bdc6cb72a..0b5ad7b0b 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Errors open Util open Names @@ -14,10 +13,8 @@ open Term open Termops open Univ open Evd -open Declarations open Environ open Closure -open Esubst open Reduction exception Elimconst diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 22ffcb56e..1909528c5 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -7,14 +7,12 @@ (************************************************************************) open Errors -open Util open Term open Inductive open Inductiveops open Names open Reductionops open Environ -open Typeops open Declarations open Termops diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index ae4e3b2f8..9791598fd 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -10,21 +10,16 @@ open Pp open Errors open Util open Names -open Nameops open Term open Libnames open Globnames open Termops open Namegen -open Declarations -open Inductive open Libobject open Environ open Closure open Reductionops open Cbv -open Glob_term -open Pattern open Patternops open Matching open Locus diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 49c93ffdd..8e56d59a6 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -7,10 +7,8 @@ (************************************************************************) (*i*) -open Errors open Util open Term -open Sign open Names open Globnames open Mod_subst diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 9bd539abc..e4f481e58 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -12,10 +12,7 @@ open Util open Names open Nameops open Term -open Sign open Environ -open Libnames -open Nametab open Locus (* Sorts and sort family *) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 3e9183780..8fd0f768e 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -14,9 +14,6 @@ open Term open Sign open Evd open Environ -open Nametab -open Mod_subst -open Errors open Util open Typeclasses_errors open Libobject diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 5350ecfcc..4a0b66a7b 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -8,16 +8,10 @@ (*i*) open Names -open Decl_kinds open Term -open Sign open Evd open Environ -open Nametab -open Mod_subst open Constrexpr -open Pp -open Util open Globnames (*i*) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index ebb30bf35..df1833f84 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -8,7 +8,6 @@ open Errors open Util -open Names open Term open Environ open Reductionops @@ -17,7 +16,6 @@ open Pretype_errors open Inductive open Inductiveops open Typeops -open Evd open Arguments_renaming let meta_type evd mv = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 20446ba00..7821a5f4f 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,20 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Errors open Util open Names -open Nameops open Term open Termops open Namegen -open Sign open Environ open Evd open Reduction open Reductionops -open Glob_term open Evarutil open Pretype_errors open Retyping diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index c077fbe83..f99d8c109 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -612,7 +612,6 @@ let pr_red_flag pr r = pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++ hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")) -open Genarg let pr_metaid id = str"?" ++ pr_id id diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 50baf36f8..7118388cb 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -220,7 +220,6 @@ let rec pr_glob_generic prc prlc prtac prpat x = try pi2 (Stringmap.find s !genarg_pprule) prc prlc prtac x with Not_found -> str "[no printer for " ++ str s ++ str "]" -open Closure let rec pr_generic prc prlc prtac prpat x = match Genarg.genarg_tag x with @@ -543,7 +542,6 @@ let linfo = 5 let level_of (n,p) = match p with E -> n | L -> n-1 | Prec n -> n | Any -> lseq -open Closure (** A printer for tactics that polymorphically works on the three "raw", "glob" and "typed" levels; in practice, the environment is diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 70094b48c..748e5297b 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -8,8 +8,6 @@ open Pp open Names -open Nameops -open Nametab let pr_located = Loc.pr_located @@ -20,14 +18,10 @@ open Extend open Vernacexpr open Ppconstr open Pptactic -open Glob_term -open Genarg open Libnames -open Ppextend open Constrexpr open Constrexpr_ops open Decl_kinds -open Tacinterp open Declaremods let pr_spc_lconstr = pr_sep_com spc pr_lconstr_expr diff --git a/printing/prettyp.ml b/printing/prettyp.ml index d81a3389f..86b2da2eb 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -18,12 +18,7 @@ open Nameops open Term open Termops open Declarations -open Inductive -open Inductiveops -open Sign -open Reduction open Environ -open Declare open Impargs open Libobject open Libnames diff --git a/printing/printer.ml b/printing/printer.ml index 33d099289..70a90b8ea 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -10,13 +10,9 @@ open Pp open Errors open Util open Names -open Nameops open Term open Sign open Environ -open Global -open Declare -open Libnames open Globnames open Nametab open Evd @@ -24,10 +20,8 @@ open Proof_type open Refiner open Pfedit open Constrextern -open Tacexpr open Ppconstr -open Store.Field let emacs_str s = if !Flags.print_emacs then s else "" @@ -638,8 +632,6 @@ let pr_instance_gmap insts = open Declarations open Termops open Reduction -open Inductive -open Inductiveops let print_params env params = if params = [] then mt () else pr_rel_context env params ++ brk(1,2) diff --git a/printing/tactic_printer.ml b/printing/tactic_printer.ml index 3c96a41b9..551db10d5 100644 --- a/printing/tactic_printer.ml +++ b/printing/tactic_printer.ml @@ -8,8 +8,6 @@ open Pp open Errors -open Util -open Sign open Evd open Tacexpr open Proof_type diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 20a2ebd06..f3e414126 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -14,19 +14,15 @@ open Nameops open Term open Termops open Namegen -open Sign open Environ open Evd open Reduction open Reductionops -open Glob_term -open Pattern open Tacred open Pretype_errors open Evarutil open Unification open Mod_subst -open Coercion open Misctypes (* Abbreviations *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 3b188c8d0..d7379c902 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -6,26 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp -open Errors -open Util open Names -open Nameops open Term open Termops -open Sign -open Environ open Evd -open Evarutil -open Proof_type open Refiner open Logic open Reduction -open Reductionops open Tacmach -open Glob_term -open Pattern -open Tacexpr open Clenv diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 0024a5c10..260d6d092 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -7,13 +7,9 @@ (************************************************************************) open Errors -open Util open Names -open Term open Evd open Evarutil -open Sign -open Refiner (******************************************) (* Instantiation of existential variables *) diff --git a/proofs/logic.ml b/proofs/logic.ml index a79485d1e..dcf1e4c73 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -11,21 +11,15 @@ open Errors open Util open Names open Nameops -open Evd open Term open Termops -open Sign open Environ open Reductionops -open Inductive open Inductiveops open Typing open Proof_type -open Typeops open Type_errors open Retyping -open Evarutil -open Tacexpr open Misctypes type refiner_error = diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index d528e95a8..f7d9446b5 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -7,20 +7,11 @@ (************************************************************************) open Pp -open Errors -open Util open Names -open Nameops -open Sign -open Term open Entries open Environ open Evd -open Typing open Refiner -open Tacexpr -open Proof_type -open Lib let refining = Proof_global.there_are_pending_proofs let check_no_pending_proofs = Proof_global.check_no_pending_proof diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index a3e240c8d..bedf058fc 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -314,7 +314,6 @@ let maximal_unfocus k p = module Bullet = struct - open Store.Field type t = Vernacexpr.bullet diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index dec7b2b07..4a404b6f3 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -7,12 +7,9 @@ (************************************************************************) (*i*) -open Environ open Evd open Names -open Libnames open Term -open Pp open Tacexpr (* open Decl_expr *) open Glob_term diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 4b04374da..910653ddb 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -9,14 +9,8 @@ open Pp open Errors open Util -open Term -open Termops -open Sign open Evd -open Sign open Environ -open Reductionops -open Type_errors open Proof_type open Logic diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 85ae41a53..cab124d93 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -6,12 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Errors open Util open Names open Namegen -open Sign open Term open Termops open Environ @@ -23,7 +21,6 @@ open Tacred open Proof_type open Logic open Refiner -open Tacexpr let re_sig it gc = { it = it; sigma = gc } @@ -194,8 +191,6 @@ let rename_hyp l = with_check (rename_hyp_no_check l) (* Pretty-printers *) open Pp -open Tacexpr -open Glob_term let db_pr_goal sigma g = let env = Goal.V82.env sigma g in diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index 49026cc0b..10ce0e76b 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Constrextern open Pp open Tacexpr open Termops diff --git a/tactics/auto.ml b/tactics/auto.ml index 8d0d0e78b..5068552d1 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -15,11 +15,8 @@ open Namegen open Term open Termops open Inductiveops -open Sign open Environ -open Inductive open Evd -open Reduction open Typing open Pattern open Patternops @@ -28,7 +25,6 @@ open Tacmach open Proof_type open Pfedit open Genredexpr -open Evar_refiner open Tacred open Tactics open Tacticals @@ -39,9 +35,7 @@ open Globnames open Nametab open Smartlocate open Libobject -open Library open Printer -open Declarations open Tacexpr open Mod_subst open Misctypes diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 00e8e1384..d2d18c53b 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -7,19 +7,15 @@ (************************************************************************) open Equality -open Hipattern open Names open Pp open Proof_type open Tacticals -open Tacinterp open Tactics open Term open Termops open Errors open Util -open Glob_term -open Vernacinterp open Tacexpr open Mod_subst open Locus diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 3a0f1000f..e8cde2967 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -8,7 +8,6 @@ open Term open Names -open Termdn open Pattern open Globnames diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 6389e0d33..14a9ae9c2 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -6,17 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Errors open Term -open Proof_type open Hipattern open Tacmach open Tacticals open Tactics open Coqlib open Reductionops -open Glob_term open Misctypes (* Absurd *) diff --git a/tactics/elim.ml b/tactics/elim.ml index 304b4117d..a2ec6dfa5 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -6,24 +6,16 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Errors open Util open Names open Term open Termops -open Environ -open Libnames -open Reduction open Inductiveops -open Proof_type -open Clenv open Hipattern open Tacmach open Tacticals open Tactics -open Hiddentac -open Genarg open Tacexpr open Misctypes diff --git a/tactics/equality.ml b/tactics/equality.ml index 16669b567..b4cb48285 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -11,7 +11,6 @@ open Errors open Util open Names open Nameops -open Univ open Term open Termops open Namegen @@ -21,26 +20,19 @@ open Environ open Libnames open Globnames open Reductionops -open Typeops open Typing open Retyping open Tacmach -open Proof_type open Logic -open Evar_refiner -open Pattern open Matching open Hipattern open Tacexpr open Tacticals open Tactics open Tacred -open Glob_term open Coqlib -open Vernacexpr open Declarations open Indrec -open Printer open Clenv open Clenvtac open Evd diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index d2bc7fcf4..dd02adde1 100644 --- a/tactics/evar_tactics.ml +++ b/tactics/evar_tactics.ml @@ -6,16 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term -open Pp open Errors open Evar_refiner open Tacmach open Tacexpr open Refiner -open Proof_type open Evd -open Sign open Locus (* The instantiate tactic *) diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 9c7208a0e..77379cb74 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -6,13 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term -open Proof_type -open Tacmach -open Glob_term open Refiner -open Genarg open Tacexpr open Tactics open Util diff --git a/tactics/inv.ml b/tactics/inv.ml index 976947f2e..cb1ffb385 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -14,26 +14,16 @@ open Nameops open Term open Termops open Namegen -open Global -open Sign open Environ open Inductiveops open Printer -open Reductionops open Retyping open Tacmach -open Proof_type -open Evar_refiner open Clenv -open Tactics open Tacticals open Tactics open Elim open Equality -open Typing -open Pattern -open Matching -open Glob_term open Misctypes open Tacexpr @@ -208,7 +198,6 @@ let split_dep_and_nodep hyps gl = if var_occurs_in_pf gl id then (d::l1,l2) else (l1,d::l2)) hyps ([],[]) -open Coqlib (* Computation of dids is late; must have been done in rewrite_equations*) (* Will keep generalizing and introducing back and forth... *) diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 9dc266ef1..5242d0f3e 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -10,7 +10,6 @@ open Pp open Errors open Util open Names -open Nameops open Term open Termops open Namegen @@ -18,21 +17,15 @@ open Sign open Evd open Printer open Reductionops -open Declarations open Entries open Inductiveops open Environ open Tacmach -open Proof_type open Pfedit -open Evar_refiner open Clenv open Declare open Tacticals open Tactics -open Inv -open Vernacexpr -open Safe_typing open Decl_kinds let no_inductive_inconstr env constr = diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index 83f65b274..5d5972089 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -6,12 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Util open Names open Term -open Libobject -open Library open Pattern open Globnames diff --git a/tactics/refine.ml b/tactics/refine.ml index b0705c024..fc2da8d0a 100644 --- a/tactics/refine.ml +++ b/tactics/refine.ml @@ -54,10 +54,7 @@ open Term open Termops open Namegen open Tacmach -open Sign open Environ -open Reduction -open Typing open Tactics open Tacticals open Printer diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 459236fe5..b0997c067 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -8,9 +8,6 @@ open Constrintern open Closure -open RedFlags -open Declarations -open Entries open Libobject open Pattern open Patternops @@ -19,7 +16,6 @@ open Pp open Genredexpr open Glob_term open Glob_ops -open Sign open Tacred open Errors open Util @@ -39,18 +35,13 @@ open Constrexpr_ops open Term open Termops open Tacexpr -open Safe_typing -open Typing open Hiddentac open Genarg -open Decl_kinds open Mod_subst open Printer open Inductiveops -open Syntax_def open Pretyping open Extrawit -open Pcoq open Evd open Misctypes open Miscops diff --git a/tactics/tactic_option.ml b/tactics/tactic_option.ml index b846c9eb7..7989b41db 100644 --- a/tactics/tactic_option.ml +++ b/tactics/tactic_option.ml @@ -7,7 +7,6 @@ (************************************************************************) open Libobject -open Proof_type open Pp let declare_tactic_option ?(default=Tacexpr.TacId []) name = diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 150e0050c..aaa75a4e2 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -14,20 +14,9 @@ open Term open Termops open Sign open Declarations -open Inductive -open Reduction -open Environ -open Libnames -open Refiner open Tacmach open Clenv open Clenvtac -open Glob_term -open Pattern -open Matching -open Genarg -open Tacexpr -open Locus open Misctypes (************************************************************************) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 895b6dc35..1ccb3ffdb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -16,7 +16,6 @@ open Term open Termops open Namegen open Declarations -open Inductive open Inductiveops open Reductionops open Environ @@ -28,14 +27,12 @@ open Genredexpr open Tacmach open Proof_type open Logic -open Evar_refiner open Clenv open Clenvtac open Refiner open Tacticals open Hipattern open Coqlib -open Nametab open Tacexpr open Decl_kinds open Evarutil diff --git a/tactics/termdn.ml b/tactics/termdn.ml index ff847ba6e..ffcde31ae 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -6,16 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors -open Util open Names -open Nameops open Term open Pattern open Patternops -open Glob_term open Globnames -open Nametab (* Discrimination nets of terms. See the module dn.ml for further explanations. diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index e8abd8e17..59cc3afd8 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -11,20 +11,12 @@ open Tacmach open Errors -open Util -open Flags -open Decl_kinds open Pp -open Entries open Termops open Declarations -open Declare open Term open Names open Globnames -open Goptions -open Mod_subst -open Indrec open Inductiveops open Tactics open Tacticals diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 4c991056e..2338e7f39 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -12,7 +12,6 @@ open Printer open Names open Term open Evd -open Sign open Globnames (*i*) diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml index 74e4701c0..d1e379cca 100644 --- a/toplevel/cerrors.ml +++ b/toplevel/cerrors.ml @@ -8,7 +8,6 @@ open Pp open Errors -open Util open Indtypes open Type_errors open Pretype_errors diff --git a/toplevel/class.ml b/toplevel/class.ml index 78b712301..dfb74b9e9 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -7,25 +7,17 @@ (************************************************************************) open Errors -open Util open Pp open Names -open Nameops open Term open Termops -open Inductive -open Declarations open Entries open Environ -open Inductive -open Lib open Classops open Declare -open Libnames open Globnames open Nametab open Decl_kinds -open Safe_typing let strength_min l = if List.mem Local l then Local else Global diff --git a/toplevel/classes.ml b/toplevel/classes.ml index b3f9d4872..c4c017577 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -8,23 +8,17 @@ (*i*) open Names -open Decl_kinds open Term -open Sign -open Entries open Evd open Environ open Nametab -open Mod_subst open Errors -open Pp open Util open Typeclasses_errors open Typeclasses open Libnames open Globnames open Constrintern -open Glob_term open Constrexpr (*i*) @@ -73,7 +67,6 @@ type binder_list = (identifier Loc.located * bool * constr_expr) list (* Declare everything in the parameters as implicit, and the class instance as well *) -open Topconstr let type_ctx_instance evars env ctx inst subst = let rec aux (subst, instctx) l = function diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index eac009984..718e65b50 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -7,8 +7,6 @@ (************************************************************************) open Pp -open System -open Toplevel let (/) = Filename.concat diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f06edd316..df155eebb 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -13,9 +13,7 @@ open System open Flags open Names open Libnames -open Nameops open States -open Toplevel open Coqinit let () = at_exit flush_all diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b4648246a..3cdeb0be9 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -7,15 +7,12 @@ (************************************************************************) open Pp -open Errors open Util -open Flags open Names open Nameops open Namegen open Term open Termops -open Inductive open Indtypes open Sign open Environ @@ -23,11 +20,9 @@ open Pretype_errors open Type_errors open Typeclasses_errors open Indrec -open Reduction open Cases open Logic open Printer -open Glob_term open Evd let pr_lconstr c = quote (pr_lconstr c) diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml index 13b4d13fe..a7bc895c9 100644 --- a/toplevel/ide_slave.ml +++ b/toplevel/ide_slave.ml @@ -7,12 +7,9 @@ (************************************************************************) open Vernacexpr -open Names open Errors -open Util open Pp open Printer -open Namegen (** Ide_slave : an implementation of [Interface], i.e. mainly an interp function and a rewind function. This specialized loop is triggered diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index bb60fed73..b99f83e5c 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -15,7 +15,6 @@ declaring new schemes *) open Pp -open Flags open Errors open Util open Names @@ -31,10 +30,7 @@ open Globnames open Goptions open Nameops open Termops -open Typeops -open Inductiveops open Pretyping -open Topconstr open Nametab open Smartlocate open Vernacexpr diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml index 5680f993e..0c9cf877d 100644 --- a/toplevel/lemmas.ml +++ b/toplevel/lemmas.ml @@ -26,7 +26,6 @@ open Declare open Pretyping open Termops open Namegen -open Evd open Evarutil open Reductionops open Constrexpr diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml index d85695d50..0866db092 100644 --- a/toplevel/libtypes.ml +++ b/toplevel/libtypes.ml @@ -10,7 +10,6 @@ open Term open Summary open Libobject open Globnames -open Names (* * Module construction *) diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 77949a126..4eebfc8f7 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -19,11 +19,9 @@ open Notation_ops open Ppextend open Extend open Libobject -open Summary open Constrintern open Vernacexpr open Pcoq -open Glob_term open Libnames open Tok open Lexer diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 6338fa9e4..2a0f3c167 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -1,18 +1,9 @@ open Printf -open Pp -open Environ -open Term -open Names open Globnames -open Summary open Libobject open Entries open Decl_kinds -open Errors -open Util -open Evd open Declare -open Proof_type (** - Get types of existentials ; @@ -537,7 +528,6 @@ let declare_definition prg = (fun local gr -> prg.prg_hook local gr; gr) open Pp -open Ppconstr let rec lam_index n t acc = match kind_of_term t with diff --git a/toplevel/record.ml b/toplevel/record.ml index 88ff5e646..978329e13 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -17,13 +17,8 @@ open Environ open Declarations open Entries open Declare -open Nametab open Constrintern -open Command -open Inductive -open Safe_typing open Decl_kinds -open Indtypes open Type_errors open Constrexpr open Constrexpr_ops diff --git a/toplevel/search.ml b/toplevel/search.ml index 3ab4feb5e..81fdf84aa 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -10,12 +10,9 @@ open Pp open Errors open Util open Names -open Nameops open Term -open Glob_term open Declarations open Libobject -open Declare open Environ open Pattern open Matching diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml index fe6dbe642..ace83cf64 100644 --- a/toplevel/toplevel.ml +++ b/toplevel/toplevel.ml @@ -8,9 +8,7 @@ open Pp open Errors -open Util open Flags -open Cerrors open Vernac open Pcoq diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b897a6d91..a494a10cc 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -10,7 +10,6 @@ open Pp open Errors -open Util open Flags open System open Vernacexpr diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c30c6c0c1..18cef702c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -13,7 +13,6 @@ open Errors open Util open Flags open Names -open Entries open Nameops open Term open Pfedit @@ -26,13 +25,10 @@ open Command open Goptions open Libnames open Globnames -open Nametab open Vernacexpr open Decl_kinds open Constrexpr -open Pretyping open Redexpr -open Syntax_def open Lemmas open Declaremods open Misctypes diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 242667f3a..dca47f714 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -8,12 +8,6 @@ open Pp open Errors -open Util -open Names -open Libnames -open Himsg -open Proof_type -open Tacinterp let disable_drop e = if e <> Drop then e |