aboutsummaryrefslogtreecommitdiff
path: root/plugins/btauto/Reflect.v
diff options
context:
space:
mode:
authorVincent Laporte2018-09-11 14:32:22 +0200
committerVincent Laporte2018-09-25 09:45:55 +0000
commita1f10626bed1db14ce116e9201ed05dadfc366b4 (patch)
treee8f35a49caa3a8b8f6c96a84344fd666401a17e9 /plugins/btauto/Reflect.v
parent7eb8a7eb8d23ffaf149f71a46fb1b089b90db7f8 (diff)
Remove romega
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 3bd7cd622c..d82e8ae8ad 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -1,4 +1,4 @@
-Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega.
+Require Import Bool DecidableClass Algebra Ring PArith Omega.
Section Bool.