Put all plugins behind an "API".

134 files changed, 175 insertions, 4 deletions

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 6281b2675e..00e80d041f 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -1,3 +1,5 @@
+open API
+
 let contrib_name = "btauto"
 
 let init_constant dir s =
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index ba398c3858..e8589f2ceb 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -10,6 +10,7 @@
 (* Downey,Sethi and Tarjan. *)
 (* Plus some e-matching and constructor handling by P. Corbineau *)
 
+open API
 open CErrors
 open Util
 open Pp
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index c7fa2f56fd..871de72539 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Util
 open Term
 open Names
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 642ceba3db..eecb7bc983 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -9,6 +9,7 @@
 (* This file uses the (non-compressed) union-find structure to generate *)
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
+open API
 open CErrors
 open Term
 open Ccalgo
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index eacbfeac70..4e4d42f869 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Ccalgo
 open Term
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index b638f23606..e8b2d7615d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -8,6 +8,7 @@
 
 (* This file is the interface between the c-c algorithm and Coq *)
 
+open API
 open Evd
 open Names
 open Inductiveops
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index b4bb62be8e..ef32d2b83e 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -7,6 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open EConstr
 
 val proof_tac: Ccproof.proof -> unit Proofview.tactic
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 7e76854b16..43b150c346 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
 open Ltac_plugin
 open Cctac
 open Stdarg
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index b3ab29cced..31cbc8e25f 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Context.Named.Declaration
 
 let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index 9ea876f131..3a7e7b837d 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 (** [start_deriving f suchthat lemma] starts a proof of [suchthat]
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index deadb3b4d5..445923e01b 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Stdarg
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index c498eb5890..9c3f97696f 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Pp
 open Util
 open Names
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index b8e95afb38..4c9b1e1a5a 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Globnames
 open Miniml
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2c85b185c4..688bcd025c 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Miniml
 open Term
 open Declarations
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 90f4f911b7..1e7a6ba5bd 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -8,6 +8,7 @@
 
 (*s This module declares the extraction commands. *)
 
+open API
 open Names
 open Libnames
 open Globnames
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 92ece7ccf9..f1a50e7eba 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open API
 open Util
 open Names
 open Term
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index cdda777a6c..2b4b05a957 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -8,6 +8,7 @@
 
 (*s Extraction from Coq terms to Miniml. *)
 
+open API
 open Names
 open Term
 open Declarations
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 3ed959cf2c..6cba83ef91 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -8,6 +8,9 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+open Grammar_API.Pcoq.Prim
+
 DECLARE PLUGIN "extraction_plugin"
 
 (* ML names *)
@@ -15,7 +18,6 @@ DECLARE PLUGIN "extraction_plugin"
 open Ltac_plugin
 open Genarg
 open Stdarg
-open Pcoq.Prim
 open Pp
 open Names
 open Nameops
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index eb13fd6755..8cdfb34992 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -8,6 +8,7 @@
 
 (*s Production of Haskell syntax. *)
 
+open API
 open Pp
 open CErrors
 open Util
diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml
index e43c47d050..1bf19f186b 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -1,3 +1,4 @@
+open API
 open Pp
 open Util
 open Names
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index db33615228..28226f225f 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -8,6 +8,7 @@
 
 (*s Target language for extraction: a core ML called MiniML. *)
 
+open API
 open Pp
 open Names
 open Globnames
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 402fe4ffe6..5a50899c66 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 (*i*)
+open API
 open Util
 open Names
 open Libnames
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index c667552490..2655dfc897 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Globnames
 open Miniml
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index b67b9931ec..2b1e810604 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Globnames
 open CErrors
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index dc8708249a..45e890be0f 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Globnames
 open Miniml
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 4399fc561f..83abaf508e 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -8,6 +8,7 @@
 
 (*s Production of Ocaml syntax. *)
 
+open API
 open Pp
 open CErrors
 open Util
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 3c81564e34..55168cc297 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -8,6 +8,7 @@
 
 (*s Production of Scheme syntax. *)
 
+open API
 open Pp
 open CErrors
 open Util
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 29dd8ff4f4..607ca1b3a9 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Term
 open Declarations
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 15a08756c0..cd1667bdb0 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Libnames
 open Globnames
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 9900792cac..314a2b2f96 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Hipattern
 open Names
 open Term
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 3f438c04a0..a31de5e61f 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Term
 open EConstr
 open Globnames
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index e3fab6d012..139baaeb31 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open API
+open Grammar_API
 open Ltac_plugin
 open Formula
 open Sequent
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 0fa3089e73..a5a81bb166 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Ltac_plugin
 open Formula
 open Sequent
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index 4fd1e38a27..aaf79ae885 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 val ground_tac: unit Proofview.tactic ->
   ((Sequent.t -> unit Proofview.tactic) -> unit Proofview.tactic) -> unit Proofview.tactic
 
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index e1d765a420..92372fe291 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Unify
 open Rules
 open CErrors
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 47550f314e..b0e4b2690b 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Globnames
 open Rules
 
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index b7fe25a32a..72ede1f7dd 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open CErrors
 open Util
 open Names
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index fb21730830..682047075b 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Term
 open EConstr
 open Names
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 826afc35b6..4a93e01dca 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Term
 open EConstr
 open CErrors
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 6ed251f34e..c43a91ceed 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open EConstr
 open Formula
 open Globnames
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 49bf07155f..24fd8dd88f 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Util
 open Term
 open EConstr
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index c9cca9bd8d..7f1fb9bd01 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Term
 open EConstr
 
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 317444cf16..2af79aec9b 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -12,6 +12,7 @@
 des inéquations et équations sont entiers. En attendant la tactique Field.
 *)
 
+open API
 open Term
 open Tactics
 open Names
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 : 
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index ea1660d901..63057c3aea 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
 open Util
 open Names
 open Locus
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 7db484d825..958f43bd79 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Util
 open Names
 open Term
diff --git a/plugins/ltac/evar_tactics.mli b/plugins/ltac/evar_tactics.mli
index cfe7476658..7c734cd9af 100644
--- a/plugins/ltac/evar_tactics.mli
+++ b/plugins/ltac/evar_tactics.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Tacexpr
 open Locus
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index fdb8d34618..b26fd78ef2 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+open Grammar_API
 open Pp
 open Genarg
 open Stdarg
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 9b41675120..b2b3f8b6bb 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Tacexpr
 open Names
 open Constrexpr
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 8afe3053d0..9f53c44a47 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+open Grammar_API
 open Pp
 open Genarg
 open Stdarg
diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli
index 18334dafe7..c7ec269677 100644
--- a/plugins/ltac/extratactics.mli
+++ b/plugins/ltac/extratactics.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 val discrHyp : Names.Id.t -> unit Proofview.tactic
 val injHyp : Names.Id.t -> unit Proofview.tactic
 
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 2c2a4b8509..68b63f02c3 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+open Grammar_API
 open Pp
 open Genarg
 open Stdarg
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index dd5307638c..3d7d5e3fe2 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
 open Class_tactics
 open Stdarg
 open Tacarg
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index 679aa11272..e91e251112 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -14,6 +14,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
 open Eqdecide
 open Names
 
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 36ac10bfe7..7855fbcfc9 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -8,6 +8,9 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+open Grammar_API
+
 DECLARE PLUGIN "ltac_plugin"
 
 open Util
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 4dceb03314..18e62a2111 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -12,7 +12,8 @@
   Syntax for the subtac terms and types.
   Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *)
 
-
+open API
+open Grammar_API
 open Libnames
 open Constrexpr
 open Constrexpr_ops
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 25258ffa90..e6ddc5cc1b 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -10,6 +10,8 @@
 
 (* Syntax for rewriting with strategies *)
 
+open API
+open Grammar_API
 open Names
 open Misctypes
 open Locus
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 83bfd0233a..e94cf1c637 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Pp
 open CErrors
 open Util
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 7e979d269d..84c5d3a44f 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Pcoq
 
 (* Main entry for extensions *)
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 810e1ec39a..9261a11c71 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -8,6 +8,8 @@
 
 (** Ltac parsing entries *)
 
+open API
+open Grammar_API
 open Loc
 open Names
 open Pcoq
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 9446f9df4d..c84a7c00a7 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Pp
 open Names
 open Namegen
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 4265c416b6..519283759a 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -9,6 +9,7 @@
 (** This module implements pretty-printers for tactic_expr syntactic
     objects and their subcomponents. *)
 
+open API
 open Pp
 open Genarg
 open Geninterp
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index b237e917d5..0fbb9df2db 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Unicode
 open Pp
 open Printer
diff --git a/plugins/ltac/profile_ltac.mli b/plugins/ltac/profile_ltac.mli
index e5e2e41975..09fc549c60 100644
--- a/plugins/ltac/profile_ltac.mli
+++ b/plugins/ltac/profile_ltac.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 (** Ltac profiling primitives *)
 
 val do_profile :
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index 8cb76d81c5..83fb6963b8 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
@@ -10,6 +10,7 @@
 
 (** Ltac profiling entrypoints *)
 
+open API
 open Profile_ltac
 open Stdarg
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 68dc1fd376..9069635c12 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Pp
 open CErrors
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 6683d753bc..77286452bf 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Constr
 open Environ
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 42552c4846..2c9bf14be2 100644
--- a/plugins/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
@@ -8,6 +8,7 @@
 
 (** Generic arguments based on Ltac. *)
 
+open API
 open Genarg
 open Geninterp
 open Tacexpr
diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli
index bfa423db20..e82cb516c0 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Genarg
 open Tacexpr
 open Constrexpr
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index e037bb4b26..14e5aa72af 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Util
 open Names
 open Term
diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli
index 9883c03c46..2c02171d0d 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Util
 open Names
 open EConstr
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index f44ccbd3b5..dbc32c2f6c 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Pp
 open CErrors
 open Util
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 07aa7ad82e..c5223052cc 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -8,6 +8,8 @@
 
 (** Ltac toplevel command entries. *)
 
+open API
+open Grammar_API
 open Vernacexpr
 open Tacexpr
 
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index efb7e780db..14b5e00c72 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Util
 open Pp
 open Names
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index d1e2a7bbe6..2295852ce3 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Tacexpr
 open Geninterp
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index cfb698cd87..9b6ac8a9ae 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Loc
 open Names
 open Constrexpr
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index d201cf9490..bc1dd26d92 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Pattern
 open Pp
 open Genredexpr
@@ -14,7 +16,6 @@ open Tacred
 open CErrors
 open Util
 open Names
-open Nameops
 open Libnames
 open Globnames
 open Nametab
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 8ad52ca023..1841ab42bf 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Pp
 open Names
 open Tacexpr
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ff76d06cf3..85d3944b18 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Constrintern
 open Patternops
 open Pp
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index fb50a64346..a1841afe36 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Tactic_debug
 open EConstr
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 2858df3130..6d33724f1a 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Util
 open Tacexpr
 open Mod_subst
diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli
index c1bf272579..2cfe8fac94 100644
--- a/plugins/ltac/tacsubst.mli
+++ b/plugins/ltac/tacsubst.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Tacexpr
 open Mod_subst
 open Genarg
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index e6d0370f36..8126421c7d 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Util
 open Names
 open Pp
diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli
index ac35464c45..6cfaed3053 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Environ
 open Pattern
 open Names
diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml
index 5b5cd06cc7..6dcef414c2 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -9,6 +9,7 @@
 (** This file extends Matching with the main logic for Ltac's
     (lazy)match and (lazy)match goal. *)
 
+open API
 open Names
 open Tacexpr
 open Context.Named.Declaration
diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli
index 300b546f11..304eec463e 100644
--- a/plugins/ltac/tactic_matching.mli
+++ b/plugins/ltac/tactic_matching.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 (** This file extends Matching with the main logic for Ltac's
     (lazy)match and (lazy)match goal. *)
 
diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml
index a5ba3b8371..53dfe22a9c 100644
--- a/plugins/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Libobject
 open Pp
 
diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli
index ed759a76db..2817b54a11 100644
--- a/plugins/ltac/tactic_option.mli
+++ b/plugins/ltac/tactic_option.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Tacexpr
 open Vernacexpr
 
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index d8e21d81d1..13492ed51c 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Term
 open EConstr
 open Hipattern
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 83f374346e..03041ea0ab 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -16,6 +16,7 @@
 (*                                                                      *)
 (************************************************************************)
 
+open API
 open Pp
 open Mutils
 open Goptions
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index ccb6daa116..d803c75549 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,6 +16,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
 open Ltac_plugin
 open Stdarg
 open Tacarg
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 7598852531..589c13907c 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
 open Ltac_plugin
 open Names
 
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 6ba4c0f930..dd1d8764ab 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open CErrors
 open Util
 open Term
diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli
index e876ccfa5d..d6eb1b406e 100644
--- a/plugins/nsatz/nsatz.mli
+++ b/plugins/nsatz/nsatz.mli
@@ -6,4 +6,5 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 val nsatz_compute : Constr.t -> unit Proofview.tactic
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 465e770199..94e3f508ff 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -13,6 +13,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open API
 open CErrors
 open Util
 open Names
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index ce7ffb1e7e..8cea98783a 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -15,6 +15,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+
 DECLARE PLUGIN "omega_plugin"
 
 open Ltac_plugin
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 980f03db33..c43d7d0b5b 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
 open Ltac_plugin
 open Names
 open Misctypes
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index ffacd8b361..a81b8944c9 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -101,6 +101,7 @@
 
 
 (*i*)
+open API
 open CErrors
 open Util
 open Names
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index d97dea0397..4db4bdc2ca 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -6,6 +6,8 @@
 
  *************************************************************************)
 
+open API
+
 let module_refl_name = "ReflOmegaCore"
 let module_refl_path = ["Coq"; "romega"; module_refl_name]
 
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index a452b1a917..6dc5d9f7e5 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -6,6 +6,7 @@
 
  *************************************************************************)
 
+open API
 
 (** Coq objects used in romega *)
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 6479c683b2..30d93654b1 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+
 DECLARE PLUGIN "romega_plugin"
 
 open Ltac_plugin
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 575634174f..1a53862ec4 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -6,6 +6,7 @@
 
  *************************************************************************)
 
+open API
 open Pp
 open Util
 open Const_omega
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 7e58ef9a3e..565308f72e 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
 open Ltac_plugin
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 153a6a49af..8dd7a5e469 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open CErrors
 open Util
 open Goptions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 1b07a8ca84..b9678fadf0 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 module Search = Explore.Make(Proof_search)
 
 open Ltac_plugin
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index 0925523641..c01e63505b 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -7,6 +7,8 @@
 (************************************************************************)
 (* raises Not_found if no proof is found *)
 
+open API
+
 type atom_env=
     {mutable next:int;
      mutable env:(Term.constr*int) list}
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 05ab8ab326..ada41274fa 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+open Grammar_API
 open Ltac_plugin
 open Pp
 open Util
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 85cbdc5a41..a107b59482 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Ltac_plugin
 open Pp
 open Util
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index d9d32c681d..7f685063c4 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open EConstr
 open Libnames
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
index c26fcc8d1f..46572acd0f 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Constr
 open Libnames
 open Constrexpr
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 67e6c7e939..051a9fb4e6 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -8,6 +8,9 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
+open API
+open Grammar_API
+
 (* Defining grammar rules with "xx" in it automatically declares keywords too,
  * we thus save the lexer to restore it at the end of the file *)
 let frozen_lexer = CLexer.get_keyword_state () ;;
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 8be989de57..088dd021ee 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -1,6 +1,8 @@
 (* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 
+open API
+open Grammar_API
 open Genarg
 open Tacexpr
 open Environ
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index e7eea02849..6bf5b8cfca 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+open API
+
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "ascii_syntax_plugin"
 let () = Mltop.add_known_module __coq_plugin_name
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 9a4cd6c254..a3d13c4077 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "nat_syntax_plugin"
 let () = Mltop.add_known_module __coq_plugin_name
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index e23852bf8f..f116e3a649 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "numbers_syntax_plugin"
 let () = Mltop.add_known_module __coq_plugin_name
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 7ce066c59d..a734681235 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Util
 open Names
 open Globnames
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index b7f13b0400..a4335a508b 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
+open API
 open Globnames
 open Ascii_syntax_plugin.Ascii_syntax
 open Glob_term
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 479448e06e..dfff8d9dfb 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Pp
 open CErrors
 open Util