15 files changed, 27 insertions, 2 deletions
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index 795211c20..bc5a39002 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 e31948ffe..8a95d5b4b 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 a45203d3d..ce99756e0 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 c2c437c80..5d6f172c4 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 9ae8fcbf6..c3ae05de6 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 1635cecc0..11107385d 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 90282fcf7..21d0b9f3d 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 78d1e1756..7ed40acb4 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 6fd8ab8e9..20b3ac1e1 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 b384478ae..83092ccc4 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 1f11b07ad..47a62c9e6 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 c07825f8c..4b6c9b790 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 7d0b7a1bc..b90854701 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 58a4d7ea6..605a23a98 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 8df061870..8d83ffc33 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 *)