diff options
Diffstat (limited to 'printing/prettyp.ml')
| -rw-r--r-- | printing/prettyp.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index d81a3389f7..86b2da2eb0 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -18,12 +18,7 @@ open Nameops open Term open Termops open Declarations -open Inductive -open Inductiveops -open Sign -open Reduction open Environ -open Declare open Impargs open Libobject open Libnames |