diff options
Diffstat (limited to 'contrib/romega/ReflOmegaCore.v')
| -rw-r--r-- | contrib/romega/ReflOmegaCore.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index 9d379548..12176d66 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. |