diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/romega/ROmega.v | 1 | ||||
| -rw-r--r-- | contrib/romega/ReflOmegaCore.v | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v index 991267ee5b..68bc43bb60 100644 --- a/contrib/romega/ROmega.v +++ b/contrib/romega/ROmega.v @@ -7,4 +7,5 @@ *************************************************************************) Require Import ReflOmegaCore. +Require Export Setoid. Require Export PreOmega. diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v index ee44d6d214..46512aab00 100644 --- a/contrib/romega/ReflOmegaCore.v +++ b/contrib/romega/ReflOmegaCore.v @@ -7,7 +7,7 @@ *************************************************************************) -Require Import List Bool Sumbool EqNat Ring_theory Decidable. +Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable. Delimit Scope Int_scope with I. (* Abstract Integers. *) |