Put all plugins behind an "API".

45 files changed, 65 insertions, 2 deletions

diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index ea1660d901..63057c3aea 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
 open Util
 open Names
 open Locus
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 7db484d825..958f43bd79 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -6,6 +6,7 @@
 (*         *       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 cfe7476658..7c734cd9af 100644
--- a/plugins/ltac/evar_tactics.mli
+++ b/plugins/ltac/evar_tactics.mli
@@ -6,6 +6,7 @@
 (*         *       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 fdb8d34618..b26fd78ef2 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+open Grammar_API
 open Pp
 open Genarg
 open Stdarg
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index 9b41675120..b2b3f8b6bb 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Tacexpr
 open Names
 open Constrexpr
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 8afe3053d0..9f53c44a47 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+open Grammar_API
 open Pp
 open Genarg
 open Stdarg
diff --git a/plugins/ltac/extratactics.mli b/plugins/ltac/extratactics.mli
index 18334dafe7..c7ec269677 100644
--- a/plugins/ltac/extratactics.mli
+++ b/plugins/ltac/extratactics.mli
@@ -6,6 +6,8 @@
 (*         *       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 2c2a4b8509..68b63f02c3 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+open Grammar_API
 open Pp
 open Genarg
 open Stdarg
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index dd5307638c..3d7d5e3fe2 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -8,6 +8,7 @@
 
 (*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 679aa11272..e91e251112 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -14,6 +14,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
 open Eqdecide
 open Names
 
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 36ac10bfe7..7855fbcfc9 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -8,6 +8,9 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open API
+open Grammar_API
+
 DECLARE PLUGIN "ltac_plugin"
 
 open Util
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index 4dceb03314..18e62a2111 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -12,7 +12,8 @@
   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
 open Constrexpr_ops
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 25258ffa90..e6ddc5cc1b 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -10,6 +10,8 @@
 
 (* Syntax for rewriting with strategies *)
 
+open API
+open Grammar_API
 open Names
 open Misctypes
 open Locus
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 83bfd0233a..e94cf1c637 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Pp
 open CErrors
 open Util
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 7e979d269d..84c5d3a44f 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Pcoq
 
 (* Main entry for extensions *)
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli
index 810e1ec39a..9261a11c71 100644
--- a/plugins/ltac/pltac.mli
+++ b/plugins/ltac/pltac.mli
@@ -8,6 +8,8 @@
 
 (** Ltac parsing entries *)
 
+open API
+open Grammar_API
 open Loc
 open Names
 open Pcoq
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 9446f9df4d..c84a7c00a7 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -6,6 +6,7 @@
 (*         *       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 4265c416b6..519283759a 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -9,6 +9,7 @@
 (** 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 b237e917d5..0fbb9df2db 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -6,6 +6,7 @@
 (*         *       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 e5e2e41975..09fc549c60 100644
--- a/plugins/ltac/profile_ltac.mli
+++ b/plugins/ltac/profile_ltac.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+
 (** Ltac profiling primitives *)
 
 val do_profile :
diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4
index 8cb76d81c5..83fb6963b8 100644
--- a/plugins/ltac/profile_ltac_tactics.ml4
+++ b/plugins/ltac/profile_ltac_tactics.ml4
@@ -10,6 +10,7 @@
 
 (** Ltac profiling entrypoints *)
 
+open API
 open Profile_ltac
 open Stdarg
 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 68dc1fd376..9069635c12 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -6,6 +6,7 @@
 (*         *       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 6683d753bc..77286452bf 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Names
 open Constr
 open Environ
diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml
index 42552c4846..2c9bf14be2 100644
--- a/plugins/ltac/tacarg.ml
+++ b/plugins/ltac/tacarg.ml
@@ -8,6 +8,7 @@
 
 (** 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 bfa423db20..e82cb516c0 100644
--- a/plugins/ltac/tacarg.mli
+++ b/plugins/ltac/tacarg.mli
@@ -6,6 +6,7 @@
 (*         *       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 e037bb4b26..14e5aa72af 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -6,6 +6,7 @@
 (*         *       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 9883c03c46..2c02171d0d 100644
--- a/plugins/ltac/taccoerce.mli
+++ b/plugins/ltac/taccoerce.mli
@@ -6,6 +6,7 @@
 (*         *       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 f44ccbd3b5..dbc32c2f6c 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Pp
 open CErrors
 open Util
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 07aa7ad82e..c5223052cc 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -8,6 +8,8 @@
 
 (** 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 efb7e780db..14b5e00c72 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -6,6 +6,7 @@
 (*         *       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 d1e2a7bbe6..2295852ce3 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -6,6 +6,7 @@
 (*         *       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 cfb698cd87..9b6ac8a9ae 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -6,6 +6,7 @@
 (*         *       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 d201cf9490..bc1dd26d92 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Pattern
 open Pp
 open Genredexpr
@@ -14,7 +16,6 @@ open Tacred
 open CErrors
 open Util
 open Names
-open Nameops
 open Libnames
 open Globnames
 open Nametab
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 8ad52ca023..1841ab42bf 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Pp
 open Names
 open Tacexpr
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index ff76d06cf3..85d3944b18 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Constrintern
 open Patternops
 open Pp
diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli
index fb50a64346..a1841afe36 100644
--- a/plugins/ltac/tacinterp.mli
+++ b/plugins/ltac/tacinterp.mli
@@ -6,6 +6,7 @@
 (*         *       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 2858df3130..6d33724f1a 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
+open Grammar_API
 open Util
 open Tacexpr
 open Mod_subst
diff --git a/plugins/ltac/tacsubst.mli b/plugins/ltac/tacsubst.mli
index c1bf272579..2cfe8fac94 100644
--- a/plugins/ltac/tacsubst.mli
+++ b/plugins/ltac/tacsubst.mli
@@ -6,6 +6,7 @@
 (*         *       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 e6d0370f36..8126421c7d 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -6,6 +6,7 @@
 (*         *       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 ac35464c45..6cfaed3053 100644
--- a/plugins/ltac/tactic_debug.mli
+++ b/plugins/ltac/tactic_debug.mli
@@ -6,6 +6,7 @@
 (*         *       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 5b5cd06cc7..6dcef414c2 100644
--- a/plugins/ltac/tactic_matching.ml
+++ b/plugins/ltac/tactic_matching.ml
@@ -9,6 +9,7 @@
 (** 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 300b546f11..304eec463e 100644
--- a/plugins/ltac/tactic_matching.mli
+++ b/plugins/ltac/tactic_matching.mli
@@ -6,6 +6,8 @@
 (*         *       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 a5ba3b8371..53dfe22a9c 100644
--- a/plugins/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
@@ -6,6 +6,7 @@
 (*         *       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 ed759a76db..2817b54a11 100644
--- a/plugins/ltac/tactic_option.mli
+++ b/plugins/ltac/tactic_option.mli
@@ -6,6 +6,7 @@
 (*         *       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 d8e21d81d1..13492ed51c 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open API
 open Term
 open EConstr
 open Hipattern