From cf57e0cdafd45cf6944666086ec14174705f0b61 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 16 Jul 2008 14:34:15 +0000
Subject: ROmega : make it work even if no Require Import ZArith has been done

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11228 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/romega/ROmega.v        | 1 +
 contrib/romega/ReflOmegaCore.v | 3 +--
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index 68bc43bb60..4281cc5736 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -9,3 +9,4 @@
 Require Import ReflOmegaCore.
 Require Export Setoid.
 Require Export PreOmega.
+Require Export ZArith_base.
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 9d379548a6..12176d661d 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -7,7 +7,7 @@
 
  *************************************************************************)
 
-Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable.
+Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base.
 Delimit Scope Int_scope with I.
 
 (* Abstract Integers. *)
@@ -81,7 +81,6 @@ End Int.
 
 Module Z_as_Int <: Int.
 
-  Require Import ZArith_base.
   Open Scope Z_scope.
 
   Definition int := Z. 
-- 
cgit v1.2.3