Now parsing rules of ML-declared tactics are only made available after the

corresponding Declare ML Module command. This changes essentially two
things:

1. ML plugins are forced to use the DECLARE PLUGIN statement before any
TACTIC EXTEND statement. The plugin name must be exactly the string passed to
the Declare ML Module command.

2. ML tactics are only made available after the Coq module that does the
corresponding Declare ML Module is imported. This may break a few things,
as it already broke quite some uses of omega in the stdlib.

15 files changed, 27 insertions, 2 deletions

diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index 795211c200..bc5a390027 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -1,4 +1,4 @@
-Require Import Bool PArith DecidableClass ROmega.
+Require Import Bool PArith DecidableClass Omega ROmega.
 
 Ltac bool :=
 repeat match goal with
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index e31948ffe4..8a95d5b4be 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -1,4 +1,4 @@
-Require Import Bool DecidableClass Algebra Ring PArith ROmega.
+Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega.
 
 Section Bool.
 
diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4
index a45203d3dd..ce99756e01 100644
--- a/plugins/btauto/g_btauto.ml4
+++ b/plugins/btauto/g_btauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+DECLARE PLUGIN "btauto_plugin"
+
 TACTIC EXTEND btauto
 | [ "btauto" ] -> [ Refl_btauto.Btauto.tac ]
 END
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index c2c437c80c..5d6f172c4c 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.ml4
@@ -10,6 +10,8 @@
 
 open Cctac
 
+DECLARE PLUGIN "cc_plugin"
+
 (* Tactic registration *)
 
 TACTIC EXTEND cc
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 9ae8fcbf67..c3ae05de6a 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -16,6 +16,8 @@ open Tacticals
 open Tacinterp
 open Libnames
 
+DECLARE PLUGIN "ground_plugin"
+
 (* declaring search depth as a global option *)
 
 let ground_depth=ref 3
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index 1635cecc08..11107385da 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -10,6 +10,8 @@
 
 open FourierR
 
+DECLARE PLUGIN "fourier_plugin"
+
 TACTIC EXTEND fourier
   [ "fourierz" ] -> [ Proofview.V82.tactic fourier ]
 END
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 90282fcf7b..21d0b9f3db 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -19,6 +19,8 @@ open Genarg
 open Tacticals
 open Misctypes
 
+DECLARE PLUGIN "recdef_plugin"
+
 let pr_binding prc = function
   | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ cut () ++ prc c)
   | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 78d1e17563..7ed40acb43 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -19,6 +19,8 @@
 open Errors
 open Misctypes
 
+DECLARE PLUGIN "micromega_plugin"
+
 let out_arg = function
   | ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable")
   | ArgArg x -> x
diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 6fd8ab8e9a..20b3ac1e1c 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.ml4
@@ -17,6 +17,8 @@ open Coqlib
 open Num
 open Utile
 
+DECLARE PLUGIN "nsatz_plugin"
+
 (***********************************************************************
  Operations on coefficients
 *)
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index b384478ae2..83092ccc49 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -15,6 +15,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+DECLARE PLUGIN "omega_plugin"
+
 open Coq_omega
 
 let omega_tactic l =
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 1f11b07ad9..47a62c9e6f 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.ml4
@@ -14,6 +14,8 @@ open Tacexpr
 open Geninterp
 open Quote
 
+DECLARE PLUGIN "quote_plugin"
+
 let loc = Loc.ghost
 let cont = (loc, Id.of_string "cont")
 let x = (loc, Id.of_string "x")
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index c07825f8cd..4b6c9b7905 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma" i*)
 
+DECLARE PLUGIN "romega_plugin"
+
 open Refl_omega
 
 let romega_tactic l =
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 7d0b7a1bc1..b908547011 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -8,6 +8,8 @@
 
 (*i camlp4deps: "grammar/grammar.cma"  i*)
 
+DECLARE PLUGIN "rtauto_plugin"
+
 TACTIC EXTEND rtauto
   [ "rtauto" ] -> [ Proofview.V82.tactic (Refl_tauto.rtauto_tac) ]
 END
diff --git a/plugins/setoid_ring/Rings_Z.v b/plugins/setoid_ring/Rings_Z.v
index 58a4d7ea65..605a23a987 100644
--- a/plugins/setoid_ring/Rings_Z.v
+++ b/plugins/setoid_ring/Rings_Z.v
@@ -1,6 +1,7 @@
 Require Export Cring.
 Require Export Integral_domain.
 Require Export Ncring_initial.
+Require Export Omega.
 
 Instance Zcri: (Cring (Rr:=Zr)).
 red. exact Z.mul_comm. Defined.
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 8df061870d..8d83ffc330 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -31,6 +31,8 @@ open Decl_kinds
 open Entries
 open Misctypes
 
+DECLARE PLUGIN "newring_plugin"
+
 (****************************************************************************)
 (* controlled reduction *)