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 /engine | |
| parent | e1d2a898feacbe4bd363818f259bce5fd74c2ee7 (diff) | |
Remove unused [open] statements
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 1 | ||||
| -rw-r--r-- | engine/eConstr.mli | 1 | ||||
| -rw-r--r-- | engine/evarutil.ml | 1 | ||||
| -rw-r--r-- | engine/evd.ml | 4 | ||||
| -rw-r--r-- | engine/proofview.mli | 1 | ||||
| -rw-r--r-- | engine/termops.ml | 1 | ||||
| -rw-r--r-- | engine/universes.ml | 1 |
7 files changed, 0 insertions, 10 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index bb9075e74..54d3ce6cf 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open CSig open CErrors open Util open Names diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 3a9469e55..693b592fd 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -9,7 +9,6 @@ open CSig open Names open Constr -open Context open Environ type t diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 1624dc93e..fba466107 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -10,7 +10,6 @@ open CErrors open Util open Names open Term -open Vars open Termops open Namegen open Pre_env diff --git a/engine/evd.ml b/engine/evd.ml index 5419a10a8..6b1e1a855 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -14,8 +14,6 @@ open Nameops open Term open Vars open Environ -open Globnames -open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -360,8 +358,6 @@ module EvMap = Evar.Map module EvNames : sig -open Misctypes - type t val empty : t diff --git a/engine/proofview.mli b/engine/proofview.mli index a3b0304b1..da8a8fecd 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -13,7 +13,6 @@ state and returning a value of type ['a]. *) open Util -open Term open EConstr (** Main state of tactics *) diff --git a/engine/termops.ml b/engine/termops.ml index 29dcddbb0..19e62f8e6 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1427,7 +1427,6 @@ let dependency_closure env sigma sign hyps = List.rev lh let global_app_of_constr sigma c = - let open Univ in let open Globnames in match EConstr.kind sigma c with | Const (c, u) -> (ConstRef c, u), None diff --git a/engine/universes.ml b/engine/universes.ml index ab561784c..1900112dd 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -13,7 +13,6 @@ open Term open Environ open Univ open Globnames -open Decl_kinds let pr_with_global_universes l = try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) |