Put all plugins behind an "API".

18 files changed, 20 insertions, 1 deletions

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