diff options
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 59090fb42..2f6a6a7d7 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -12,13 +12,11 @@ open Util open Names open Term open Pp -open Libnames open Globnames open Tacticals open Tactics open Indfun_common open Tacmach -open Sign open Hiddentac open Misctypes |