diff options
| -rw-r--r-- | parsing/printer.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index 561c85785..0d4cdfe5a 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -20,7 +20,6 @@ open Global open Declare open Libnames open Nametab -open Ppconstr open Evd open Proof_type open Decl_mode |