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 6281b2675..00e80d041 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 ba398c385..e8589f2ce 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 c7fa2f56f..871de7253 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 642ceba3d..eecb7bc98 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 eacbfeac7..4e4d42f86 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 b638f2360..e8b2d7615 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 b4bb62be8..ef32d2b83 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 7e76854b1..43b150c34 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 b3ab29cce..31cbc8e25 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 9ea876f13..3a7e7b837 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 deadb3b4d..445923e01 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 c498eb589..9c3f97696 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 b8e95afb3..4c9b1e1a5 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 2c85b185c..688bcd025 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 90f4f911b..1e7a6ba5b 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 92ece7ccf..f1a50e7eb 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 cdda777a6..2b4b05a95 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 3ed959cf2..6cba83ef9 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 eb13fd675..8cdfb3499 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 e43c47d05..1bf19f186 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 db3361522..28226f225 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 402fe4ffe..5a50899c6 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 c66755249..2655dfc89 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 b67b9931e..2b1e81060 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 dc8708249..45e890be0 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 4399fc561..83abaf508 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 3c81564e3..55168cc29 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 29dd8ff4f..607ca1b3a 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 15a08756c..cd1667bdb 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 9900792ca..314a2b2f9 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 3f438c04a..a31de5e61 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 e3fab6d01..139baaeb3 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 0fa3089e7..a5a81bb16 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 4fd1e38a2..aaf79ae88 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 e1d765a42..92372fe29 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 47550f314..b0e4b2690 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 b7fe25a32..72ede1f7d 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 fb2173083..682047075 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 826afc35b..4a93e01dc 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 6ed251f34..c43a91cee 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 49bf07155..24fd8dd88 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 c9cca9bd8..7f1fb9bd0 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 317444cf1..2af79aec9 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 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 : 
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index ea1660d90..63057c3ae 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 7db484d82..958f43bd7 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 cfe747665..7c734cd9a 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 fdb8d3461..b26fd78ef 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 9b4167512..b2b3f8b6b 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 8afe3053d..9f53c44a4 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 18334dafe..c7ec26967 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 2c2a4b850..68b63f02c 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 dd5307638..3d7d5e3fe 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 679aa1127..e91e25111 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 36ac10bfe..7855fbcfc 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 4dceb0331..18e62a211 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 25258ffa9..e6ddc5cc1 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 83bfd0233..e94cf1c63 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 7e979d269..84c5d3a44 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 810e1ec39..9261a11c7 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 9446f9df4..c84a7c00a 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 4265c416b..519283759 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 b237e917d..0fbb9df2d 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 e5e2e4197..09fc549c6 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 8cb76d81c..83fb6963b 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 68dc1fd37..9069635c1 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 6683d753b..77286452b 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 42552c484..2c9bf14be 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 bfa423db2..e82cb516c 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 e037bb4b2..14e5aa72a 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 9883c03c4..2c02171d0 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 f44ccbd3b..dbc32c2f6 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 07aa7ad82..c5223052c 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 efb7e780d..14b5e00c7 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 d1e2a7bbe..2295852ce 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 cfb698cd8..9b6ac8a9a 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 d201cf949..bc1dd26d9 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 8ad52ca02..1841ab42b 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 ff76d06cf..85d3944b1 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 fb50a6434..a1841afe3 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 2858df313..6d33724f1 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 c1bf27257..2cfe8fac9 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 e6d0370f3..8126421c7 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 ac35464c4..6cfaed305 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 5b5cd06cc..6dcef414c 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 300b546f1..304eec463 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 a5ba3b837..53dfe22a9 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 ed759a76d..2817b54a1 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 d8e21d81d..13492ed51 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 83f374346..03041ea0a 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 ccb6daa11..d803c7554 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 759885253..589c13907 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 6ba4c0f93..dd1d8764a 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 e876ccfa5..d6eb1b406 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 465e77019..94e3f508f 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 ce7ffb1e7..8cea98783 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 980f03db3..c43d7d0b5 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 ffacd8b36..a81b8944c 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 d97dea039..4db4bdc2c 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 a452b1a91..6dc5d9f7e 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 6479c683b..30d93654b 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 575634174..1a53862ec 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 7e58ef9a3..565308f72 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 153a6a49a..8dd7a5e46 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 1b07a8ca8..b9678fadf 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 092552364..c01e63505 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 05ab8ab32..ada41274f 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 85cbdc5a4..a107b5948 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 d9d32c681..7f685063c 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 c26fcc8d1..46572acd0 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 67e6c7e93..051a9fb4e 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 8be989de5..088dd021e 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 e7eea0284..6bf5b8cfc 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 9a4cd6c25..a3d13c407 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 e23852bf8..f116e3a64 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 7ce066c59..a73468123 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 b7f13b040..a4335a508 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 479448e06..dfff8d9df 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