13 files changed, 21 insertions, 1 deletions
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index d3b65c1746..7cf478e183 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -80,3 +80,12 @@ Delimit Scope core_scope with core.
 
 Open Scope core_scope.
 Open Scope type_scope.
+
+(** ML Tactic Notations *)
+
+Declare ML Module "extratactics".
+Declare ML Module "eauto".
+Declare ML Module "g_class".
+Declare ML Module "g_eqdecide".
+Declare ML Module "g_rewrite".
+Declare ML Module "tauto".
diff --git a/theories/Reals/Cos_plus.v b/theories/Reals/Cos_plus.v
index c296d427d0..2cfd2790fb 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 9c7472fe05..335d5b16a1 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 40064fd511..dbf48e61a7 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 0166ceda65..311f290987 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 b2d9c749fd..c66c7b412b 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 0614f39982..3a5f932dde 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 45a7032707..dcf2f97095 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 88c4de2390..d5f1994c56 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 76b44d9690..ae8074a28c 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 52657b4015..7f3282a358 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.
 
 (*****************************************************************)
diff --git a/theories/Sorting/PermutEq.v b/theories/Sorting/PermutEq.v
index 995a77ccec..87ffce0b6f 100644
--- a/theories/Sorting/PermutEq.v
+++ b/theories/Sorting/PermutEq.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation.
+Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation Omega.
 
 Set Implicit Arguments.
 
diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index 40d2b1295f..aeddeb70c2 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -23,6 +23,7 @@ Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zdiv.
 Require Import Znumtheory.
+Require Import Omega.
 
 Open Scope Z_scope.