[API] Remove `open API` in ml files in favor of `-open API` flag.

18 files changed, 0 insertions, 18 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 19ba31fbbd..9772ebd641 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -6,7 +6,6 @@
 (*         *       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 28a7c4d457..d6342b59c6 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -6,7 +6,6 @@
 (*         *       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 79d602dbe8..7d69cbff1f 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -6,7 +6,6 @@
 (*         *       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 0629a84a03..f289b63ad4 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -8,7 +8,6 @@
 
 (*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 d638c232bb..3661faadab 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 (*i*)
-open API
 open Util
 open Names
 open Term
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 5ee34103c5..e1d43f3405 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -8,7 +8,6 @@
 
 (*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 2fa453e533..4372ea557b 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Grammar_API.Pcoq.Prim
 
 DECLARE PLUGIN "extraction_plugin"
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 6146f32bbe..0f537abece 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -8,7 +8,6 @@
 
 (*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 1bf19f186b..e43c47d050 100644
--- a/plugins/extraction/json.ml
+++ b/plugins/extraction/json.ml
@@ -1,4 +1,3 @@
-open API
 open Pp
 open Util
 open Names
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index ea966baee6..be8282da06 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -8,7 +8,6 @@
 
 (*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 f8c846725e..f1bcde2f3f 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 (*i*)
-open API
 open Util
 open Names
 open Libnames
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 1db96413a8..42d22a7b45 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,7 +6,6 @@
 (*         *       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 365dc191ab..a896a8d037 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Names
 open ModPath
 open Globnames
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 1d9db3a5fc..ad60b58d5d 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -6,7 +6,6 @@
 (*         *       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 2ac411d06f..9cbc3fd713 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -8,7 +8,6 @@
 
 (*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 bb96489ab0..1ccc273704 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -8,7 +8,6 @@
 
 (*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 dff3548fd8..ca98f07e8d 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Names
 open ModPath
 open Term
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 0215aa8e48..2b3007f025 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Names
 open Libnames
 open Globnames