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 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

(limited to 'plugins')

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.
-- 
cgit v1.2.3