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

160 files changed, 14 insertions, 160 deletions

diff --git a/Makefile.build b/Makefile.build
index 05d751f54..c00e96ea1 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -112,7 +112,7 @@ TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 COQOPTS=$(COQ_XML) $(NATIVECOMPUTE)
 BOOTCOQC=$(TIMER) $(COQTOPBEST) -boot $(COQOPTS) -compile
 
-LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS)))
+LOCALINCLUDES=$(if $(filter plugins/%,$<),-I lib -I API -open API $(addprefix -I plugins/,$(PLUGINDIRS)),$(addprefix -I ,$(SRCDIRS)))
 MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB)
 
 OCAMLC := $(OCAMLFIND) ocamlc $(CAMLFLAGS)
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt
index c3c86ac5c..57c7a97d5 100644
--- a/dev/doc/changes.txt
+++ b/dev/doc/changes.txt
@@ -28,6 +28,16 @@ Coq is compiled with -safe-string enabled and requires plugins to do
 the same. This means that code using `String` in an imperative way
 will fail to compile now. They should switch to `Bytes.t`
 
+* Plugin API *
+
+Coq 8.7 offers a new module overlay containing a proposed plugin API
+in `API/API.ml`; this overlay is enabled by adding the `-open API`
+flag to the OCaml compiler; this happens automatically for
+developments in the `plugin` folder and `coq_makefile`.
+
+However, `coq_makefile` can be instructed not to enable this flag by
+passing `-bypass-API`.
+
 * ML API *
 
 Added two functions for declaring hooks to be executed in reduction
diff --git a/plugins/.merlin b/plugins/.merlin
new file mode 100644
index 000000000..dd6678ba0
--- /dev/null
+++ b/plugins/.merlin
@@ -0,0 +1,2 @@
+REC
+FLG -open API
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 00e80d041..6281b2675 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -1,5 +1,3 @@
-open API
-
 let contrib_name = "btauto"
 
 let init_constant dir s =
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 3e4febf47..182821322 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -10,7 +10,6 @@
 (* Downey,Sethi and Tarjan. *)
 (* Plus some e-matching and constructor handling by P. Corbineau *)
 
-open API
 open CErrors
 open Util
 open Pp
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 1441e13fb..e6abf1ccf 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Util
 open Term
 open Names
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 4c9ebcfc4..a43a167e8 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -9,7 +9,6 @@
 (* This file uses the (non-compressed) union-find structure to generate *)
 (* proof-trees that will be transformed into proof-terms in cctac.ml4   *)
 
-open API
 open CErrors
 open Term
 open Ccalgo
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 0488a5db7..9f53123db 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Ccalgo
 open Term
 
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 4c5d85a5f..4934b0750 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -8,7 +8,6 @@
 
 (* This file is the interface between the c-c algorithm and Coq *)
 
-open API
 open Evd
 open Names
 open Inductiveops
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index ef32d2b83..b4bb62be8 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -7,7 +7,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open EConstr
 
 val proof_tac: Ccproof.proof -> unit Proofview.tactic
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index add3f90b1..6ed4672ce 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Ltac_plugin
 open Cctac
 open Stdarg
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 19d23c0e4..1524079f4 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Context.Named.Declaration
 
 let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index 7ea64a528..690a7c508 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
-
 (** [start_deriving f suchthat lemma] starts a proof of [suchthat]
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4
index ce9129bcf..df701ed80 100644
--- a/plugins/derive/g_derive.ml4
+++ b/plugins/derive/g_derive.ml4
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Stdarg
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
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
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 4319fa71c..db1a46a03 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -6,7 +6,6 @@
 (*         *       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 535d75735..106c469c6 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -6,7 +6,6 @@
 (*         *       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 81d714aa2..c001ee382 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
-open API
 open Grammar_API
 open Ltac_plugin
 open Formula
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index bd420546f..f660ba734 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -6,7 +6,6 @@
 (*         *       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 e15af1f23..d763fe635 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -6,7 +6,6 @@
 (*         *       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 4c8b96be1..169073630 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -6,7 +6,6 @@
 (*         *       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 c2eb1d68c..ec2a056e3 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -6,7 +6,6 @@
 (*         *       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 b0fcd98cc..d6309b057 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -6,7 +6,6 @@
 (*         *       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 05f60eccc..d8d4c1a38 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -6,7 +6,6 @@
 (*         *       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 6fddaafa3..5ba98fb58 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open EConstr
 open CErrors
 open Util
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 2488ffded..0a2e84bb8 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -6,7 +6,6 @@
 (*         *       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 2da3dc768..a1409edd0 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -6,7 +6,6 @@
 (*         *       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 cf2ef8ba6..d3e8aeee8 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Term
 open EConstr
 
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index a6299c3c4..68af1b3b6 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -12,7 +12,6 @@
 des inéquations et équations sont entiers. En attendant la tactique Field.
 *)
 
-open API
 open Term
 open Tactics
 open Names
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index dc43ea7c4..8cd47f7de 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,4 +1,3 @@
-open API
 open Printer
 open CErrors
 open Util
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index d03fc475e..64fbfaeed 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,4 +1,3 @@
-open API
 open Names
 
 val prove_princ_for_struct :
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d726c1a2b..513fce248 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,4 +1,3 @@
-open API
 open Printer
 open CErrors
 open Util
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index d6ad7ef0d..5a7ffe059 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Names
 open Term
 open Misctypes
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 56048f92e..c495703ee 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 (*i camlp4deps: "grammar/grammar.cma" i*)
-open API
 open Grammar_API
 open Ltac_plugin
 open Util
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index db2af2be5..379c83b24 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1,4 +1,3 @@
-open API
 open Printer
 open Pp
 open Names
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 7ad7de079..0cab5a6d3 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -1,4 +1,3 @@
-open API
 open Names
 
 (*
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 726a8203d..7cb35838c 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,4 +1,3 @@
-open API
 open Pp
 open Glob_term
 open CErrors
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index b6d2c4543..99a258de9 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,4 +1,3 @@
-open API
 open Names
 open Glob_term
 open Misctypes
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ff7667e99..863c9dc8d 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,4 +1,3 @@
-open API
 open CErrors
 open Util
 open Names
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index fc7da6a33..7a60da44f 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,4 +1,3 @@
-open API
 open Misctypes
 
 val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 61fbca23f..f4f9ba2bb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,4 +1,3 @@
-open API
 open Names
 open Pp
 open Libnames
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index f7a9cedd7..5e425cd18 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -1,4 +1,3 @@
-open API
 open Names
 open Pp
 
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e6f10a880..8dea6c90f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Ltac_plugin
 open Declarations
 open CErrors
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 63662a443..52a82b0e5 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -8,7 +8,6 @@
 
 (* Merging of induction principles. *)
 
-open API
 open Globnames
 open Tactics
 open Indfun_common
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index bc550c8b9..d3eccb58d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 
 module CVars = Vars
 
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index f3d5e7332..63bbdbe7e 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,4 +1,3 @@
-open API
 
 (* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
 val tclUSER_if_not_mes : 
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 47fd324f9..2769802cf 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 4342f5b5e..4cab6ef33 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 0658008c0..122aecd75 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 af1d349db..72c6f9090 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 e5a2d003a..419c5e8c4 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 e56b510be..6d80ab549 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 fe90f633f..c423585e5 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 6145e373b..4d13d89a4 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 946b99f6c..dd24aa3db 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 a7c05664f..549436902 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 cf6bd98b3..c93e873ee 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 a2e8fc270..1935d560a 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 8956e21b9..3c27b2747 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 49af905d8..e539b5867 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 898c1d1c3..2adcf02e6 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 782d13a38..794cb527f 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 8d8e82c7c..327b347ec 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 c15225ebf..1127c9831 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 e25f1926d..32494a879 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 eb4146cfc..52827cb36 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 9f171cee6..2b1106ee2 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 3a77f34a1..bbd7834d5 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 73e309cc2..35205ac58 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 610a722fb..1bf9ea4c1 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 4c3687ec7..6c4f3dd87 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 bdfa6d989..9e3a54cc8 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 ab46455c8..1a67f6f88 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 c6b4feba1..791b7f48d 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 9980e0961..ccd44b914 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 58d1766ff..13b44f0e2 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 23e12bfc0..958109e5a 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 471320684..64da097de 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 c3e39ec11..df03c7b47 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 4749017e1..ad2e70908 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 bad3e774d..7b054947b 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 ab94e21f0..73e4f3d6a 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 750843c9d..c1ca85433 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 c401e67f1..5ac377567 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 9113b620f..5394b1e11 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 469c6bdbc..ef6362270 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 3e9668072..63b8cc482 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 304eec463..01334d36c 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 5b95e9c77..fdeab8dc4 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 dc3bbf7d6..dd91944d4 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 e809d87dc..01d3f79c7 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
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index a662f8bad..a4103634e 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -16,7 +16,6 @@
 (*                                                                      *)
 (************************************************************************)
 
-open API
 open Pp
 open Mutils
 open Goptions
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 37a21cd59..b15dd7ae6 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,7 +16,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Ltac_plugin
 open Stdarg
 open Tacarg
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 261f3dab4..01c3d7940 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Ltac_plugin
 
 DECLARE PLUGIN "nsatz_plugin"
diff --git a/plugins/nsatz/nsatz.ml b/plugins/nsatz/nsatz.ml
index 7e63b916d..72934a15d 100644
--- a/plugins/nsatz/nsatz.ml
+++ b/plugins/nsatz/nsatz.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open CErrors
 open Util
 open Term
diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli
index b692522f2..d6e3071aa 100644
--- a/plugins/nsatz/nsatz.mli
+++ b/plugins/nsatz/nsatz.mli
@@ -6,5 +6,4 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 val nsatz_compute : Term.constr -> unit Proofview.tactic
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 3badb92f5..d07b2e0b4 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -13,7 +13,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open API
 open CErrors
 open Util
 open Names
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 8d24027d8..735af6bab 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -15,7 +15,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 
 DECLARE PLUGIN "omega_plugin"
 
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 88076dca9..f7ebd3204 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Ltac_plugin
 open Names
 open Misctypes
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 8ee5ce8b1..e1e73b1c3 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -101,7 +101,6 @@
 
 
 (*i*)
-open API
 open CErrors
 open Util
 open Names
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 06c80a825..4ffbd5aa8 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -6,7 +6,6 @@
 
  *************************************************************************)
 
-open API
 open Names
 
 let module_refl_name = "ReflOmegaCore"
diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli
index 6dc5d9f7e..a452b1a91 100644
--- a/plugins/romega/const_omega.mli
+++ b/plugins/romega/const_omega.mli
@@ -6,7 +6,6 @@
 
  *************************************************************************)
 
-open API
 
 (** Coq objects used in romega *)
 
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 53f6f42c8..5fd9c9419 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 
 DECLARE PLUGIN "romega_plugin"
 
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 60e6e7de7..517df41d9 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -6,7 +6,6 @@
 
  *************************************************************************)
 
-open API
 open Pp
 open Util
 open Const_omega
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 69a2043f6..bfa1e5f39 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 1158817d6..43a4107ad 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open CErrors
 open Util
 open Goptions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 944e0ac5e..9f02388c3 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 
 module Search = Explore.Make(Proof_search)
 
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index 080dcdac2..bec18f6df 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 (* raises Not_found if no proof is found *)
 
-open API
 
 type atom_env=
     {mutable next:int;
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index ada41274f..6c82346bc 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -8,7 +8,6 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
-open API
 open Grammar_API
 open Ltac_plugin
 open Pp
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 955cc767c..0f996c65a 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Ltac_plugin
 open Pp
 open Util
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index 7f685063c..d9d32c681 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Names
 open EConstr
 open Libnames
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
index b7afd2eff..d37582bd7 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Term
 open Libnames
 open Constrexpr
diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli
index 94eaa1d6a..cdd4ee645 100644
--- a/plugins/ssr/ssrast.mli
+++ b/plugins/ssr/ssrast.mli
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Names
 open Ltac_plugin
 
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index 3988f00ba..cc0e86684 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Printer
 open Pretyping
 open Globnames
diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli
index 20a1263d2..af9f7491a 100644
--- a/plugins/ssr/ssrbwd.mli
+++ b/plugins/ssr/ssrbwd.mli
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 
 val apply_top_tac : Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 411ce6853..608b778e4 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Grammar_API
 open Util
 open Names
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index f61168576..4b045e989 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Tacmach
 open Names
 open Environ
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index bd9a05891..832044909 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Util
 open Names
 open Printer
diff --git a/plugins/ssr/ssrelim.mli b/plugins/ssr/ssrelim.mli
index 825b4758e..66e202b48 100644
--- a/plugins/ssr/ssrelim.mli
+++ b/plugins/ssr/ssrelim.mli
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Ssrmatching_plugin
 
 val ssrelim :
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index b0fe89897..ab6a60f4e 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Ltac_plugin
 open Util
 open Names
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index f9ab5d74f..a3366887f 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Ssrmatching_plugin
 open Ssrast
 
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 660c2e776..8e6329a15 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Names
 open Tacmach
 
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 7f254074c..e5b5b58ff 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Names
 
 open Ltac_plugin
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 06bbd749e..023778fdb 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Names
 open Pp
 open Term
diff --git a/plugins/ssr/ssripats.mli b/plugins/ssr/ssripats.mli
index aefdc8e11..6c36e67e8 100644
--- a/plugins/ssr/ssripats.mli
+++ b/plugins/ssr/ssripats.mli
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Ssrmatching_plugin
 open Ssrast
 open Ssrcommon
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 09917339a..228444b82 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Grammar_API
 open Names
 open Pp
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 154820666..c93e10405 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Grammar_API
 
 val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
diff --git a/plugins/ssr/ssrprinters.ml b/plugins/ssr/ssrprinters.ml
index 427109c1b..e865ef706 100644
--- a/plugins/ssr/ssrprinters.ml
+++ b/plugins/ssr/ssrprinters.ml
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Pp
 open Names
 open Printer
diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli
index 8da9bc72b..5c68872b7 100644
--- a/plugins/ssr/ssrprinters.mli
+++ b/plugins/ssr/ssrprinters.mli
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Ssrast
 
 val pp_term :
diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml
index b586d05e1..5e43c8374 100644
--- a/plugins/ssr/ssrtacticals.ml
+++ b/plugins/ssr/ssrtacticals.ml
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Names
 open Termops
 open Tacmach
diff --git a/plugins/ssr/ssrtacticals.mli b/plugins/ssr/ssrtacticals.mli
index 297cfdfdc..c1f65a31e 100644
--- a/plugins/ssr/ssrtacticals.mli
+++ b/plugins/ssr/ssrtacticals.mli
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 
 val tclSEQAT :
   Ltac_plugin.Tacinterp.interp_sign ->
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index cb6a2cd69..fbe3cd2b9 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Grammar_API
 open Names
 open Term
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index cc142e091..338ecccc2 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Util
 open Names
 open Term
diff --git a/plugins/ssr/ssrview.mli b/plugins/ssr/ssrview.mli
index 8a7bd5d6e..6fd906ff4 100644
--- a/plugins/ssr/ssrview.mli
+++ b/plugins/ssr/ssrview.mli
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Ssrast
 open Ssrcommon
 
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 7674a8dde..74519f6c5 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -8,7 +8,6 @@
 
 (* This file is (C) Copyright 2006-2015 Microsoft Corporation and Inria. *)
 
-open API
 open Grammar_API
 
 (* Defining grammar rules with "xx" in it automatically declares keywords too,
diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli
index 1853bc35d..0c09d7bfb 100644
--- a/plugins/ssrmatching/ssrmatching.mli
+++ b/plugins/ssrmatching/ssrmatching.mli
@@ -1,7 +1,6 @@
 (* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 
-open API
 open Grammar_API
 open Goal
 open Genarg
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 6bf5b8cfc..c41ec39cb 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-open API
 
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "ascii_syntax_plugin"
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index fe1eef866..af64b1479 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "int31_syntax_plugin"
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index c6ee899ed..524a5c522 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 
 (* Poor's man DECLARE PLUGIN *)
 let __coq_plugin_name = "nat_syntax_plugin"
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 9cfa50071..06117de79 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Util
 open Names
 open Globnames
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index a4335a508..b7f13b040 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-open API
 open Globnames
 open Ascii_syntax_plugin.Ascii_syntax
 open Glob_term
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 719d8b1cc..af3df2889 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open API
 open Pp
 open CErrors
 open Util
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 43f7670a6..c3aedf538 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -197,7 +197,7 @@ let generate_conf_coq_config oc args bypass_API =
   section oc "Coq configuration.";
   let src_dirs = if bypass_API
                  then Coq_config.all_src_dirs
-                 else Coq_config.api_dirs @ Coq_config.plugins_dirs in
+                 else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in
   Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs;
   fprintf oc "COQMF_MAKEFILE=%s\n" (quote (List.hd args)); 
 ;;