diff options
| author | regisgia | 2012-09-14 15:59:23 +0000 |
|---|---|---|
| committer | regisgia | 2012-09-14 15:59:23 +0000 |
| commit | 6dae53d279afe2b8dcfc43dd2aded9431944c5c8 (patch) | |
| tree | 716cb069d32317bdc620dc997ba6b0eb085ffbdd /library | |
| parent | 0affc36749655cd0a906af0c0aad64fd350d4fec (diff) | |
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
Diffstat (limited to 'library')
| -rw-r--r-- | library/assumptions.ml | 3 | ||||
| -rw-r--r-- | library/declare.ml | 1 | ||||
| -rw-r--r-- | library/decls.ml | 1 | ||||
| -rw-r--r-- | library/dischargedhypsmap.ml | 11 | ||||
| -rw-r--r-- | library/global.ml | 3 | ||||
| -rw-r--r-- | library/globnames.ml | 3 | ||||
| -rw-r--r-- | library/goptions.ml | 4 | ||||
| -rw-r--r-- | library/heads.ml | 2 | ||||
| -rw-r--r-- | library/impargs.ml | 1 | ||||
| -rw-r--r-- | library/libobject.ml | 2 | ||||
| -rw-r--r-- | library/library.ml | 1 | ||||
| -rw-r--r-- | library/nameops.ml | 1 | ||||
| -rw-r--r-- | library/nametab.ml | 3 |
13 files changed, 0 insertions, 36 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml index 6bab64a7b5..2d4b6169d1 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 83f9e12d09..58ad1f00f0 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 dd8a702e85..f6fa626b17 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 b8a7da3671..c26f652dfa 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 e7f37801b3..c2bd551284 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 c5e668ce32..8d298bc949 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 8330ca3d2b..861109d3db 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 0245748444..c86a91cc97 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 a7d4bcbfba..cd6365289c 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 da9b58a25a..ffd87ce806 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 23bf567580..a82b504812 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 65d5bb989d..01a9a62403 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 0aac3873ad..9c2b9b53d7 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 |