Merge PR #18947: deprecate Bvector

Reviewed-by: proux01
Co-authored-by: proux01 <proux01@users.noreply.github.com>

2 files changed, 29 insertions, 1 deletions

diff --git a/doc/changelog/11-standard-library/18947-deprecate-Bvector.rst b/doc/changelog/11-standard-library/18947-deprecate-Bvector.rst
new file mode 100644
index 0000000..eacd903
--- /dev/null
+++ b/doc/changelog/11-standard-library/18947-deprecate-Bvector.rst
@@ -0,0 +1,3 @@
+- **Deprecated:** ``Bool.Bvector``. Users are encouraged to consider ``list bool`` instead. Please open an issue if you would like to keep using ``Bvector``.
+  (`#18947 <https://github.com/coq/coq/pull/18947>`_,
+  by Andres Erbsen).
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 8016e9b..8a42d5b 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -10,7 +10,8 @@
 
 (** N.B.: Using this encoding of bit vectors is discouraged.
 See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>. *)
-Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be technically difficult, see <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v>.").
+Attributes deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.").
+Local Set Warnings "-deprecated".
 
 (** Bit vectors. Contribution by Jean Duprat (ENS Lyon). *)
 
@@ -50,53 +51,72 @@ NOTA BENE: all shift operations expect predecessor of size as parameter
 (they only work on non-empty vectors).
 *)
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. Please open an issue if you would like to keep using Bvector.")]
 Definition Bvector := Vector.t bool.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition Bnil := @Vector.nil bool.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition Bcons := @Vector.cons bool.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition Bvect_true := Vector.const true.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition Bvect_false := Vector.const false.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition Blow := @Vector.hd bool.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition Bhigh := @Vector.tl bool.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition Bsign := @Vector.last bool.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition Bneg := @Vector.map _ _ negb.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition BVand := @Vector.map2 _ _ _ andb.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition BVor := @Vector.map2 _ _ _ orb.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition BVxor := @Vector.map2 _ _ _ xorb.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition BVeq m n := @Vector.eqb bool eqb m n.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) :=
   Bcons carry n (Vector.shiftout bv).
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition BshiftRl (n:nat) (bv:Bvector (S n)) (carry:bool) :=
   Bhigh (S n) (Vector.shiftin carry bv).
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Definition BshiftRa (n:nat) (bv:Bvector (S n)) :=
   Bhigh (S n) (Vector.shiftrepeat bv).
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Fixpoint BshiftL_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   match p with
     | O => bv
     | S p' => BshiftL n (BshiftL_iter n bv p') false
   end.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Fixpoint BshiftRl_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   match p with
     | O => bv
     | S p' => BshiftRl n (BshiftRl_iter n bv p') false
   end.
 
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) :=
   match p with
     | O => bv
@@ -108,10 +128,15 @@ End BOOLEAN_VECTORS.
 Module BvectorNotations.
 Declare Scope Bvector_scope.
 Delimit Scope Bvector_scope with Bvector.
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Notation "^~ x" := (Bneg _ x) (at level 35, right associativity) : Bvector_scope.
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Infix    "^&"   := (BVand  _) (at level 40, left  associativity) : Bvector_scope.
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Infix    "^⊕"   := (BVxor  _) (at level 45, left  associativity) : Bvector_scope.
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Infix    "^|"   := (BVor   _) (at level 50, left  associativity) : Bvector_scope.
+#[deprecated(since="8.20", note="Consider [list bool] instead. See <https://github.com/coq/coq/blob/master/theories/Vectors/Vector.v> for details. Please open an issue if you would like to keep using Bvector.")]
 Infix    "=?"   := (BVeq _ _) (at level 70, no    associativity) : Bvector_scope.
 Open Scope Bvector_scope.
 End BvectorNotations.