diff options
Diffstat (limited to 'proofs/tacmach.mli')
| -rw-r--r-- | proofs/tacmach.mli | 1 |
1 files changed, 0 insertions, 1 deletions
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. *) |