From bd41c9d104550ad5472a28655cd6353ba6df1696 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 6 Feb 2014 01:05:30 +0100
Subject: Less dependencies in Omega.

---
 plugins/omega/Omega.v             | 2 +-
 plugins/setoid_ring/InitialRing.v | 3 +--
 theories/NArith/Nnat.v            | 2 +-
 3 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/plugins/omega/Omega.v b/plugins/omega/Omega.v
index ea5a8cb712..7e7b52bb90 100644
--- a/plugins/omega/Omega.v
+++ b/plugins/omega/Omega.v
@@ -54,4 +54,4 @@ Hint Extern 10 (~ (_ < _)%Z) => abstract omega: zarith.
 Hint Extern 10 (~ (_ >= _)%Z) => abstract omega: zarith.
 Hint Extern 10 (~ (_ > _)%Z) => abstract omega: zarith.
 
-Hint Extern 10 False => abstract omega: zarith.
\ No newline at end of file
+Hint Extern 10 False => abstract omega: zarith.
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index e805151ce4..ca178dd384 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -6,8 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import ZArith_base.
-Require Import Zpow_def.
+Require Import Zbool.
 Require Import BinInt.
 Require Import BinNat.
 Require Import Setoid.
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 346169e7fc..cddc5f4cfb 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Arith_base Compare_dec Sumbool Div2 Min Max.
+Require Import Minus Compare_dec Sumbool Div2 Min Max.
 Require Import BinPos BinNat Pnat.
 
 (** * Conversions from [N] to [nat] *)
-- 
cgit v1.2.3