17 files changed, 19 insertions, 1 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index fd4962398..023cbad43 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 61752aa33..069f767dd 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 b8070ff88..fd4b52b65 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 45ad332fc..bf1906bfb 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 d28e0aba0..d9cd026d8 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 785633e25..0e2ca4900 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 0cab5a6d3..7ad7de079 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 6fd496f50..eae72d9e8 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 99a258de9..b6d2c4543 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 f1a9758e8..f277c563a 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 ba89fe4a7..a82a8b360 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 a73425543..8f62231ae 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 5ef8f05bb..aa42b2ab9 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 bcfa6b931..8152e181a 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 763443717..290d0bb91 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 ff397d2e9..bd74d2cf6 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 80f02e01c..e1a072799 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 :