diff options
| author | letouzey | 2008-07-16 14:34:15 +0000 |
|---|---|---|
| committer | letouzey | 2008-07-16 14:34:15 +0000 |
| commit | cf57e0cdafd45cf6944666086ec14174705f0b61 (patch) | |
| tree | 059cc054c4178306ff8fc2768240e0b8cdd3440f | |
| parent | 65ebb5f12290fe8046105b1f1ebd31faaea22c3b (diff) | |
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
| -rw-r--r-- | contrib/romega/ROmega.v | 1 | ||||
| -rw-r--r-- | 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. |