Merge branch 'msammler/coq_17648' into 'master'

Fix tests for coq#17648

See merge request !479

tests/bitvector.ref

@@ -6,11 +6,6 @@ The command has indeed failed with message:
 The term "BV 10 5" has type "bv 10" while it is expected to have type "bv 2".
 BV 2 3 = BV 10 5
      : Prop
-The command has indeed failed with message:
-Unable to satisfy the following constraints:
-
-?bv_is_wf : "BvWf 2 4"
-
 "bvn_to_bv_test"
      : string
 1 goal

tests/bitvector.v

@@ -5,7 +5,6 @@ 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 3).
 
 Check "bvn_to_bv_test".
 Goal bvn_to_bv 2 (BV 2 3) = Some (BV 2 3). Proof. simpl. Show. done. Abort.