diff options
Diffstat (limited to 'plugins/ltac/rewrite.mli')
| -rw-r--r-- | plugins/ltac/rewrite.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 7a20838a2..6683d753b 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -14,7 +14,6 @@ open Constrexpr open Tacexpr open Misctypes open Evd -open Proof_type open Tacinterp (** TODO: document and clean me! *) |