diff options
Diffstat (limited to 'plugins/extraction/modutil.mli')
| -rw-r--r-- | plugins/extraction/modutil.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 52805bc87..42c8b11f3 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -7,11 +7,8 @@ (************************************************************************) open Names -open Declarations -open Environ open Globnames open Miniml -open Mod_subst (*s Functions upon ML modules. *) |