update file structure

CHANGELOG.md

@@ -32,11 +32,12 @@ Coq 8.19 is newly supported by this version of std++.
   `{[ (x, y) : nat * nat | x = y ]}`. (by Thibaut Pérami)
 - Add `inv select` and `inversion select` tactics that allow selecting the
   to-be-inverted hypothesis with a pattern.
-- Create a `coq-stdpp-bitvector` package containing the previously
-  unstable `bitvector` library. Users of the library need to change
-  the import path from `stdpp.unstable.bitvector` to
-  `stdpp.bitvector.bitvector` and from `stdpp.unstable.bitvector_tactics` to
-  `stdpp.bitvector.tactics`.
+- The new `coq-stdpp-bitvector` package contains a library for `n`-bit
+  bitvectors (i.e., fixed-size integers with `n` bits).
+  Users of the previous unstable version need to change the import path from
+  `stdpp.unstable.bitvector` to `stdpp.bitvector.definitions` and from
+  `stdpp.unstable.bitvector_tactics` to `stdpp.bitvector.tactics`. The
+  complete library can be imported with `stdpp.bitvector.bitvector`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

_CoqProject

@@ -56,7 +56,8 @@ stdpp/telescopes.v
 stdpp/binders.v
 stdpp/ssreflect.v
 
-stdpp_bitvector/bitvector.v
+stdpp_bitvector/definitions.v
 stdpp_bitvector/tactics.v
+stdpp_bitvector/bitvector.v
 
 stdpp_unstable/bitblast.v

stdpp_bitvector/tactics.v

 (** This file is maintained by Michael Sammler. *)
-From stdpp.bitvector Require Export bitvector.
+From stdpp.bitvector Require Export definitions.
 From stdpp Require Import options.
 
 (** * bitvector tactics *)

stdpp_unstable/bitblast.v

@@ -3,7 +3,7 @@ https://gitlab.mpi-sws.org/iris/stdpp/-/issues/141 for details on remaining
 issues before stabilization. This file is maintained by Michael Sammler. *)
 From Coq Require Import ssreflect.
 From Coq.btauto Require Export Btauto.
-From stdpp.bitvector Require Import bitvector.
+From stdpp.bitvector Require Import definitions.
 From stdpp Require Export tactics numbers list.
 From stdpp Require Import options.
 

tests/bitvector.v → tests/bitvector_definitions.v

 From stdpp Require Import strings.
-From stdpp.bitvector Require Import bitvector.
+From stdpp.bitvector Require Import definitions.
 
 Check "notation_test".
 Check (BV 10 3 = BV 10 5).