diff --git a/theories/bitvector.v b/theories/bitvector.v
index b5fd0bb8eca65f54b23eececbcdba960c3922b4a..69515089bb051bf2f5d8a3a8d2f106603ec6d20b 100644
--- a/theories/bitvector.v
+++ b/theories/bitvector.v
@@ -358,16 +358,15 @@ Qed.
 
 (** * Notation for [bv n] *)
 Ltac solve_bitvector_eq :=
-  try (vm_compute; done);
+  try (vm_compute; exact (conj eq_refl eq_refl));
   lazymatch goal with
-  | |- -1 < ?v < 2 ^ ?l =>
-    fail "Bitvector constant" v "does not fit into" l "bits"
+    |- bv_wf ?n ?v =>
+    fail "Bitvector constant" v "does not fit into" n "bits"
   end.
 
 Notation "'[BV{' l }  v ]" := (BV l v _) (at level 9, only printing) : stdpp_scope.
 (* TODO: Somehow the following version creates a warning. *)
 (* Notation "'[BV{' l } v ]" := (BV l v _) (at level 9, format "[BV{ l }  v ]", only printing) : stdpp_scope. *)
-(* TODO: This notation breaks when used in gmap notations. Why? *)
 Notation "'[BV{' l }  v ]" := (BV l v ltac:(solve_bitvector_eq)) (at level 9, only parsing) : stdpp_scope.
 
 (** * Automation *)