diff options
Diffstat (limited to 'contrib/micromega/RMicromega.v')
| -rw-r--r-- | contrib/micromega/RMicromega.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/micromega/RMicromega.v b/contrib/micromega/RMicromega.v index a662744bc..ef28db321 100644 --- a/contrib/micromega/RMicromega.v +++ b/contrib/micromega/RMicromega.v @@ -15,7 +15,7 @@ Require Import OrderedRing. Require Import RingMicromega. Require Import Refl. -Require Import Reals. +Require Import Raxioms RIneq Rpow_def DiscrR. Require Setoid. Definition Rsrt : ring_theory R0 R1 Rplus Rmult Rminus Ropp (@eq R). |