17 files changed, 19 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index fd49623986..023cbad436 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,3 +1,4 @@
+open API
 open Printer
 open CErrors
 open Util
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 61752aa339..069f767dd6 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,3 +1,4 @@
+open API
 open Names
 
 val prove_princ_for_struct :
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index b8070ff885..fd4b52b65c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,3 +1,4 @@
+open API
 open Printer
 open CErrors
 open Util
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 45ad332fc5..bf1906bfb0 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Term
 open Misctypes
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index d28e0aba0a..d9cd026d8a 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 (*i camlp4deps: "grammar/grammar.cma" i*)
+open API
+open Grammar_API
 open Ltac_plugin
 open Util
 open Pp
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 785633e256..0e2ca49000 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1,3 +1,4 @@
+open API
 open Printer
 open Pp
 open Names
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 0cab5a6d35..7ad7de0792 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -1,3 +1,4 @@
+open API
 open Names
 
 (*
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 6fd496f508..eae72d9e84 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,3 +1,4 @@
+open API
 open Pp
 open Glob_term
 open CErrors
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 99a258de98..b6d2c45437 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,3 +1,4 @@
+open API
 open Names
 open Glob_term
 open Misctypes
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index f1a9758e80..f277c563a1 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,3 +1,4 @@
+open API
 open CErrors
 open Util
 open Names
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index ba89fe4a78..a82a8b3605 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,3 +1,4 @@
+open API
 open Misctypes
 
 val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a734255435..8f62231aeb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,3 +1,4 @@
+open API
 open Names
 open Pp
 open Libnames
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 5ef8f05bb7..aa42b2ab9b 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -1,3 +1,4 @@
+open API
 open Names
 open Pp
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index bcfa6b9316..8152e181a3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Ltac_plugin
 open Declarations
 open CErrors
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 7634437171..290d0bb918 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -8,6 +8,7 @@
 
 (* Merging of induction principles. *)
 
+open API
 open Globnames
 open Tactics
 open Indfun_common
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ff397d2e92..bd74d2cf64 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 module CVars = Vars
 
 open Term
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 80f02e01c4..e1a072799e 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,4 +1,4 @@
-
+open API
 
 (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
 val tclUSER_if_not_mes :