diff options
Diffstat (limited to 'toplevel/command.mli')
| -rw-r--r-- | toplevel/command.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/toplevel/command.mli b/toplevel/command.mli index 1de47d38c4..3a38e52cee 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -11,7 +11,6 @@ open Term open Entries open Libnames open Globnames -open Tacexpr open Vernacexpr open Constrexpr open Decl_kinds |