create new package for stdpp-bitvector library

_CoqProject

@@ -2,6 +2,7 @@
 # `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
 -Q stdpp stdpp
 -Q stdpp_unstable stdpp.unstable
+-Q stdpp_bitvector stdpp.bv
 # Fixing this one requires Coq 8.19
 -arg -w -arg -argument-scope-delimiter
 
@@ -55,6 +56,6 @@ stdpp/telescopes.v
 stdpp/binders.v
 stdpp/ssreflect.v
 
-stdpp_unstable/bitblast.v
-stdpp_unstable/bitvector.v
-stdpp_unstable/bitvector_tactics.v
+stdpp_bitvector/bitblast.v
+stdpp_bitvector/bitvector.v
+stdpp_bitvector/bitvector_tactics.v

coq-stdpp-bitvector.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The std++ team"
+license: "BSD-3-Clause"
+homepage: "https://gitlab.mpi-sws.org/iris/stdpp"
+bug-reports: "https://gitlab.mpi-sws.org/iris/stdpp/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/stdpp.git"
+version: "dev"
+
+synopsis: "std++ bitvector"
+description: """
+Needs description
+"""
+tags: [
+  "logpath:stdpp.bv"
+]
+
+depends: [
+  "coq-stdpp" {= version}
+]
+
+build: ["./make-package" "stdpp_bitvector" "-j%{jobs}%"]
+install: ["./make-package" "stdpp_bitvector" "install"]

stdpp_unstable/bitvector_tactics.v → stdpp_bitvector/bitvector_tactics.v

 (** This file is still experimental. See its tracking issue
 https://gitlab.mpi-sws.org/iris/stdpp/-/issues/146 for details on remaining
 issues before stabilization. This file is maintained by Michael Sammler. *)
-From stdpp.unstable Require Export bitvector.
-From stdpp.unstable Require Import bitblast.
+From stdpp.bv Require Export bitvector.
+From stdpp.bv Require Import bitblast.
 From stdpp Require Import options.
 
 (** * bitvector tactics *)

tests/bitblast.v

-From stdpp.unstable Require Import bitblast.
+From stdpp.bv Require Import bitblast.
 
 Local Open Scope Z_scope.
 

tests/bitvector.v

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

tests/bitvector_tactics.v

 From stdpp Require Import strings.
-From stdpp.unstable Require Import bitblast bitvector_tactics.
+From stdpp.bv Require Import bitblast bitvector_tactics.
 Unset Mangle Names.
 
 Local Open Scope Z_scope.