Moving the Ltac plugin to a pack-based one.

This is cumbersome, because now code may fail at link time if it's not
referring to the correct module name. Therefore, one has to add corresponding
open statements a the top of every file depending on a Ltac module. This
includes seemingly unrelated files that use EXTEND statements.

23 files changed, 25 insertions, 2 deletions

diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4
index f3e2c99f4..298027448 100644
--- a/plugins/btauto/g_btauto.ml4
+++ b/plugins/btauto/g_btauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "btauto_plugin"
 
 TACTIC EXTEND btauto
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index 6f6811334..7e76854b1 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Cctac
 open Stdarg
 
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index f68c01b18..2b63ed6d6 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Names
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index e19dc86c4..deb2ede1d 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Pp
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 18a35c6cf..a71d20f0d 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -10,6 +10,7 @@
 
 DECLARE PLUGIN "decl_mode_plugin"
 
+open Ltac_plugin
 open Compat
 open Pp
 open Decl_expr
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 59a0bb5a2..f5de638ed 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open CErrors
 open Pp
 open Decl_expr
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index e1d6bb4a8..3ed959cf2 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -12,6 +12,7 @@ DECLARE PLUGIN "extraction_plugin"
 
 (* ML names *)
 
+open Ltac_plugin
 open Genarg
 open Stdarg
 open Pcoq.Prim
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 260e86ad6..e28d6aa62 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open Ltac_plugin
 open Formula
 open Sequent
 open Ground
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 628af4e71..d6cd7e2a0 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open Formula
 open Sequent
 open Rules
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index 7c665ae7b..1960fa835 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open FourierR
 
 DECLARE PLUGIN "fourier_plugin"
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 6603a95a8..368b23be3 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 (*i camlp4deps: "grammar/grammar.cma" i*)
+open Ltac_plugin
 open Compat
 open Util
 open Term
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index c8b4e4833..70333b063 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open Tacexpr
 open Declarations
 open CErrors
diff --git a/plugins/ltac/ltac_plugin.mllib b/plugins/ltac/ltac_plugin.mlpack
index af1c7149d..af1c7149d 100644
--- a/plugins/ltac/ltac_plugin.mllib
+++ b/plugins/ltac/ltac_plugin.mlpack
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 79020ed03..ccb6daa11 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -16,6 +16,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Stdarg
 open Tacarg
 
diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4
index 5f906a8da..195dec362 100644
--- a/plugins/nsatz/g_nsatz.ml4
+++ b/plugins/nsatz/g_nsatz.ml4
@@ -1,5 +1,3 @@
-DECLARE PLUGIN "nsatz_plugin"
-
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
@@ -10,6 +8,8 @@ DECLARE PLUGIN "nsatz_plugin"
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "nsatz_plugin"
 
 TACTIC EXTEND nsatz_compute
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 27115abec..6b711a176 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -17,6 +17,7 @@
 
 DECLARE PLUGIN "omega_plugin"
 
+open Ltac_plugin
 open Names
 open Coq_omega
 open Stdarg
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index e7e6ecef9..f2c021f59 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Names
 open Misctypes
 open Tacexpr
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index 2f38688d1..9a54ad778 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -10,6 +10,7 @@
 
 DECLARE PLUGIN "romega_plugin"
 
+open Ltac_plugin
 open Names
 open Refl_omega
 open Stdarg
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index d27b04834..7e58ef9a3 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+open Ltac_plugin
+
 DECLARE PLUGIN "rtauto_plugin"
 
 TACTIC EXTEND rtauto
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 367a13333..35d6768c1 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -8,6 +8,7 @@
 
 module Search = Explore.Make(Proof_search)
 
+open Ltac_plugin
 open CErrors
 open Util
 open Term
diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4
index 0987c44ae..707ff79a6 100644
--- a/plugins/setoid_ring/g_newring.ml4
+++ b/plugins/setoid_ring/g_newring.ml4
@@ -8,6 +8,7 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Pp
 open Util
 open Libnames
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 657efe175..59f23a637 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -6,6 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Ltac_plugin
 open Pp
 open CErrors
 open Util
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index fc988a2c5..f4f6efa4a 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -15,6 +15,7 @@ let frozen_lexer = CLexer.freeze () ;;
 (*i camlp4use: "pa_extend.cmo" i*)
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+open Ltac_plugin
 open Names
 open Pp
 open Pcoq