Put all plugins behind an "API".

13 files changed, 15 insertions, 0 deletions

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