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/setoid_ring/InitialRing.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'plugins/setoid_ring')

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