diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 20:11:47 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:42:01 +0200 |
| commit | 4e84e83911c1cf7613a35b921b1e68e097f84b5a (patch) | |
| tree | 86caa28a08dde1e771c365350550ffdd633ba1f8 /vernac | |
| parent | e1d2a898feacbe4bd363818f259bce5fd74c2ee7 (diff) | |
Remove unused [open] statements
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 2 | ||||
| -rw-r--r-- | vernac/classes.ml | 2 | ||||
| -rw-r--r-- | vernac/obligations.mli | 1 | ||||
| -rw-r--r-- | vernac/search.ml | 2 | ||||
| -rw-r--r-- | vernac/search.mli | 1 |
5 files changed, 0 insertions, 8 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 015552d68..25091f783 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -9,7 +9,6 @@ (* This file is about the automatic generation of schemes about decidable equality, created by Vincent Siles, Oct 2007 *) -open Tacmach open CErrors open Util open Pp @@ -716,7 +715,6 @@ let compute_lb_goal ind lnamesparrec nparrec = ))), eff let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = - let open EConstr in let list_id = list_id lnamesparrec in let avoid = ref [] in let first_intros = diff --git a/vernac/classes.ml b/vernac/classes.ml index 833719965..d515b0c9b 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -66,8 +66,6 @@ let _ = Hook.set Typeclasses.classes_transparent_state_hook (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db)) -open Vernacexpr - (** TODO: add subinstances *) let existing_instance glob g info = let c = global g in diff --git a/vernac/obligations.mli b/vernac/obligations.mli index 11366fe91..a276f9f9a 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -12,7 +12,6 @@ open Evd open Names open Pp open Globnames -open Vernacexpr open Decl_kinds (** Forward declaration. *) diff --git a/vernac/search.ml b/vernac/search.ml index 6279b17ae..5b6e9a9c3 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -14,11 +14,9 @@ open Declarations open Libobject open Environ open Pattern -open Printer open Libnames open Globnames open Nametab -open Goptions module NamedDecl = Context.Named.Declaration diff --git a/vernac/search.mli b/vernac/search.mli index 82b79f75d..e34522d8a 100644 --- a/vernac/search.mli +++ b/vernac/search.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term open Environ |