[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 19ba31fbb..9772ebd64 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 28a7c4d45..d6342b59c 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 79d602dbe..7d69cbff1 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 0629a84a0..f289b63ad 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 d638c232b..3661faada 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 5ee34103c..e1d43f340 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 2fa453e53..4372ea557 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 6146f32bb..0f537abec 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 1bf19f186..e43c47d05 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 ea966baee..be8282da0 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 f8c846725..f1bcde2f3 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 1db96413a..42d22a7b4 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 365dc191a..a896a8d03 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 1d9db3a5f..ad60b58d5 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 2ac411d06..9cbc3fd71 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 bb96489ab..1ccc27370 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 dff3548fd..ca98f07e8 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 0215aa8e4..2b3007f02 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