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.

10 files changed, 10 insertions, 0 deletions

diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index c296d427d..2cfd2790f 100644
--- a/theories/Reals/Cos_plus.v
+++ b/theories/Reals/Cos_plus.v
@@ -12,6 +12,7 @@ Require Import SeqSeries.
 Require Import Rtrigo_def.
 Require Import Cos_rel.
 Require Import Max.
+Require Import Omega.
 Local Open Scope nat_scope.
 Local Open Scope R_scope.
 
diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index 9c7472fe0..335d5b16a 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -10,6 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo_def.
+Require Import Omega.
 Local Open Scope R_scope.
 
 Definition A1 (x:R) (N:nat) : R :=
diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 40064fd51..dbf48e61a 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -15,6 +15,7 @@ Require Import PSeries_reg.
 Require Import Div2.
 Require Import Even.
 Require Import Max.
+Require Import Omega.
 Local Open Scope nat_scope.
 Local Open Scope R_scope.
 
diff --git a/theories/Reals/Machin.v b/theories/Reals/Machin.v
index 0166ceda6..311f29098 100644
--- a/theories/Reals/Machin.v
+++ b/theories/Reals/Machin.v
@@ -16,6 +16,7 @@ Require Import Rseries.
 Require Import SeqProp.
 Require Import PartSum.
 Require Import Ratan.
+Require Import Omega.
 
 Local Open Scope R_scope.
 
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v
index b2d9c749f..c66c7b412 100644
--- a/theories/Reals/Ranalysis2.v
+++ b/theories/Reals/Ranalysis2.v
@@ -9,6 +9,7 @@
 Require Import Rbase.
 Require Import Rfunctions.
 Require Import Ranalysis1.
+Require Import Omega.
 Local Open Scope R_scope.
 
 (**********)
diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index 0614f3998..3a5f932dd 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -14,6 +14,7 @@ Require Import Fourier.
 Require Import RiemannInt.
 Require Import SeqProp.
 Require Import Max.
+Require Import Omega.
 Local Open Scope R_scope.
 
 (** * Preliminaries lemmas *)
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
index 45a703270..dcf2f9709 100644
--- a/theories/Reals/Ratan.v
+++ b/theories/Reals/Ratan.v
@@ -18,6 +18,7 @@ Require Import SeqProp.
 Require Import Ranalysis5.
 Require Import SeqSeries.
 Require Import PartSum.
+Require Import Omega.
 
 Local Open Scope R_scope.
 
diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 88c4de239..d5f1994c5 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -12,6 +12,7 @@ Require Import Rfunctions.
 Require Import Rseries.
 Require Import PartSum.
 Require Import Binomial.
+Require Import Omega.
 Local Open Scope R_scope.
 
 (** TT Ak; 0<=k<=N *)
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 76b44d969..ae8074a28 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.v
@@ -10,6 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
 Require Import PartSum.
+Require Import Omega.
 Local Open Scope R_scope.
 
 Set Implicit Arguments.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 52657b401..7f3282a35 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -10,6 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
 Require Import Max.
+Require Import Omega.
 Local Open Scope R_scope.
 
 (*****************************************************************)