aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/micromega/Psatz.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/micromega/Psatz.v')
-rw-r--r--plugins/micromega/Psatz.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 5090542c6..804a16b79 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -18,7 +18,7 @@ Require Import RMicromega.
Require Import QArith.
Require Import ZArith.
Require Import Rdefinitions.
-Require Export RingMicromega.
+Require Import RingMicromega.
Require Import VarMap.
Require Tauto.
Declare ML Module "micromega_plugin".