diff options
Diffstat (limited to 'plugins/extraction/common.ml')
| -rw-r--r-- | plugins/extraction/common.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 4b6bf39be..b6b7e5833 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -7,11 +7,8 @@ (************************************************************************) open Pp -open Errors open Util open Names -open Term -open Declarations open Namegen open Nameops open Libnames @@ -19,8 +16,6 @@ open Globnames open Table open Miniml open Mlutil -open Modutil -open Mod_subst let string_of_id id = let s = Names.string_of_id id in |