Merge branch 'msammler/coq_16748' into 'master'

Fix bitvector tests for coq#16748

See merge request !421

tests/bitvector.v

@@ -5,7 +5,7 @@ Check "notation_test".
 Check (BV 10 3 = BV 10 5).
 Fail Check (BV 2 3 = BV 10 5).
 Check (BV 2 3 =@{bvn} BV 10 5).
-Fail Goal (BV 2 4 = BV 2 5).
+Fail Goal (BV 2 4 = BV 2 3).
 
 Check "bvn_to_bv_test".
 Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). Proof. simpl. Show. done. Abort.