diff options
Diffstat (limited to 'contrib/micromega/Micromegatac.v')
| -rw-r--r-- | contrib/micromega/Micromegatac.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/micromega/Micromegatac.v b/contrib/micromega/Micromegatac.v index 5459634c9..13c7eace1 100644 --- a/contrib/micromega/Micromegatac.v +++ b/contrib/micromega/Micromegatac.v @@ -18,7 +18,7 @@ Require Import RMicromega. Require Import QArith. Require Export Ring_normalize. Require Import ZArith. -Require Import Reals. +Require Import Raxioms. Require Export RingMicromega. Require Import VarMap. Require Tauto. |