From 6dae53d279afe2b8dcfc43dd2aded9431944c5c8 Mon Sep 17 00:00:00 2001 From: regisgia Date: Fri, 14 Sep 2012 15:59:23 +0000 Subject: This patch removes unused "open" (automatically generated from compiler warnings). I was afraid that such a brutal refactoring breaks some obscure invariant about linking order and side-effects but the standard library still compiles. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15800 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/cc/ccalgo.ml | 1 - plugins/cc/ccproof.ml | 1 - plugins/cc/cctac.ml | 5 ----- plugins/decl_mode/decl_interp.ml | 1 - plugins/decl_mode/decl_proof_instr.ml | 1 - plugins/decl_mode/ppdecl_proof.ml | 1 - plugins/extraction/common.ml | 5 ----- plugins/extraction/extraction.ml | 3 --- plugins/extraction/mlutil.ml | 3 --- plugins/extraction/modutil.ml | 3 --- plugins/extraction/ocaml.ml | 1 - plugins/extraction/scheme.ml | 2 -- plugins/firstorder/formula.ml | 3 --- plugins/firstorder/ground.ml | 2 -- plugins/firstorder/instances.ml | 4 ---- plugins/firstorder/rules.ml | 1 - plugins/firstorder/sequent.ml | 1 - plugins/firstorder/unify.ml | 4 ---- plugins/funind/functional_principles_proofs.ml | 2 -- plugins/funind/functional_principles_types.ml | 5 ----- plugins/funind/glob_term_to_relation.ml | 1 - plugins/funind/glob_termops.ml | 1 - plugins/funind/indfun.ml | 1 - plugins/funind/indfun_common.ml | 1 - plugins/funind/invfun.ml | 2 -- plugins/funind/merge.ml | 2 -- plugins/funind/recdef.ml | 6 ------ plugins/syntax/nat_syntax.ml | 10 ---------- plugins/syntax/z_syntax.ml | 5 ----- 29 files changed, 78 deletions(-) (limited to 'plugins') 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 -- cgit v1.2.3