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 /proofs | |
| parent | e1d2a898feacbe4bd363818f259bce5fd74c2ee7 (diff) | |
Remove unused [open] statements
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.mli | 1 | ||||
| -rw-r--r-- | proofs/goal.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 3 | ||||
| -rw-r--r-- | proofs/refiner.ml | 1 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 1 |
5 files changed, 0 insertions, 7 deletions
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index 5b7164705..26069207e 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -8,7 +8,6 @@ (** Legacy components of the previous proof engine. *) -open Term open Clenv open EConstr open Unification diff --git a/proofs/goal.ml b/proofs/goal.ml index 9046f4534..fc8e635a0 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -8,7 +8,6 @@ open Util open Pp -open Term open Sigma.Notations module NamedDecl = Context.Named.Declaration diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 03bc5e471..e59db9e42 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -11,9 +11,6 @@ open Evd open Names open Term -open Glob_term -open Nametab -open Misctypes (** This module defines the structure of proof tree and the tactic type. So, it is used by [Proof_tree] and [Refiner] *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index bc12b3ba7..259e96a27 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open Evd -open Environ open Proof_type open Logic diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 627a8e0e7..e6e60e27f 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -15,7 +15,6 @@ open Proof_type open Redexpr open Pattern open Locus -open Misctypes (** Operations for handling terms under a local typing context. *) |