aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/btauto/Reflect.v
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/btauto/Reflect.v')
-rw-r--r--plugins/btauto/Reflect.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index e31948ffe..8a95d5b4b 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -1,4 +1,4 @@
-Require Import Bool DecidableClass Algebra Ring PArith ROmega.
+Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega.
Section Bool.