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.v8
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index d7162e620..5363c5465 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -60,13 +60,13 @@ Definition Bhigh := @Vector.tl bool.
Definition Bsign := @Vector.last bool.
-Definition Bneg n (v : Bvector n) := Vector.map negb v.
+Definition Bneg := @Vector.map _ _ negb.
-Definition BVand n (v : Bvector n) := Vector.map2 andb v.
+Definition BVand := @Vector.map2 _ _ _ andb.
-Definition BVor n (v : Bvector n) := Vector.map2 orb v.
+Definition BVor := @Vector.map2 _ _ _ orb.
-Definition BVxor n (v : Bvector n) := Vector.map2 xorb v.
+Definition BVxor := @Vector.map2 _ _ _ xorb.
Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
Bcons carry n (Vector.shiftout bv).