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

45 files changed, 0 insertions, 45 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 47fd324f97..2769802cf4 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Util
 open Locus
 open Misctypes
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 4342f5b5e1..4cab6ef336 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -6,7 +6,6 @@
 (*         *       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 0658008c00..122aecd75b 100644
--- a/plugins/ltac/evar_tactics.mli
+++ b/plugins/ltac/evar_tactics.mli
@@ -6,7 +6,6 @@
 (*         *       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 af1d349db2..72c6f90900 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Grammar_API
 open Pp
 open Genarg
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index e5a2d003a5..419c5e8c45 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Grammar_API
 open Tacexpr
 open Names
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index e56b510be0..6d80ab5494 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Grammar_API
 open Pp
 open Genarg
diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli
index fe90f633f2..c423585e5e 100644
--- a/plugins/ltac/extratactics.mli
+++ b/plugins/ltac/extratactics.mli
@@ -6,7 +6,6 @@
 (*         *       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 6145e373b1..4d13d89a49 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Grammar_API
 open Pp
 open Genarg
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 946b99f6c0..dd24aa3dbf 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -8,7 +8,6 @@
 
 (*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 a7c05664f5..5494369022 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -14,7 +14,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Eqdecide
 
 DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index cf6bd98b38..c93e873ee3 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Grammar_API
 
 DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index a2e8fc270d..1935d560a4 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -12,7 +12,6 @@
   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
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 8956e21b93..3c27b27475 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -10,7 +10,6 @@
 
 (* Syntax for rewriting with strategies *)
 
-open API
 open Grammar_API
 open Names
 open Misctypes
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 49af905d89..e539b58674 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Grammar_API
 open Pp
 open CErrors
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 898c1d1c31..2adcf02e69 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Grammar_API
 open Pcoq
 
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 782d13a38d..794cb527f3 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -8,7 +8,6 @@
 
 (** Ltac parsing entries *)
 
-open API
 open Grammar_API
 open Loc
 open Names
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 8d8e82c7ce..327b347ec0 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -6,7 +6,6 @@
 (*         *       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 c15225ebfc..1127c98319 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -9,7 +9,6 @@
 (** 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 e25f1926d5..32494a8793 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -6,7 +6,6 @@
 (*         *       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 eb4146cfc1..52827cb36b 100644
--- a/plugins/ltac/profile_ltac.mli
+++ b/plugins/ltac/profile_ltac.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 
 (** Ltac profiling primitives *)
 
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index 9f171cee66..2b1106ee21 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
@@ -10,7 +10,6 @@
 
 (** Ltac profiling entrypoints *)
 
-open API
 open Profile_ltac
 open Stdarg
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3a77f34a1c..bbd7834d58 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -6,7 +6,6 @@
 (*         *       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 73e309cc21..35205ac58a 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Names
 open Environ
 open EConstr
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 610a722fb1..1bf9ea4c1d 100644
--- a/plugins/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
@@ -8,7 +8,6 @@
 
 (** 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 4c3687ec75..6c4f3dd873 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -6,7 +6,6 @@
 (*         *       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 bdfa6d9896..9e3a54cc86 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -6,7 +6,6 @@
 (*         *       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 ab46455c82..1a67f6f888 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -6,7 +6,6 @@
 (*         *       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 c6b4feba1c..791b7f48db 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Grammar_API
 open Pp
 open CErrors
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 9980e0961a..ccd44b914e 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -8,7 +8,6 @@
 
 (** 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 58d1766ff7..13b44f0e2c 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -6,7 +6,6 @@
 (*         *       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 23e12bfc0d..958109e5a7 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -6,7 +6,6 @@
 (*         *       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 471320684d..64da097deb 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -6,7 +6,6 @@
 (*         *       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 c3e39ec11a..df03c7b472 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Grammar_API
 open Pattern
 open Pp
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 4749017e16..ad2e709085 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Grammar_API
 open Pp
 open Names
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index bad3e774de..7b054947b7 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Grammar_API
 open Constrintern
 open Patternops
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index ab94e21f0a..73e4f3d6ab 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -6,7 +6,6 @@
 (*         *       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 750843c9d0..c1ca854334 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Grammar_API
 open Util
 open Tacexpr
diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli
index c401e67f11..5ac3775676 100644
--- a/plugins/ltac/tacsubst.mli
+++ b/plugins/ltac/tacsubst.mli
@@ -6,7 +6,6 @@
 (*         *       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 9113b620f0..5394b1e116 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -6,7 +6,6 @@
 (*         *       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 469c6bdbca..ef6362270a 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -6,7 +6,6 @@
 (*         *       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 3e96680729..63b8cc4824 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -9,7 +9,6 @@
 (** 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 304eec463e..01334d36c9 100644
--- a/plugins/ltac/tactic_matching.mli
+++ b/plugins/ltac/tactic_matching.mli
@@ -6,7 +6,6 @@
 (*         *       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 5b95e9c778..fdeab8dc4b 100644
--- a/plugins/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
@@ -6,7 +6,6 @@
 (*         *       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 dc3bbf7d69..dd91944d48 100644
--- a/plugins/ltac/tactic_option.mli
+++ b/plugins/ltac/tactic_option.mli
@@ -6,7 +6,6 @@
 (*         *       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 e809d87dc7..01d3f79c74 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Term
 open EConstr
 open Hipattern