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.
 
 (*****************************************************************)