diff options
Diffstat (limited to 'interp/smartlocate.mli')
| -rw-r--r-- | interp/smartlocate.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 5f772c591..86aa69681 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -7,7 +7,6 @@ (************************************************************************) open Loc -open Pp open Names open Libnames open Globnames |