From 8581e1a977518c354eb06820d3513238412af7de Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Mon, 30 Mar 2015 22:15:02 +0200
Subject: Accomodating #4166 (providing "Require Import OmegaTactic" as a
 replacement for 8.4's "Require Omega").

---
 theories/Reals/Cos_rel.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Reals')

diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v
index cfb30662b..6d30319c9 100644
--- a/theories/Reals/Cos_rel.v
+++ b/theories/Reals/Cos_rel.v
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import SeqSeries.
 Require Import Rtrigo_def.
-Require Import Omega.
+Require Import OmegaTactic.
 Local Open Scope R_scope.
 
 Definition A1 (x:R) (N:nat) : R :=
-- 
cgit v1.2.3