diff options
Diffstat (limited to 'printing/printer.mli')
| -rw-r--r-- | printing/printer.mli | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/printing/printer.mli b/printing/printer.mli index 2d7f0a5d33..6ca55b16b5 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -8,19 +8,14 @@ open Pp open Names -open Libnames open Globnames open Term open Context open Environ -open Glob_term open Pattern -open Nametab -open Termops open Evd open Proof_type open Glob_term -open Tacexpr (** These are the entry points for printing terms, context, tac, ... *) |