aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool/Bvector.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Bool/Bvector.v')
-rw-r--r--theories/Bool/Bvector.v1
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 472af69c5..b41d65c39 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -10,7 +10,6 @@
Require Export Bool Sumbool.
Require Import Minus.
-Import Lt. (* For Hints *)
Open Local Scope nat_scope.