Remove many superfluous 'open' indicated by ocamlc -w +33

 With ocaml 4.01, the 'unused open' warning also checks the mli :-)

 Beware: some open are reported as useless when compiling with camlp5,
 but are necessary for compatibility with camlp4. These open are now
 marked with a comment.

4 files changed, 0 insertions, 11 deletions

diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 56b1a3f1cb..d6f21fb86b 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -6,7 +6,6 @@ open Vars
 open Context
 open Namegen
 open Names
-open Declarations
 open Declareops
 open Pp
 open Entries
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index cc9ae912dc..2dd78d8908 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -18,7 +18,6 @@ open Indfun
 open Genarg
 open Tacticals
 open Misctypes
-open Miscops
 
 let pr_binding prc = function
   | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 56fc9bd2cd..91a5ddf826 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,10 +1,3 @@
-open Names
-open Term
-open Pp
-open Indfun_common
-open Libnames
-open Glob_term
-open Declarations
 open Misctypes
 
 val do_generate_principle :  
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f951debfde..ca0a432d6a 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -10,7 +10,6 @@ open Term
 open Vars
 open Namegen
 open Environ
-open Declarations
 open Declareops
 open Entries
 open Pp
@@ -24,7 +23,6 @@ open Tacticals
 open Tacmach
 open Tactics
 open Nametab
-open Decls
 open Declare
 open Decl_kinds
 open Tacred