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 ea1660d90..63057c3ae 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 7db484d82..958f43bd7 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 cfe747665..7c734cd9a 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 fdb8d3461..b26fd78ef 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 9b4167512..b2b3f8b6b 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 8afe3053d..9f53c44a4 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 18334dafe..c7ec26967 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 2c2a4b850..68b63f02c 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 dd5307638..3d7d5e3fe 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 679aa1127..e91e25111 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 36ac10bfe..7855fbcfc 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 4dceb0331..18e62a211 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 25258ffa9..e6ddc5cc1 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 83bfd0233..e94cf1c63 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 7e979d269..84c5d3a44 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 810e1ec39..9261a11c7 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 9446f9df4..c84a7c00a 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 4265c416b..519283759 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 b237e917d..0fbb9df2d 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 e5e2e4197..09fc549c6 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 8cb76d81c..83fb6963b 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 68dc1fd37..9069635c1 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 6683d753b..77286452b 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 42552c484..2c9bf14be 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 bfa423db2..e82cb516c 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 e037bb4b2..14e5aa72a 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 9883c03c4..2c02171d0 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 f44ccbd3b..dbc32c2f6 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 07aa7ad82..c5223052c 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 efb7e780d..14b5e00c7 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 d1e2a7bbe..2295852ce 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 cfb698cd8..9b6ac8a9a 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 d201cf949..bc1dd26d9 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 8ad52ca02..1841ab42b 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 ff76d06cf..85d3944b1 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 fb50a6434..a1841afe3 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 2858df313..6d33724f1 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 c1bf27257..2cfe8fac9 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 e6d0370f3..8126421c7 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 ac35464c4..6cfaed305 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 5b5cd06cc..6dcef414c 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 300b546f1..304eec463 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 a5ba3b837..53dfe22a9 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 ed759a76d..2817b54a1 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 d8e21d81d..13492ed51 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