.gitattributes

@@ -3,3 +3,5 @@
 
 # Convert to native line endings on checkout.
 *.ref text
+# Shell scripts need Linux line endings.
+*.sh eol=lf

.gitignore

@@ -15,7 +15,14 @@
 .coq-native/
 Makefile.coq
 Makefile.coq.conf
+_CoqProject
+_CoqProject.*
+Makefile.package.*
+.Makefile.package.*
 *.crashcoqide
 html/
-build-dep/
+builddep/
 _opam
+_build/
+*.install
+config/local-flags

.gitlab-ci.yml

@@ -5,9 +5,29 @@ stages:
 
 variables:
   CPU_CORES: "10"
+  OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
+  # Avoid needlessly increasing our TCB with native_compute
+  COQEXTRAFLAGS: "-native-compiler no"
+
+.only_branches: &only_branches
+  only:
+  - /^master/@iris/stdpp
+  - /^ci/@iris/stdpp
+
+.only_mr: &only_mr
+  only:
+  - merge_requests
+
+.branches_and_mr: &branches_and_mr
+  only:
+  - /^master/@iris/stdpp
+  - /^ci/@iris/stdpp
+  - merge_requests
 
 .template: &template
+  <<: *only_branches
   stage: build
+  interruptible: true
   tags:
   - fp
   script:
@@ -16,10 +36,7 @@ variables:
   cache:
     key: "$CI_JOB_NAME"
     paths:
-    - opamroot/
-  only:
-  - master@iris/stdpp
-  - /^ci/@iris/stdpp
+    - _opam/
   except:
   - triggers
   - schedules
@@ -27,32 +44,52 @@ variables:
 
 ## Build jobs
 
-build-coq.8.12.dev:
+# The newest version runs with timing.
+build-coq.9.0.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.12.dev"
+    OPAM_PINS: "coq version 9.0.0"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
     CI_COQCHK: "1"
-
-build-coq.8.11.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.11.2"
-    OPAM_PKG: "coq-stdpp"
+    OPAM_PKG: "1"
     DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
   tags:
   - fp-timing
+  interruptible: false
+
+# The newest version also runs in MRs, without timing.
+build-coq.9.0.0-mr:
+  <<: *template
+  <<: *only_mr
+  variables:
+    OPAM_PINS: "coq version 9.0.0"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
+
+# Also ensure Dune works (broken on older Coq versions due to Stdlib split).
+build-coq.9.0.0-dune:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 9.0.0   dune version 3.18.1"
+    MAKE_TARGET: "dune"
 
-build-coq.8.10.2:
+build-coq.8.20.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.10.2"
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
 
-build-coq.8.9.1:
+build-coq.8.19.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.9.1"
+    OPAM_PINS: "coq version 8.19.1"
+    DENY_WARNINGS: "1"
 
-build-coq.8.8.2:
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.18.0:
   <<: *template
+  <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.8.2"
+    OPAM_PINS: "coq version 8.18.0"
+    DENY_WARNINGS: "1"

.gitmodules

-[submodule "ci"]
-	path = ci
-	url = https://gitlab.mpi-sws.org/FP/iris-ci.git

CHANGELOG.md

 This file lists "large-ish" changes to the std++ Coq library, but not every
 API-breaking change is listed.
 
-## std++ master
+## 1.12.0 (2025-06-04)
 
-Coq 8.7 is no longer supported by this release.
+std++ 1.12 supports Coq 8.18, 8.19, 8.20, and Rocq 9.0.
+
+This released of std++ was managed by Jesper Bengtson, Ralf Jung,
+and Robbert Krebbers, with contributinos from Andres Erbsen, Kimaya Bedarkar,
+Marijn van Wezel, Michael Sammler, Ralf Jung, Robbert Krebbers, Rodolphe Lepigre,
+Rudy Peterson, and Marijn van Wezel. Thanks a lot to everyone involved.
+
+**Detailed list of changes:**
+
+- Add lemmas `Forall_vinsert` and `Forall_vreplicate`. (by Rudy Peterson)
+- Add `disj_union_list` and associated lemmas for `gmultiset`. (by Marijn van Wezel)
+- Add lemma `lookup_total_fmap`.
+- Add lemmas about `last` and `head`: `last_app_Some`, `last_app_None`,
+  `head_app_Some`, `head_app_None` and `head_app`. (by Marijn van Wezel)
+- Rename `map_filter_empty_iff` to `map_empty_filter` and add
+  `map_empty_filter_1` and `map_empty_filter_2`. (by Michael Sammler)
+- Add lemma about `zip_with`: `lookup_zip_with_None` and add lemmas for `zip`:
+ `length_zip`, `zip_nil_inv`, `lookup_zip_Some`,`lookup_zip_None`. (by Kimaya Bedarkar)
+- Add `elem_of_seq` and `seq_nil`. (by Kimaya Bedarkar)
+- Add lemmas `StronglySorted_app`, `StronglySorted_cons` and
+  `StronglySorted_app_2`. Rename lemmas
+  `elem_of_StronglySorted_app` → `StronglySorted_app_1_elem_of`,
+  `StronglySorted_app_inv_l` → `StronglySorted_app_1_l`
+  `StronglySorted_app_inv_r` → `StronglySorted_app_1_r`. (by Marijn van Wezel)
+- Add `SetUnfoldElemOf` instance for `dom` on `gmultiset`. (by Marijn van Wezel)
+- Split up `stdpp.list` into smaller files. Users should keep importing
+  `stdpp.list`; the organization into smaller modules is considered an
+  implementation detail. `stdpp.list_numbers` is now re-exported by `stdpp.list`
+  and also considered part of the list module, so existing imports should be
+  updated.
+- Remove `list_remove` and `list_remove_list`. There were no lemmas about these
+  functions; they existed solely to facilitate the proofs of decidability of
+  `submseteq` and `≡ₚ`, which have been refactored.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# length
+s/\bmap_filter_empty_iff\b/map_empty_filter/g
+# StronglySorted
+s/\belem_of_StronglySorted_app\b/StronglySorted_app_1_elem_of/g
+s/\bStronglySorted_app_inv_(l|r)\b/StronglySorted_app_1_\1/g
+EOF
+```
+
+## std++ 1.11.0 (2024-10-30)
+
+The highlights of this release include:
+* support for building with dune
+* stronger versions of the induction principles for `map_fold`, exposing the order in
+  which elements are processed
+
+std++ 1.11 supports Coq 8.18, 8.19 and 8.20.
+Coq 8.16 and 8.17 are no longer supported.
+
+This release of std++ was managed by Jesper Bengtson, Ralf Jung, 
+and Robbert Krebbers, with contributions from Andres Erbsen, Lennard Gäher, 
+Léo Stefanesco, Marijn van Wezel, Paolo G. Giarrusso, Pierre Roux,
+Ralf Jung, Robbert Krebbers, Rodolphe Lepigre, Sanjit Bhat, Yannick Zakowski, 
+and Yiyun Liu. Thanks a lot to everyone involved!
+
+
+**Detailed list of changes:**
+
+- Generalize `foldr_comm_acc`, `map_fold_comm_acc`, `set_fold_comm_acc`, and
+  `gmultiset_set_fold_comm_acc` to have more general type. (by Yannick Zakowski)
+- Strengthen `map_disjoint_difference_l` and `map_disjoint_difference_l`, and
+  thereby make them consistent with the corresponding lemmas for sets.
+- Add support for compiling the packages with dune. (by Rodolphe Lepigre)
+- Add lemmas `gset_to_gmap_singleton`, `difference_union_intersection`,
+  `difference_union_intersection_L`. (by Léo Stefanesco)
+- Make the build script compatible with BSD systems. (by Yiyun Liu)
+- Rename lemmas `X_length` into `length_X`, see the sed script below for an
+  overview. This follows https://github.com/coq/coq/pull/18564.
+- Redefine `map_imap` so its closure argument can contain recursive
+  occurrences of a `Fixpoint`.
+- Add lemma `fmap_insert_inv`.
+- Rename `minimal_exists` to `minimal_exists_elem_of` and
+  `minimal_exists_L` to `minimal_exists_elem_of_L`.
+  Add new `minimal_exists` lemma. (by Lennard Gäher)
+- Generalize `map_relation R P Q` to have the key (extra argument `K`) in the
+  predicates `R`, `P` and `Q`.
+- Generalize `map_included R` to a predicate `R : K → A → B → Prop`, i.e., (a)
+  to have the key, and (b) to have different types `A` and `B`.
+- Add `map_Forall2` and some basic lemmas about it.
+- Rename `map_not_Forall2` into `map_not_relation`.
+- Replace the induction principle `map_fold_ind` for `map_fold` with a stronger
+  version:
+  + The main new induction principle is `map_first_key_ind`, which is meant
+    to be used together with the lemmas `map_fold_insert_first_key` and
+    `map_to_list_insert_first_key` (and others about `map_first_key`). This
+    induction scheme reflects all these operations (induction, `map_fold`,
+    `map_to_list`) process the map in the same order.
+  + The new primitive induction principle `map_fold_fmap_ind` is only relevant
+    for implementers of `FinMap` instances.
+  + The lemma `map_fold_foldr` has been strengthened to (a) drop the
+    commutativity requirement and (b) give an equality (`=`) instead of being
+    generic over a relation `R`.
+  + The lemma `map_to_list_fmap` has been strengthened to give an equality (`=`)
+    instead of a permutation (`≡ₚ`).
+  + The lemmas `map_fold_comm_acc_strong` and `map_fold_comm_acc` have been
+    strengthened to only require commutativity w.r.t. the operation being
+    pulled out of the accumulator, not commutativity of
+    the folded function itself.
+- Add lemmas `Sorted_unique_strong` and `StronglySorted_unique_strong` that only
+  require anti-symmetry for the elements that are in the list.
+- Rename `foldr_cons_permute` into `foldr_cons_permute_strong` and strengthen
+  (a) from function `f : A → A → A` to `f : A → B → B`, and (b) to only require
+  associativity/commutativity for the elements that are in the list.
+- Rename `foldr_cons_permute_eq` into `foldr_cons_permute`.
+- Various improvements to the support of strings:
+  + Add string literal notation "my string" to `std_scope`, and no longer
+    globally open `string_scope`.
+  + Move all definitions and lemmas about strings/ascii into the modules
+    `String`/`Ascii`, i.e., rename `string_rev_app` → `String.rev_app`,
+    `string_rev` → `String.rev`, `is_nat` → `Ascii.is_nat`,
+    `is_space` → `Ascii.is_space` and `words` → `String.words`.
+  + The file `std.strings` no longer exports the `String` module, it only
+    exports the `string` type, its constructors, induction principles, and
+    notations (in `string_scope`). Similar to the number types (`nat`, `N`,
+    `Z`), importing the `String` module yourself is discouraged, rather use
+    `String.function` and `String.lemma`.
+  + Add `String.le` and some theory about it (decidability, proof irrelevance,
+    total order).
+- Add lemmas `foldr_idemp_strong` and `foldr_idemp`.
+- Add lemmas `set_fold_union_strong` and `set_fold_union`.
+- Add lemmas `map_fold_union_strong`, `map_fold_union`,
+  `map_fold_disj_union_strong`, `map_fold_disj_union` and `map_fold_proper`.
+- Add `gmultiset_map` and associated lemmas. (by Marijn van Wezel)
+- Add `CProd` type class for Cartesian products; with instances for `list`,
+  `gset`, `boolset`, `MonadSet` (i.e., `propset`, `listset`); and `set_solver`
+  tactic support. (by Thibaut Pérami)
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# length
+s/\bnil_length\b/length_nil/g
+s/\bcons_length\b/length_cons/g
+s/\bapp_length\b/length_app/g
+s/\bmap_to_list_length\b/length_map_to_list/g
+s/\bseq_length\b/length_seq/g
+s/\bseqZ_length\b/length_seqZ/g
+s/\bjoin_length\b/length_join/g
+s/\bZ_to_little_endian_length\b/length_Z_to_little_endian/g
+s/\balter_length\b/length_alter/g
+s/\binsert_length\b/length_insert/g
+s/\binserts_length\b/length_inserts/g
+s/\breverse_length\b/length_reverse/g
+s/\btake_length\b/length_take/g
+s/\btake_length_le\b/length_take_le/g
+s/\btake_length_ge\b/length_take_ge/g
+s/\bdrop_length\b/length_drop/g
+s/\breplicate_length\b/length_replicate/g
+s/\bresize_length\b/length_resize/g
+s/\brotate_length\b/length_rotate/g
+s/\breshape_length\b/length_reshape/g
+s/\bsublist_alter_length\b/length_sublist_alter/g
+s/\bmask_length\b/length_mask/g
+s/\bfilter_length\b/length_filter/g
+s/\bfilter_length_lt\b/length_filter_lt/g
+s/\bfmap_length\b/length_fmap/g
+s/\bmapM_length\b/length_mapM/g
+s/\bset_mapM_length\b/length_set_mapM/g
+s/\bimap_length\b/length_imap/g
+s/\bzip_with_length\b/length_zip_with/g
+s/\bzip_with_length_l\b/length_zip_with_l/g
+s/\bzip_with_length_l_eq\b/length_zip_with_l_eq/g
+s/\bzip_with_length_r\b/length_zip_with_r/g
+s/\bzip_with_length_r_eq\b/length_zip_with_r_eq/g
+s/\bzip_with_length_same_l\b/length_zip_with_same_l/g
+s/\bzip_with_length_same_r\b/length_zip_with_same_r/g
+s/\bnatset_to_bools_length\b/length_natset_to_bools/g
+s/\bvec_to_list_length\b/length_vec_to_list/g
+s/\bfresh_list_length\b/length_fresh_list/g
+s/\bbv_to_little_endian_length\b/length_bv_to_little_endian/g
+s/\bbv_seq_length\b/length_bv_seq/g
+s/\bbv_to_bits_length\b/length_bv_to_bits/g
+# renaming of minimal_exists
+s/\bminimal_exists_L\b/minimal_exists_elem_of_L/g
+s/\bminimal_exists\b/minimal_exists_elem_of/g
+# map_relation
+s/\bmap_not_Forall2\b/map_not_relation/g
+# map_fold
+s/\bmap_fold_ind2\b/map_fold_weak_ind/g
+# foldr_cons_permute
+s/\bfoldr_cons_permute\b/foldr_cons_permute_strong/g
+s/\bfoldr_cons_permute_eq\b/foldr_cons_permute/g
+# strings
+s/\bstring_rev_app\b/String.rev_app/g
+s/\bstring_rev\b/String.rev/g
+s/\bis_nat\b/Ascii.is_nat/g
+s/\bis_space\b/Ascii.is_space/g
+s/\bwords\b/String.words/g
+EOF
+```
+
+
+## std++ 1.10.0 (2024-04-12)
+
+The highlight of this release is the bitvector library with support for
+fixed-size integers. It is distributed as a separate package,
+`coq-stdpp-bitvector`. The library is developed and maintained by Michael
+Sammler.
+
+std++ 1.10 supports Coq 8.18 and 8.19.
+Coq 8.16 and 8.17 are no longer supported.
+
+This release of std++ was managed by Ralf Jung and Robbert Krebbers, with
+contributions from Mathias Adam Møller, Michael Sammler, Pierre Rousselin,
+Pierre Roux, and Thibaut Pérami. Thanks a lot to everyone involved!
+
+**Detailed list of changes:**
+
+- Add `TCSimpl` type class that is similar to `TCEq` but performs `simpl`
+  before proving the goal by reflexivity.
+- Add new typeclass `MThrow E M` to generally represent throwing an error of
+  type `E` in monad `M`. (by Thibaut Pérami and Mathias Adam Møller)
+  As a consequence:
+  + Replace `MGuard` with `MThrow` and define `guard` in terms of `MThrow`.
+  + The new `guard` is an ordinary function, while the old guard was a notation.
+    Hence, use the monadic bind to compose guards. For example, write
+    `guard P;; m`/`p ← guard P; m` instead of `guard P; m`/`guard P as p; m`.
+  + Replace the tactic `case_option_guard` with a more general `case_guard`
+    version.
+- Equip `solve_proper` with support for subrelations. When the goal is `R x y`
+  and an assumption `R' x y` is found, we search for an instance of
+  `SolveProperSubrelation R' R` and if we find one, that finishes the proof.
+- Remove `wf` alias for the standard `well_founded`.
+- Add lemmas `Nat.lt_wf_0_projected`, `N.lt_wf_0_projected`, `Z.lt_wf_projected`
+  for easy measure/size induction.
+- Add `inv` tactic as a more well-behaved alternative to `inversion_clear`
+  (inspired by CompCert), and `oinv` as its version on open terms.
+  These tactics support both named hypotheses (`inv H`) and using a number
+  to refer to a hypothesis on the goal (`inv 1`).
+- Add `prod_swap : A * B → B * A` and some basic theory about it.
+- Add lemma `join_app`.
+- Allow patterns and type annotations in `propset` notation, e.g.,
+  `{[ (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.
+- 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`.
+  (by Michael Sammler)
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# well_founded
+s/\bwf\b/well_founded/g
+EOF
+```
+
+## std++ 1.9.0 (2023-10-11)
+
+This highlights of this release are:
+* `gmap` and related types are re-implemented based on Appel and Leroy's
+  [Efficient Extensional Binary Tries](https://inria.hal.science/hal-03372247),
+  making them usable in nested inductive definitions and improving
+  extensionality. More information can be found in Robbert Krebbers' Coq
+  Workshop talk, see https://coq-workshop.gitlab.io/2023/
+* New tactics `ospecialize`, `odestruct`, `oinversion` etc are added. These
+  tactics improve upon `efeed` / `edestruct` by allowing one to leave more terms
+  open when specializing arguments. For instance, `odestruct (H _ x)` will turn
+  the `_` into an evar rather than trying to infer it immediately, making it
+  usable in many situations where `edestruct` fails. This can significantly
+  shorten the overhead involved in forward reasoning proofs. For more
+  information, see the test cases provided here:
+  https://gitlab.mpi-sws.org/iris/stdpp/-/blob/master/tests/tactics.v#L114
+
+std++ 1.9 supports Coq 8.16 to 8.18. Coq 8.12 to 8.15 are no longer supported.
+
+This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Johannes
+Hostert, with contributions from Dorian Lesbre, Herman Bergwerf, Ike Mulder,
+Isaak van Bakel, Jan-Oliver Kaiser, Jonas Kastberg, Marijn van Wezel, Michael
+Sammler, Paolo Giarrusso, Tej Chajed, and Thibaut Pérami. Thanks a lot to
+everyone involved!
+
+**Detailed list of changes:**
+
+- Rename `difference_difference` → `difference_difference_l` and
+  `difference_difference_L` → `difference_difference_l_L`, add
+  `difference_difference_r` and `difference_difference_r_L`.
+- Let `set_solver` use `eauto` (instead of `idtac`) as its default solver.
+- Add tactic `tc_solve` (this was `iSolveTC` in Iris).
+- Change `f_equiv` to use `reflexivity` in a way similar to `f_equal`. That is,
+  let `f_equiv` solve goals and subgoals of the form `R x x`. However, we use
+  a restricted `fast_reflexivity` as full `reflexivity` can be quite expensive.
+- Rename `loopup_total_empty` → `lookup_total_empty`.
+- Let `naive_solver tac` fail if `tac` creates new evars. Before it would
+  succeed with a proof that contains unresolved evars/shelved goals.
+- Add lemmas `Nat.mul_reg_{l,r}` for cancellation of multiplication on `nat`.
+  (Names are analogous to the `Z.` lemmas for Coq's standard library.)
+- Rename `map_preimage` into `map_preimg` to be consistent with `dom`.
+- Improve `bijective_finite`: do not require an inverse, do not unnecessarily
+  remove duplicates.
+- Add operation `*:` for "scalar" multiplication of multisets.
+- Add `by` parameter to `multiset_solver`, which defaults to `eauto`.
+- Add `map_img` operator for map image/codomain and some lemmas about it. (by
+  Dorian Lesbre)
+- Remove `Permutation_alt`, `submseteq_Permutation_length_le`, and
+  `submseteq_Permutation_length_eq`; use `submseteq_length_Permutation` instead.
+- Remove `map_to_list_length` (which seemed to be an unneeded auxiliary lemma);
+  use `map_subset_size` instead.
+- Rename `prefix_lookup` → `prefix_lookup_Some`.
+- Extend `set_solver` with support for `set_Forall` and `set_Exists`.
+- Change `lookup_union` lemma statement to use `∪` on maps instead of `union_with`.
+- Add `set_omap` function for finite sets and associated lemmas. (by Dorian
+  Lesbre)
+- Add proof that `vec` is `Finite`. (by Herman Bergwerf.)
+- Add `min` and `max` infix notations for `positive`.
+- Add lemma `map_zip_fst_snd`.
+- Add `stdpp.ssreflect` to provide compatibility with the ssreflect tactics.
+- Set `simpl never` for `Pos` and `N` operations (similar to `Z`).
+- Add `Intersection` instance for `option`. (by Marijn van Wezel)
+- Add `lookup_intersection` lemma for the distributivity of lookup on an
+  intersection. (by Marijn van Wezel)
+- Add lemmas `map_filter_or` and `map_filter_and` for the union and intersection
+  of filters on maps. (by Marijn van Wezel)
+- Set `Hint Mode Equiv !`; this might need some type annotations for ambiguous
+  uses of `≡`.
+- Set `intuition_solver ::= auto` (the default is `auto with *`) instead of
+  redeclaring `intuition`.
+- Rename `option_union_Some` → `union_Some`, and strengthen it to become a
+  biimplication.
+- Provide new implementations of `gmap`/`gset`, `Pmap`/`Pset`, `Nmap`/`Nset` and
+  `Zmap`/`Zset` based on the "canonical" version of binary tries by Appel and
+  Leroy (see https://inria.hal.science/hal-03372247) that avoid the use of Sigma
+  types. This has several benefits:
+  + Maps enjoy more definitional equalities, because they are no longer equipped
+    with a proof of canonicity. This means more equalities can be proved by
+    `reflexivity` or even by conversion as part of unification. For example,
+    `{[ 1 := 1; 2 := 2 ]} = {[ 2 := 2; 1 := 1 ]}` and `{[ 1 ]} ∖ {[ 1 ]} = ∅`
+    hold definitionally.
+  + Maps can be used in nested recursive definitions. For example,
+    `Inductive gtest := GTest : gmap nat gtest → gtest`. (The old map types
+    would violate Coq's strict positivity condition due to the Sigma type.)
+- Make `map_fold` a primitive of the `FinMap`, and derive `map_to_list` from it.
+  (`map_fold` used to be derived from `map_to_list`.) This makes it possible to
+  use `map_fold` in nested-recursive definitions on maps. For example,
+  `Fixpoint f (t : gtest) := let 'GTest ts := t in map_fold (λ _ t', plus (f t')) 1 ts`.
+- Make `fin` number literal notations work with numbers above 10. (by Thibaut
+  Pérami)
+- Bind `fin` type to `fin` scope, so function taking a `fin` as argument will
+  implicitly parse it in `fin` scope. (by Thibaut Pérami)
+- Change premise `Equivalence` into `PreOrder` for `set_fold_proper`.
+- Weaken `Proper` premises of `set_ind`, `set_fold_ind`, `set_fold_proper`. If
+  you use `solve_proper` to solve these premises, no change should be needed. If
+  you use a manual proof, you have to remove some `intros` and/or a `split`.
+- Change `Params` of `lookup` and `lookup_total` from 4 to 5 to disable setoid
+  rewriting in the key argument. If you have `Proper ((=) ==> R ==> S) lookup`,
+  you should change that to `∀ k, Proper (R ==> S) (lookup k)`.
+- Add lemmas for moving functions in and out of fold operations across data
+  structures: new lemmas exist for sets, gmultisets, finite maps, and lists.
+  (by Isaac van Bakel)
+  + For the above structures, added lemmas which allow rewriting between
+    `g (fold f x s)` and `fold f (g x) s` for appropriately-chosen functions
+    `f`, `g` which commute.
+  + For the above structures, add strong versions of the above lemmas that
+    relate `g (fold f x s)` and `fold f (g x) s` by any preorder respected by
+    `f`, `g` restricted to the elements of `s`.
+  + Add `gmultiset_set_fold_disj_union_strong`, which generalizes
+    `gmultiset_set_fold_disj_union` to any preorder for appropriately-chosen
+    fold functions.
+- Improve efficiency of `encode`/`decode` for `string` and `ascii`.
+- Rename `equiv_Forall2` → `list_equiv_Forall2` and `equiv_option_Forall2` →
+  `option_equiv_Forall2`. Add similar lemmas `list_eq_Forall2` and
+  `option_eq_Forall2` for `=` instead of `≡`.
+- Rename `fmap_inj` → `list_fmap_eq_inj` and `option_fmap_inj` →
+  `option_fmap_eq_inj`. The new lemmas `list_fmap_inj`/`option_fmap_inj`
+  generalize injectivity to `Forall2`/`option_Forall2`.
+- Generalize `set_map`, `set_bind`, `set_omap`, `map_to_set` and `map_img`
+  lemmas from `Set_` to `SemiSet`.
+- Rename `sub_add'` to `add_sub'` for consistency with Coq's `add_sub` lemma.
+- Rename `map_filter_lookup` → `map_lookup_filter` and
+  `map_filter_lookup_Some` → `map_lookup_filter_Some` and
+  `map_filter_lookup_None` → `map_lookup_filter_None`.
+- Add `map_compose` operation, notation `m ∘ₘ n`, and associated lemmas.
+  (by Dorian Lesbre)
+- Add `Assoc`, `Comm`, `LeftId`, `RightId`, `LeftAbsorb`, `RightAbsorb`
+  instances for number types.
+- Add tactics `odestruct`, `oinversion`, `opose proof`, `ospecialize`,
+  `ogeneralize` that work with open terms. All `_` remaining after inference
+  will be turned into evars or subgoals using the same heuristic as `refine`.
+  For instance, with `H: ∀ n, P n → Q n`, `ospecialize (H _ _)` will create an
+  evar for `n` and open a subgoal for `P ?n`. `odestruct` is a more powerful
+  version of `edestruct` that does not require all `_` in the destructed term to
+  be immediately inferred.
+- Replace `feed`/`efeed` tactics by variants of the `o` tactics that
+  automatically add extra `_` until there are no more leading `∀`/`→`. `efeed
+  tac` becomes `otac*`; the `feed` variants (that only specialize `→` but not
+  `∀`) are no longer provided.
+- Add lemmas for `reverse` of `take`/`drop` and `take`/`drop` of `reverse`.
+- Rework lemmas for `take`/`drop` of an `++`:
+  + Add `take_app` and `drop_app`, which are the strongest versions, and use
+    `take_app_X` for derived versions.
+  + Consistently use `'` suffix for version with premise `n = length`, and have
+    versions without `'` with `length` inlined.
+  + Rename `take_app` → `take_app_length`, `take_app_alt` → `take_app_length'`,
+    `take_add_app` → `take_app_add'`, `take_app3_alt` → `take_app3_length'`,
+    `drop_app` → `drop_app_length`, `drop_app_alt` → `drop_app_length'`,
+    `drop_add_app` → `drop_app_add'`, `drop_app3_alt` → `drop_app3_length'`.
+- Add instance `cons_equiv_inj`.
+
+**Changes in `stdpp_unstable`:**
+
+- Add bitvector number literal notations. (by Thibaut Pérami)
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+s/\bdifference_difference(|_L)\b/difference_difference_l\1/g
+s/\bloopup_total_empty\b/lookup_total_empty/g
+# map_preimg
+s/\bmap_preimage/map_preimg/g
+s/\blookup_preimage/lookup_preimg/g
+s/\blookup_total_preimage/lookup_total_preimg/g
+# union_Some
+s/\boption_union_Some\b/union_Some/g
+# prefix_lookup
+s/\bprefix_lookup\b/prefix_lookup_Some/g
+# Forall2
+s/\bequiv_Forall2\b/list_equiv_Forall2/g
+s/\bequiv_option_Forall2\b/option_equiv_Forall2/g
+s/\bfmap_inj\b/list_fmap_eq_inj/g
+s/\boption_fmap_inj\b/option_fmap_eq_inj/g
+# add_sub
+s/\bsub_add'\b/add_sub'/g
+# map filter
+s/\bmap_filter_lookup/map_lookup_filter/g
+# take/drop app
+s/\b(take|drop)_app\b/\1_app_length/g
+s/\b(take|drop)_app_alt\b/\1_app_length'/g
+s/\b(take|drop)_add_app\b/\1_app_add'/g
+s/\b(take|drop)_app3_alt\b/\1_app3_length'/g
+EOF
+```
+
+## std++ 1.8.0 (2022-08-18)
+
+Coq 8.16 is newly supported by this release, and Coq 8.12 to 8.15 remain
+supported. Coq 8.11 is no longer supported.
+
+This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Lennard
+Gäher, with contributions from Andrej Dudenhefner, Dan Frumin, Gregory Malecha,
+Jan-Oliver Kaiser, Lennard Gäher, Léo Stefanesco, Michael Sammler, Paolo G. Giarrusso,
+Ralf Jung, Robbert Krebbers, and Vincent Siles. Thanks a lot to everyone involved!
+
+- Make sure that `gset` and `mapset` do not bump the universe.
+- Rewrite `tele_arg` to make it not bump universes. (by Gregory Malecha, BedRock
+  Systems)
+- Change `dom D M` (where `D` is the domain type) to `dom M`; the domain type is
+  now inferred automatically. To make this possible, getting the domain of a
+  `gmap` as a `coGset` and of a `Pmap` as a `coPset` is no longer supported. Use
+  `gset_to_coGset`/`Pset_to_coPset` instead.
+  When combining `dom` with `≡`, this can run into an old issue (due to a Coq
+  issue, `Equiv` does not the desired `Hint Mode !`), which can make it
+  necessary to annotate the set type at the `≡` via `≡@{D}`.
+- Rename "unsealing" lemmas from `_eq` to `_unseal`. This affects `ndot_eq` and
+  `nclose_eq`. These unsealing lemmas are internal, so in principle you should
+  not rely on them.
+- Declare `Hint Mode` for `FinSet A C` so that `C` is input, and `A` is output
+  (i.e., inferred from `C`).
+- Add function `map_preimage` to compute the preimage of a finite map.
+- Rename `map_disjoint_subseteq` → `kmap_subseteq` and
+  `map_disjoint_subset` → `kmap_subset`.
+- Add `map_Exists` as an analogue to `map_Forall`. (by Michael Sammler)
+- Add `case_match eqn:H` that behaves like `case_match` but allows naming the
+  generated equality. (by Michael Sammler)
+- Flip direction of `map_disjoint_fmap`.
+- Add `map_agree` as a weaker version of `##ₘ` which requires the maps to agree
+  on keys contained in both maps. (by Michael Sammler)
+- Rename `lookup_union_l` → `lookup_union_l'` and add `lookup_union_l`
+  as the dual to `lookup_union_r`.
+- Add `map_seqZ` as the `Z` analogue of `map_seq`. (by Michael Sammler)
+- Add the `coq-stdpp-unstable` package for libraries that are not
+  deemed stable enough to be included in the main std++ library,
+  following the `coq-iris-unstable` package. This library is contained
+  in the `stdpp_unstable` folder. The `theories` folder was renamed
+  to `stdpp`.
+- Add an unstable `bitblast` tactic for solving equalities between integers
+  involving bitwise operations. (by Michael Sammler)
+- Add the bind operation `set_bind` for finite sets. (by Dan Frumin and Paolo G.
+  Giarrusso)
+- Change `list_fmap_ext` and `list_fmap_equiv_ext` to require equality on the
+  elements of the list, not on all elements of the carrier type. This change
+  makes these lemmas consistent with those for maps.
+- Use the modules `Nat`, `Pos`, `N`, `Z`, `Nat2Z`, `Z2Nat`, `Nat2N`, `Pos2Nat`,
+  `SuccNat2Pos`, and `N2Z` for our extended results on number types. Before,
+  we prefixed our the std++ lemmas with `Nat_` or `nat_`, but now you refer
+  to them with `Nat.`, similar to the way you refer to number lemmas from Coq's
+  standard library.
+- Use a module `Qp` for our positive rationals library. You now refer to `Qp`
+  lemmas using `Qp.lem` instead of `Qp_lem`.
+- Rename `_plus`/`_minus` into `_add`/`_sub` to be consistent with Coq's current
+  convention for numbers. See the sed script below for an exact list of renames.
+- Refactor the `feed` and `efeed` tactics. In particular, improve the
+  documentation of `(e)feed` tactics, rename the primitive `(e)feed`
+  tactic to `(e)feed_core`, make the syntax of `feed_core` consistent
+  with `efeed_core`, remove the `by` parameter of `efeed_core`, and add
+  `(e)feed generalize`, `efeed inversion`, and `efeed destruct`.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+s/\bmap_disjoint_subseteq\b/kmap_subseteq/g
+s/\bmap_disjoint_subset\b/kmap_subset/g
+s/\blookup_union_l\b/lookup_union_l'/g
+# number modules --- note that this might rename your own lemmas
+# start with Nat_/N_/Z_/Qp_/P(app|reverse|length|dup)_ too eagerly.
+# Also the list of names starting with nat_ is not complete.
+s/\bNat_/Nat\./g
+s/\bNat.iter_S(|_r)\b/Nat.iter_succ\1/g
+s/\bP(app|reverse|length|dup)/Pos\.\1/g
+s/\bPlt_sum\b/Pos\.lt_sum/g
+s/\bPos\.reverse_Pdup\b/Pos\.reverse_Pdup/g
+s/\bnat_(le_sum|eq_dec|lt_pi)\b/Nat\.\1/g
+s/\bN_/N\./g
+s/\bZ_/Z\./g
+s/\bZ\.scope\b/Z_scope/g
+s/\bN\.scope\b/N_scope/g
+s/\Z\.of_nat_complete\b/Z_of_nat_complete/g
+s/\bZ\.of_nat_inj\b/Nat2Z.inj/g
+s/\bZ2Nat_/Z2Nat\./g
+s/\bNat2Z_/Nat2Z\./g
+s/\bQp_/Qp\./g
+s/\bQp\.1_1/Qp\.add_1_1/g
+# plus → add
+s/\bfin_plus_inv\b/fin_add_inv/g
+s/\bfin_plus_inv_L\b/fin_add_inv_l/g
+s/\bfin_plus_inv_R\b/fin_add_inv_r/g
+s/\bset_seq_plus\b/set_seq_add/g
+s/\bset_seq_plus_L\b/set_seq_add_L/g
+s/\bset_seq_plus_disjoint\b/set_seq_add_disjoint/g
+s/\bnsteps_plus_inv\b/nsteps_add_inv/g
+s/\bbsteps_plus_r\b/bsteps_add_r/g
+s/\bbsteps_plus_l\b/bsteps_add_l/g
+s/\btake_plus_app\b/take_add_app/g
+s/\breplicate_plus\b/replicate_add/g
+s/\btake_replicate_plus\b/take_replicate_add/g
+s/\bdrop_replicate_plus\b/drop_replicate_add/g
+s/\bresize_plus\b/resize_add/g
+s/\bresize_plus_eq\b/resize_add_eq/g
+s/\btake_resize_plus\b/take_resize_add/g
+s/\bdrop_resize_plus\b/drop_resize_add/g
+s/\bdrop_plus_app\b/drop_add_app/g
+s/\bMakeNatPlus\b/MakeNatAdd/g
+s/\bmake_nat_plus\b/make_nat_add/g
+s/\bnat_minus_plus\b/Nat\.sub_add/g
+s/\bnat_le_plus_minus\b/Nat\.le_add_sub/g
+EOF
+```
+
+## std++ 1.7.0 (2022-01-22)
+
+Coq 8.15 is newly supported by this release, and Coq 8.11 to 8.14 remain
+supported. Coq 8.10 is no longer supported.
+
+This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Tej
+Chajed, with contributions from Glen Mével, Jonas Kastberg Hinrichsen, Matthieu
+Sozeau, Michael Sammler, Ralf Jung, Robbert Krebbers, and Tej Chajed. Thanks a
+lot to everyone involved!
+
+- Add `is_closed_term` tactic for determining whether a term depends on variables bound
+  in the context. (by Michael Sammler)
+- Add `list.zip_with_take_both` and `list.zip_with_take_both'`
+- Specialize `list.zip_with_take_{l,r}`, add generalized lemmas `list.zip_with_take_{l,r}'`
+- Add `bool_to_Z` that converts true to 1 and false to 0. (by Michael Sammler)
+- Add lemmas for lookup on `mjoin` for lists. (by Michael Sammler)
+- Rename `Is_true_false` → `Is_true_false_2` and `eq_None_ne_Some` → `eq_None_ne_Some_1`.
+- Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext`.
+- Remove a spurious `Global Arguments Pos.of_nat : simpl never`.
+- Add tactics `destruct select <pat>` and `destruct select <pat> as <intro_pat>`.
+- Add some more lemmas about `Finite` and `pred_finite`.
+- Add lemmas about `last`: `last_app_cons`, `last_app`, `last_Some`, and
+  `last_Some_elem_of`.
+- Add versions of Pigeonhole principle for Finite types, natural numbers, and
+  lists.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+s/\bIs_true_false\b/Is_true_false_2/g
+s/\beq_None_ne_Some\b/eq_None_ne_Some_1/g
+# bool decide
+s/\b(bool_|)decide_iff\b/\1decide_ext/g
+EOF
+```
+
+## std++ 1.6.0 (2021-11-05)
+
+Coq 8.14 is newly supported by this release, and Coq 8.10 to 8.13 remain
+supported.
+
+This release of std++ was managed by Ralf Jung, Robbert Krebbers, and Tej
+Chajed, with contributions from Alix Trieu, Andrej Dudenhefner, Dan Frumin,
+Fengmin Zhu, Hoang-Hai Dang, Jan Menz, Lennard Gäher, Michael Sammler, Paolo G.
+Giarrusso, Ralf Jung, Robbert Krebbers, Simon Friis Vindum, Simon Gregersen, and
+Tej Chajed. Thanks a lot to everyone involved!
+
+- Remove singleton notations `{[ x,y ]}` and `{[ x,y,z ]}` for `{[ (x,y) ]}`
+  and `{[ (x,y,z) ]}`. They date back to the time we used the `singleton` class
+  with a product for maps (there's now the `singletonM` class).
+- Add map notations `{[ k1 := x1 ; .. ; kn := xn ]}` up to arity 13.
+  (by Lennard Gäher)
+- Add multiset literal notation `{[+ x1; .. ; xn +]}`.
+  + Add a new type class `SingletonMS` (with projection `{[+ x +]}` for
+    multiset singletons.
+  + Define `{[+ x1; .. ; xn +]}` as notation for `{[+ x1 +]} ⊎ .. ⊎ {[+ xn +]}`.
+- Remove the `Singleton` and `Semiset` instances for multisets to avoid
+  accidental use.
+  + This means the notation `{[ x1; .. ; xn ]}` no longer works for multisets
+    (previously, its definition was wrong, since it used `∪` instead of `⊎`).
+  + Add lemmas for `∈` and `∉` specific for multisets, since the set lemmas no
+    longer work for multisets.
+- Make `Qc_of_Z'` not an implicit coercion (from `Z` to `Qc`) any more.
+- Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
+- Rename `decide_left` → `decide_True_pi` and `decide_right` → `decide_False_pi`.
+- Add `option_guard_True_pi`.
+- Add lemma `surjective_finite`. (by Alix Trieu)
+- Add type classes `TCFalse`, `TCUnless`, `TCExists`, and `TCFastDone`. (by
+  Michael Sammler)
+- Add various results about bit representations of `Z`. (by Michael Sammler)
+- Add tactic `learn_hyp`. (by Michael Sammler)
+- Add `Countable` instance for decidable Sigma types. (by Simon Gregersen)
+- Add tactics `compute_done` and `compute_by` for solving goals by computation.
+- Add `Inj` instances for `fmap` on option and maps.
+- Various changes to `Permutation` lemmas:
+  + Rename `Permutation_nil` → `Permutation_nil_r`,
+    `Permutation_singleton` → `Permutation_singleton_r`, and
+    `Permutation_cons_inv` → `Permutation_cons_inv_r`.
+  + Add lemmas `Permutation_nil_l`, `Permutation_singleton_l`, and
+    `Permutation_cons_inv_l`.
+  + Add new instance `cons_Permutation_inj_l : Inj (=) (≡ₚ) (.:: k).`.
+  + Add lemma `Permutation_cross_split`.
+  + Make lemma `elem_of_Permutation` a biimplication
+- Add function `kmap` to transform the keys of finite maps.
+- Set `Hint Mode` for the classes `PartialOrder`, `TotalOrder`, `MRet`, `MBind`,
+  `MJoin`, `FMap`, `OMap`, `MGuard`, `SemiSet`, `Set_`, `TopSet`, and `Infinite`.
+- Strengthen the extensionality lemmas `map_filter_ext` and
+  `map_filter_strong_ext`:
+  + Rename `map_filter_strong_ext` → `map_filter_strong_ext_1` and
+    `map_filter_ext` → `map_filter_ext_1`.
+  + Add new bidirectional lemmas `map_filter_strong_ext` and `map_filter_ext`.
+  + Add `map_filter_strong_ext_2` and `map_filter_ext_2`.
+- Make collection of lemmas for filter + union/disjoint consistent for sets and
+  maps:
+  + Sets: Add lemmas `disjoint_filter`, `disjoint_filter_complement`, and
+    `filter_union_complement`.
+  + Maps: Rename `map_disjoint_filter` → `map_disjoint_filter_complement` and
+    `map_union_filter` → `map_filter_union_complement` to be consistent with sets.
+  + Maps: Add lemmas `map_disjoint_filter` and `map_filter_union` analogous to
+    sets.
+- Add cross split lemma `map_cross_split` for maps
+- Setoid results for options:
+  + Add instance `option_fmap_equiv_inj`.
+  + Add `Proper` instances for `union`, `union_with`, `intersection_with`, and
+    `difference_with`.
+  + Rename instances `option_mbind_proper` → `option_bind_proper` and
+    `option_mjoin_proper` → `option_join_proper` to be consistent with similar
+    instances for sets and lists.
+  + Rename `equiv_None` → `None_equiv_eq`.
+  + Replace `equiv_Some_inv_l`, `equiv_Some_inv_r`, `equiv_Some_inv_l'`, and
+    `equiv_Some_inv_r'` by new lemma `Some_equiv_eq` that follows the pattern of
+    other `≡`-inversion lemmas: it uses a `↔` and puts the arguments of `≡` and
+    `=` in consistent order.
+- Setoid results for lists:
+  + Add `≡`-inversion lemmas `nil_equiv_eq`, `cons_equiv_eq`,
+    `list_singleton_equiv_eq`,  and `app_equiv_eq`.
+  + Add lemmas `Permutation_equiv` and `equiv_Permutation`.
+- Setoid results for maps:
+  + Add instances `map_singleton_equiv_inj` and `map_fmap_equiv_inj`.
+  + Add and generalize many `Proper` instances.
+  + Add lemma `map_equiv_lookup_r`.
+  + Add lemma `map_equiv_iff`.
+  + Rename `map_equiv_empty` → `map_empty_equiv_eq`.
+  + Add `≡`-inversion lemmas `insert_equiv_eq`, `delete_equiv_eq`,
+    `map_union_equiv_eq`, etc.
+- Drop `DiagNone` precondition of `lookup_merge` rule of `FinMap` interface.
+  + Drop `DiagNone` class.
+  + Add `merge_proper` instance.
+  + Simplify lemmas about `merge` by dropping the `DiagNone` precondition.
+  + Generalize lemmas `partial_alter_merge`, `partial_alter_merge_l`, and
+    `partial_alter_merge_r`.
+  + Drop unused `merge_assoc'` instance.
+- Improvements to `head` and `tail` functions for lists:
+  + Define `head` as notation that prints (Coq defines it as `parsing only`)
+    similar to `tail`.
+  + Declare `tail` as `simpl nomatch`.
+  + Add lemmas about `head` and `tail`.
+- Add and extend equivalences between closure operators:
+  - Add `↔` lemmas that relate `rtc`, `tc`, `nsteps`, and `bsteps`.
+  - Rename `→` lemmas `rtc_nsteps` → `rtc_nsteps_1`,
+    `nsteps_rtc` → `rtc_nsteps_2`, `rtc_bsteps` → `rtc_bsteps_1`, and
+    `bsteps_rtc` → `rtc_bsteps_2`.
+  - Add lemmas that relate `rtc`, `tc`, `nsteps`, and `bsteps` to path
+    representations as lists.
+- Remove explicit equality from cross split lemmas so that they become easier
+  to use in forward-style proofs.
+- Add lemmas for finite maps: `dom_map_zip_with`, `dom_map_zip_with_L`,
+  `map_filter_id`, `map_filter_subseteq`, and `map_lookup_zip_Some`.
+- Add lemmas for sets: `elem_of_weaken` and `not_elem_of_weaken`.
+- Rename `insert_delete` → `insert_delete_insert`; add new `insert_delete` that
+  is consistent with `delete_insert`.
+- Fix statement of `sum_inhabited_r`. (by Paolo G. Giarrusso)
+- Make `done` work on goals of the form `is_Some`.
+- Add `mk_evar` tactic to generate evars (intended as a more useful replacement
+  for Coq's `evar` tactic).
+- Make `solve_ndisj` able to solve more goals of the form `_ ⊆ ⊤ ∖ _`,
+  `_ ∖ _ ## _`, `_ ## _ ∖ _`, as well as `_ ## ∅` and `∅ ## _`,
+  and goals containing `_ ∖ _ ∖ _`.
+- Improvements to curry:
+  + Swap names of `curry`/`uncurry`, `curry3`/`uncurry3`, `curry4`/`uncurry4`,
+    `gmap_curry`/`gmap_uncurry`, and `hcurry`/`huncurry` to be consistent with
+    Haskell and friends.
+  + Add `Params` and `Proper` instances for `curry`/`uncurry`,
+    `curry3`/`uncurry3`, and `curry4`/`uncurry4`.
+  + Add lemmas that say that `curry`/`curry3`/`curry4` and
+    `uncurry`/`uncurry3`/`uncurry4` are inverses.
+- Rename `map_union_subseteq_l_alt` → `map_union_subseteq_l'` and
+  `map_union_subseteq_r_alt` → `map_union_subseteq_r'` to be consistent with
+  `or_intro_{l,r}'`.
+- Add `union_subseteq_l'`, `union_subseteq_r'` as transitive versions of
+  `union_subseteq_l`, `union_subseteq_r` that can be more easily `apply`ed.
+- Rename `gmultiset_elem_of_singleton_subseteq` → `gmultiset_singleton_subseteq_l`
+  and swap the equivalence to be consistent with Iris's `singleton_included_l`. Add
+  `gmultiset_singleton_subseteq`, which is similar to `singleton_included` in
+  Iris.
+- Add lemmas `singleton_subseteq_l` and `singleton_subseteq` for sets.
+- Add lemmas `map_singleton_subseteq_l` and `map_singleton_subseteq` for maps.
+- Add lemmas `singleton_submseteq_l` and `singleton_submseteq` for unordered
+  list inclusion, as well as `lookup_submseteq` and `submseteq_insert`.
+- Make `map_empty` a biimplication.
+- Clean up `empty{',_inv,_iff}` lemmas:
+  + Write them all using `↔` and consistently use the `_iff` suffix.
+    (But keep the `_inv` version when it is useful for rewriting.)
+  + Remove `map_to_list_empty_inv_alt`; chain `Permutation_nil_r` and
+    `map_to_list_empty_iff` instead.
+  + Add lemma `map_filter_empty_iff`.
+- Add generalized lemma `map_filter_insert` that covers both the True and False
+  case. Rename old `map_filter_insert` → `map_filter_insert_True` and
+  `map_filter_insert_not_delete` → `map_filter_insert_False`.
+- Weaken premise of `map_filter_delete_not` to make it consistent with
+  `map_filter_insert_not'`.
+- Add lemmas for maps: `map_filter_strong_subseteq_ext`, `map_filter_subseteq_ext`,
+  `map_filter_subseteq_mono`, `map_filter_singleton`, `map_filter_singleton_True`,
+  `map_filter_singleton_False`, `map_filter_comm`, `map_union_least`,
+  `map_subseteq_difference_l`, `insert_difference`, `insert_difference'`,
+  `difference_insert`, `difference_insert_subseteq`. (by Hai Dang)
+- Add `map_size_disj_union`, `size_dom`, `size_list_to_set`.
+- Tweak reduction on `gset`, so that `cbn` matches the behavior by `simpl` and
+  does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
+- Add `get_head` tactic to determine the syntactic head of a function
+  application term.
+- Add map lookup lemmas: `lookup_union_is_Some`, `lookup_difference_is_Some`,
+  `lookup_union_Some_l_inv`, `lookup_union_Some_r_inv`.
+- Make `Forall2_nil`, `Forall2_cons` bidirectional lemmas with `Forall2_nil_2`,
+  `Forall2_cons_2` being the original one-directional versions (matching
+  `Forall_nil` and `Forall_cons`). Rename `Forall2_cons_inv` to `Forall2_cons_1`.
+- Enable `f_equiv` (and by extension `solve_proper`) to handle goals of the form
+  `f x ≡ g x` when `f ≡ g` is in scope, where `f` has a type like Iris's `-d>`
+  and `-n>`.
+- Optimize `f_equiv` by doing more syntactic checking before handing off to
+  unification. This can make some uses 50x faster, but also makes the tactic
+  slightly weaker in case the left-hand side and right-hand side of the relation
+  call a function with arguments that are convertible but not syntactically
+  equal.
+- Add lemma `choose_proper` showing that `choose P` respects predicate
+  equivalence. (by Paolo G. Giarrusso, BedRock Systems)
+- Extract module `well_founded` from `relations`, and re-export it for
+  compatibility. This contains `wf`, `Acc_impl`, `wf_guard`,
+  `wf_projected`, `Fix_F_proper`, `Fix_unfold_rel`.
+- Add induction principle `well_founded.Acc_dep_ind`, a dependent
+  version of `Acc_ind`. (by Paolo G. Giarrusso, BedRock Systems)
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+s/\bdecide_left\b/decide_True_pi/g
+s/\bdecide_right\b/decide_False_pi/g
+# Permutation
+s/\bPermutation_nil\b/Permutation_nil_r/g
+s/\bPermutation_singleton\b/Permutation_singleton_r/g
+s/\Permutation_cons_inv\b/Permutation_cons_inv_r/g
+# Filter
+s/\bmap_disjoint_filter\b/map_disjoint_filter_complement/g
+s/\bmap_union_filter\b/map_filter_union_complement/g
+# mbind
+s/\boption_mbind_proper\b/option_bind_proper/g
+s/\boption_mjoin_proper\b/option_join_proper/g
+# relations
+s/\brtc_nsteps\b/rtc_nsteps_1/g
+s/\bnsteps_rtc\b/rtc_nsteps_2/g
+s/\brtc_bsteps\b/rtc_bsteps_1/g
+s/\bbsteps_rtc\b/rtc_bsteps_2/g
+# setoid
+s/\bequiv_None\b/None_equiv_eq/g
+s/\bmap_equiv_empty\b/map_empty_equiv_eq/g
+# insert_delete
+s/\binsert_delete\b/insert_delete_insert/g
+# filter extensionality lemmas
+s/\bmap_filter_ext\b/map_filter_ext_1/g
+s/\bmap_filter_strong_ext\b/map_filter_strong_ext_1/g
+# swap curry/uncurry
+s/\b(lookup_gmap_|gmap_|h|)curry(|3|4)\b/OLD\1curry\2/g
+s/\b(lookup_gmap_|gmap_|h|)uncurry(|3|4)\b/\1curry\2/g
+s/\bOLD(lookup_gmap_|gmap_|h|)curry(|3|4)\b/\1uncurry\2/g
+s/\bgmap_curry_uncurry\b/gmap_uncurry_curry/g
+s/\bgmap_uncurry_non_empty\b/gmap_curry_non_empty/g
+s/\bgmap_uncurry_curry_non_empty\b/gmap_curry_uncurry_non_empty/g
+s/\bhcurry_uncurry\b/huncurry_curry/g
+s/\blookup_gmap_uncurry_None\b/lookup_gmap_curry_None/g
+# map_union_subseteq
+s/\bmap_union_subseteq_(r|l)_alt\b/map_union_subseteq_\1'/g
+# singleton
+s/\bgmultiset_elem_of_singleton_subseteq\b/gmultiset_singleton_subseteq_l/g
+# empty_iff
+s/\bmap_to_list_empty('|_inv)\b/map_to_list_empty_iff/g
+s/\bkmap_empty_inv\b/kmap_empty_iff/g
+s/\belements_empty'\b/elements_empty_iff/g
+s/\bgmultiset_elements_empty'\b/gmultiset_elements_empty_iff/g
+# map_filter_insert
+s/\bmap_filter_insert\b/map_filter_insert_True/g
+s/\bmap_filter_insert_not_delete\b/map_filter_insert_False/g
+# Forall2
+s/\bForall2_cons_inv\b/Forall2_cons_1/g
+EOF
+```
+
+## std++ 1.5.0 (2021-02-16)
+
+Coq 8.13 is newly supported by this release, Coq 8.8 and 8.9 are no longer
+supported.
+
+This release of std++ was managed by Ralf Jung and Robbert Krebbers, with
+contributions by Alix Trieu, Dan Frumin, Hugo Herbelin, Paulo Emílio de Vilhena,
+Simon Friis Vindum, and Tej Chajed.  Thanks a lot to everyone involved!
+
+- Overhaul of the theory of positive rationals `Qp`:
+  + Add `max` and `min` operations for `Qp`.
+  + Add the orders `Qp_le` and `Qp_lt`.
+  + Rename `Qp_plus` into `Qp_add` and `Qp_mult` into `Qp_mul` to be consistent
+    with the corresponding names for `nat`, `N`, and `Z`.
+  + Add a function `Qp_inv` for the multiplicative inverse.
+  + Define the division function `Qp_div` in terms of `Qp_inv`, and generalize
+    the second argument from `positive` to `Qp`.
+  + Add a function `pos_to_Qp` that converts a `positive` into a positive
+    rational `Qp`.
+  + Add many lemmas and missing type class instances, especially for orders,
+    multiplication, multiplicative inverse, division, and the conversion.
+  + Remove the coercion from `Qp` to `Qc`. This follows our recent tradition of
+    getting rid of coercions since they are more often confusing than useful.
+  + Rename the conversion from `Qp_car : Qp → Qc` into `Qp_to_Qc` to be
+    consistent with other conversion functions in std++. Also rename the lemma
+    `Qp_eq` into `Qp_to_Qc_inj_iff`.
+  + Use `let '(..) = ...` in the definitions of `Qp_plus`, `Qp_mult`, `Qp_inv`,
+    `Qp_le` and `Qp_lt` to avoid Coq tactics (like `injection`) to unfold these
+    definitions eagerly.
+  + Define the `Qp` literals 1, 2, 3, 4 in terms of `pos_to_Qp` instead of
+    iterated addition.
+  + Rename and restate many lemmas so as to be consistent with the conventions
+    for Coq's number types `nat`, `N`, and `Z`.
+- Add `rename select <pat> into <name>` tactic to find a hypothesis by pattern
+  and give it a fixed name.
+- Add `eunify` tactic that lifts Coq's `unify` tactic to `open_constr`.
+- Generalize `omap_insert`, `omap_singleton`, `map_size_insert`, and
+  `map_size_delete` to cover the `Some` and `None` case. Add `_Some` and `_None`
+  versions of the lemmas for the specific cases.
+- Rename `dom_map filter` → `dom_filter`, `dom_map_filter_L` → `dom_filter_L`,
+  and `dom_map_filter_subseteq` → `dom_filter_subseteq` for consistency's sake.
+- Remove unused notations `∪**`, `∪*∪**`, `∖**`, `∖*∖**`, `⊆**`, `⊆1*`, `⊆2*`,
+  `⊆1**`, `⊆2**"`, `##**`, `##1*`, `##2*`, `##1**`, `##2**` for nested
+  `zip_with` and `Forall2` versions of `∪`, `∖`, and `##`.
+- Remove unused type classes `DisjointE`, `DisjointList`, `LookupE`, and
+  `InsertE`.
+- Fix a bug where `pretty 0` was defined as `""`, the empty string. It now
+  returns `"0"` for `N`, `Z`, and `nat`.
+- Remove duplicate `map_fmap_empty` of `fmap_empty`, and rename
+  `map_fmap_empty_inv` into `fmap_empty_inv` for consistency's sake.
+- Rename `seq_S_end_app` to `seq_S`. (The lemma `seq_S` is also in Coq's stdlib
+  since Coq 8.12.)
+- Remove `omega` import and hint database in `tactics` file.
+- Remove unused `find_pat` tactic that was made mostly obsolete by `select`.
+- Rename `_11` and `_12` into `_1_1` and `_1_2`, respectively. These suffixes
+  are used for `A → B1` and `A → B2` variants of `A ↔ B1 ∧ B2` lemmas.
+- Rename `Forall_Forall2` → `Forall_Forall2_diag` to be consistent with the
+  names for big operators in Iris.
+- Rename set equality and equivalence lemmas:
+  `elem_of_equiv_L` → `set_eq`,
+  `set_equiv_spec_L` → `set_eq_subseteq`,
+  `elem_of_equiv` → `set_equiv`,
+  `set_equiv_spec` → `set_equiv_subseteq`.
+- Remove lemmas `map_filter_iff` and `map_filter_lookup_eq` in favor of the stronger
+  extensionality lemmas `map_filter_ext` and `map_filter_strong_ext`.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
+```
+sed -i -E '
+s/\bQp_plus\b/Qp_add/g
+s/\bQp_mult\b/Qp_mul/g
+s/\bQp_mult_1_l\b/Qp_mul_1_l/g
+s/\bQp_mult_1_r\b/Qp_mul_1_r/g
+s/\bQp_plus_id_free\b/Qp_add_id_free/g
+s/\bQp_not_plus_ge\b/Qp_not_add_le_l/g
+s/\bQp_le_plus_l\b/Qp_le_add_l/g
+s/\bQp_mult_plus_distr_l\b/Qp_mul_add_distr_r/g
+s/\bQp_mult_plus_distr_r\b/Qp_mul_add_distr_l/g
+s/\bmap_fmap_empty\b/fmap_empty/g
+s/\bmap_fmap_empty_inv\b/fmap_empty_inv/g
+s/\bseq_S_end_app\b/seq_S/g
+s/\bomap_insert\b/omap_insert_Some/g
+s/\bomap_singleton\b/omap_singleton_Some/g
+s/\bomap_size_insert\b/map_size_insert_None/g
+s/\bomap_size_delete\b/map_size_delete_Some/g
+s/\bNoDup_cons_11\b/NoDup_cons_1_1/g
+s/\bNoDup_cons_12\b/NoDup_cons_1_2/g
+s/\bmap_filter_lookup_Some_11\b/map_filter_lookup_Some_1_1/g
+s/\bmap_filter_lookup_Some_12\b/map_filter_lookup_Some_1_2/g
+s/\bmap_Forall_insert_11\b/map_Forall_insert_1_1/g
+s/\bmap_Forall_insert_12\b/map_Forall_insert_1_2/g
+s/\bmap_Forall_union_11\b/map_Forall_union_1_1/g
+s/\bmap_Forall_union_12\b/map_Forall_union_1_2/g
+s/\bForall_Forall2\b/Forall_Forall2_diag/g
+s/\belem_of_equiv_L\b/set_eq/g
+s/\bset_equiv_spec_L\b/set_eq_subseteq/g
+s/\belem_of_equiv\b/set_equiv/g
+s/\bset_equiv_spec\b/set_equiv_subseteq/g
+' $(find theories -name "*.v")
+```
+
+## std++ 1.4.0 (released 2020-07-15)
+
+Coq 8.12 is newly supported by this release, and Coq 8.7 is no longer supported.
+
+This release of std++ received contributions by Gregory Malecha, Michael
+Sammler, Olivier Laurent, Paolo G. Giarrusso, Ralf Jung, Robbert Krebbers,
+sarahzrf, and Tej Chajed.
 
 - Rename `Z2Nat_inj_div` and `Z2Nat_inj_mod` to `Nat2Z_inj_div` and
   `Nat2Z_inj_mod` to follow the naming convention of `Nat2Z` and
-  `Z2Nat`. The names `Z2Nat_inj_div` and `Z2Nat_inj_mod` have been
-  repurposed for be the lemmas they should actually be.
-- Added `rotate` and `rotate_take` functions for accessing a list with
-  wrap-around. Also added `rotate_nat_add` and `rotate_nat_sub` for
+  `Z2Nat`. Re-purpose the names `Z2Nat_inj_div` and `Z2Nat_inj_mod` for be the
+  lemmas they should actually be.
+- Add `rotate` and `rotate_take` functions for accessing a list with
+  wrap-around. Also add `rotate_nat_add` and `rotate_nat_sub` for
   computing indicies into a rotated list.
-- Added the `select` and `revert select` tactics for selecting and
+- Add the `select` and `revert select` tactics for selecting and
   reverting a hypothesis based on a pattern.
-- Extracted `list_numbers.v` from `list.v` and `numbers.v` for
+- Extract `list_numbers.v` from `list.v` and `numbers.v` for
   functions, which operate on lists of numbers (`seq`, `seqZ`,
   `sum_list(_with)` and `max_list(_with)`). `list_numbers.v` is
   exported by the prelude. This is a breaking change if one only
   imports `list.v`, but not the prelude.
 - Rename `drop_insert` into `drop_insert_gt` and add `drop_insert_le`.
-- Added `Countable` instance for `Ascii.ascii`.
+- Add `Countable` instance for `Ascii.ascii`.
 - Make lemma `list_find_Some` more apply friendly.
+- Add `filter_app` lemma.
 - Add tactic `multiset_solver` for solving goals involving multisets.
+- Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
+  `singletonM` and to avoid overlap with `sets.singleton_proper`.
+- Add `wn R` for weakly normalizing elements w.r.t. a relation `R`.
+- Add `encode_Z`/`decode_Z` functions to encode elements of a countable type
+  as integers `Z`, in analogy with `encode_nat`/`decode_nat`.
+- Fix list `Datatypes.length` and string `strings.length` shadowing (`length`
+  should now always be `Datatypes.length`).
+- Change the notation for pattern matching monadic bind into `'pat ← x; y`. It
+  was `''pat ← x; y` (with double `'`) due to a shortcoming of Coq ≤8.7.
 
-## std++ 1.3 (released 2020-03-18)
+## std++ 1.3.0 (released 2020-03-18)
 
 Coq 8.11 is supported by this release.
 
@@ -76,11 +1041,6 @@ Noteworthy additions and changes:
     `seqZ_lookup_ge` → `lookup_seqZ_ge`, and `seqZ_lookup` → `lookup_seqZ`
   + Rename `lookup_seq_inv` → `lookup_seq` and generalize it to a bi-implication
   + Add `NoDup_seqZ` and `Forall_seqZ`
-- Rename `fin_maps.singleton_proper` into `singletonM_proper` since it concerns
-  `singletonM` and to avoid overlap with `sets.singleton_proper`.
-- Add `wn R` for weakly normalizing elements w.r.t. a relation `R`.
-- Add `encode_Z`/`decode_Z` functions to encode elements of a countable type
-  as integers `Z`, in analogy with `encode_nat`/`decode_nat`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
@@ -164,7 +1124,8 @@ Changes:
 - Make `gset` a `Definition` instead of a `Notation` to improve performance.
 - Use `disj_union` (notation `⊎`) for disjoint union on multisets (that adds the
   multiplicities). Repurpose `∪` on multisets for the actual union (that takes
-  the max of the multiplicities). 
+  the max of the multiplicities).
+- Set `Hint Mode` for `pretty`.
 
 Naming:
 

LICENSE

-All files in this development are distributed under the terms of the BSD
-license, included below.
+All files in this development are distributed under the terms of the 3-clause
+BSD license (https://opensource.org/licenses/BSD-3-Clause), included below.
 
 Copyright: std++ developers and contributors
 

Makefile

-# Forward most targets to Coq makefile (with some trick to make this phony)
-%: Makefile.coq phony
-	+@make -f Makefile.coq $@
-
+# Default target
 all: Makefile.coq
-	+@make -f Makefile.coq all
+	+@$(MAKE) -f Makefile.coq all
 .PHONY: all
 
+# Build with dune.
+# This exists only for CI; you should just call `dune build` directly instead.
+dune:
+	@dune build --display=short
+.PHONY: dune
+
+# Permit local customization
+-include Makefile.local
+
+# Generate the _CoqProject file.
+_CoqProject: gen_CoqProject.sh config/paths config/flags config/source-list $(wildcard config/local-flags)
+	@./$< > $@
+
+# Forward most targets to Coq makefile (with some trick to make this phony)
+%: Makefile.coq phony
+	@#echo "Forwarding $@"
+	+@$(MAKE) -f Makefile.coq $@
+phony: ;
+.PHONY: phony
+
 clean: Makefile.coq
-	+@make -f Makefile.coq clean
-	find theories tests exercises solutions \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f Makefile.coq .lia.cache
+	+@$(MAKE) -f Makefile.coq clean
+	@# Make sure not to enter the `_opam` folder.
+	find [a-z]*/ \( -name "*.d" -o -name "*.vo" -o -name "*.vo[sk]" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
+	rm -f Makefile.coq .lia.cache builddep/* _CoqProject
 .PHONY: clean
 
 # Create Coq Makefile.
 Makefile.coq: _CoqProject Makefile
-	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq $(EXTRA_COQFILES)
 
 # Install build-dependencies
-build-dep/opam: opam Makefile
-	@echo "# Creating build-dep package."
-	@mkdir -p build-dep
-	@sed <opam -E 's/^(build|install|remove):.*/\1: []/; s/^name: *"(.*)" */name: "\1-builddep"/' >build-dep/opam
-	@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
-
-build-dep: build-dep/opam phony
-	@# We want opam to not just instal the build-deps now, but to also keep satisfying these
+OPAMFILES=$(wildcard *.opam)
+BUILDDEPFILES=$(addsuffix -builddep.opam, $(addprefix builddep/,$(basename $(OPAMFILES))))
+
+builddep/%-builddep.opam: %.opam Makefile
+	@echo "# Creating builddep package for $<."
+	@mkdir -p builddep
+	@sed <$< -E 's/^(build|install|remove):.*/\1: []/; s/"(.*)"(.*= *version.*)$$/"\1-builddep"\2/;' >$@
+
+builddep-opamfiles: $(BUILDDEPFILES)
+.PHONY: builddep-opamfiles
+
+builddep: builddep-opamfiles
+	@# We want opam to not just install the build-deps now, but to also keep satisfying these
 	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
 	@# that are incompatible with our build requirements.
 	@# To achieve this, we create a fake opam package that has our build-dependencies as
 	@# dependencies, but does not actually install anything itself.
-	@echo "# Installing build-dep package."
-	@opam install $(OPAMFLAGS) build-dep/
+	@echo "# Installing builddep packages."
+	@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
+.PHONY: builddep
 
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-opam: ;
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
 
-# Phony wildcard targets
-phony: ;
-.PHONY: phony
+# Some files that do *not* need to be forwarded to Makefile.coq.
+# ("::" lets Makefile.local overwrite this.)
+Makefile Makefile.local config/paths config/flags config/source-list config/local-flags $(OPAMFILES):: ;

Makefile.coq.local

+# use NO_TEST=1 to skip the tests
+NO_TEST:=
+
+# use MAKE_REF=1 to generate new reference files
+MAKE_REF:=
+
+# Only test reference output on known versions of Coq, to avoid blocking
+# Coq CI when they change the printing a little.
+# Need to make this a lazy variable (`=` instead of `:=`) since COQ_VERSION is only set later.
+COQ_REF=$(shell echo "$(COQ_VERSION)" | grep -E "^8\.(20)\." -q && echo 1)
+
 # Run tests interleaved with main build.  They have to be in the same target for this.
-real-all: $(if $(NO_TEST),,test)
+real-all: style $(if $(NO_TEST),,test)
+
+style: $(VFILES) coq-lint.sh
+# Make sure everything imports the options, and some general linting.
+	$(SHOW)"COQLINT"
+	$(HIDE)for FILE in $(VFILES); do \
+	  if ! grep -F -q 'From stdpp Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
+	  ./coq-lint.sh "$$FILE" || exit 1; \
+	done
+.PHONY: style
 
 # the test suite
-TESTFILES=$(wildcard tests/*.v)
+TESTFILES:=$(shell find tests -name "*.v")
+NORMALIZER:=test-normalizer.sed
 
 test: $(TESTFILES:.v=.vo)
 .PHONY: test
 
 COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
-COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.(7|8|9)\b" -q && echo 1)
-COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
 
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
 	$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
 -include tests/.coqdeps.d
 
-$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
-	$(HIDE)TEST="$$(basename -s .v $<)" && \
-	  if test -f "tests/$$TEST.$(COQ_MINOR_VERSION).ref"; then \
-	    REF="tests/$$TEST.$(COQ_MINOR_VERSION).ref"; \
-	  else \
-	    REF="tests/$$TEST.ref"; \
-	  fi && \
-	  echo "COQTEST$(if $(COQ_OLD), [no ref],$(if $(MAKE_REF), [make ref],)) $<$(if $(COQ_OLD),, (ref: $$REF))" && \
+# Main test script (comments out-of-line because macOS otherwise barfs?!?)
+# - Determine reference file (`REF`).
+# - Print user-visible status line.
+# - unset env vars that change Coq's output
+# - Dump Coq output into a temporary file.
+# - Run `sed -i` on that file in a way that works on macOS.
+# - Either compare the result with the reference file, or move it over the reference file.
+# - Cleanup, and mark as done for make.
+$(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref) $(NORMALIZER)
+	$(HIDE)REF=$*".ref" && \
+	  echo "COQTEST$(if $(COQ_REF),$(if $(MAKE_REF), [make ref],), [ref ignored]) $< (ref: $$REF)" && \
 	  TMPFILE="$$(mktemp)" && \
+	  unset OCAMLRUNPARAM && \
 	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
-	  $(if $(COQ_OLD),true, \
-	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff -u "$$REF" "$$TMPFILE") \
+	  sed -E -f $(NORMALIZER) "$$TMPFILE" > "$$TMPFILE".new && \
+	  mv "$$TMPFILE".new "$$TMPFILE" && \
+	  $(if $(COQ_REF),\
+	    $(if $(MAKE_REF),mv "$$TMPFILE" "$$REF",diff --strip-trailing-cr -u "$$REF" "$$TMPFILE"), \
+	    true \
 	  ) && \
 	  rm -f "$$TMPFILE" && \
 	  touch $@

README.md

@@ -26,26 +26,27 @@ Importing std++ has some side effects as the library sets some global options.
 Notably:
 
 * `Generalizable All Variables`: This option enables implicit generalization in
-  arguments of the form `` `{...}`` (i.e., anonymous arguments).  Unfortunately, it
-  also enables implicit generalization in `Instance`.  We think that the fact
-  that both behaviors are coupled together is a
-  [bug in Coq](https://github.com/coq/coq/issues/6030).
+  arguments of the form `` `{...}`` (i.e., anonymous arguments) and in terms of
+  shape `` `{}``/`` `[]``/`` `()``. See [Coq's
+  manual](https://coq.inria.fr/distrib/current/refman/language/extensions/implicit-arguments.html#implicit-generalization)
+  for further details.
 * The behavior of `Program` is tweaked: `Unset Transparent Obligations`,
   `Obligation Tactic := idtac`, `Add Search Blacklist "_obligation_"`.  See
   [`base.v`](theories/base.v) for further details.
-* It blocks `simpl` on all operations involving integers `Z` (by setting
-  `Arguments op : simpl never`). We do this because `simpl` tends to expose
-  the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
-  As a consequence of blocking `simpl`, due to
-  [Coq bug #5039](https://github.com/coq/coq/issues/5039) the `omega` tactic
-  becomes unreliable. We do not consider this an issue since we use `lia` (for
-  which the aforementioned Coq bug was fixed) instead of `omega` everywhere.
+* It blocks `simpl` on all operations involving `Z`, `N`, and `positive` (by
+  setting `Arguments op : simpl never`). We do this because `simpl` tends to
+  expose the internals of said operations (e.g. try `simpl` on `Z.of_nat (S n) + y`).
+* It sets `intuition_solver` to `auto`. The default is `auto with *`, which is
+  very expensive.
 
 ## Prerequisites
 
 This version is known to compile with:
 
- - Coq version 8.8.2 / 8.9.1 / 8.10.2 / 8.11.2
+ - Coq version 8.18.0 / 8.19.1 / 8.20.1 / 9.0.0
+
+Generally we always aim to support the last two stable Coq releases. Support for
+older versions will be dropped when it is convenient.
 
 ## Installing via opam
 
@@ -65,6 +66,19 @@ To obtain a development version, add the Iris opam repository:
 Run `make -jN` in this directory to build the library, where `N` is the number
 of your CPU cores.  Then run `make install` to install the library.
 
+## Unstable libraries
+
+The `stdpp_unstable` folder contains a set of libraries that are not
+deemed stable enough to be included in the main std++ library. These
+libraries are available via the `coq-stdpp-unstable` opam package. For
+each library, there is a corresponding "tracking issue" in the std++
+issue tracker (also linked from the library itself) which tracks the
+work that still needs to be done before moving the library to std++.
+No stability guarantees whatsoever are made for this package.
+
+Note that the unstable package is not released, so it only exists in the
+development version of std++.
+
 ## Contributing to std++
 
 If you want to report a bug, please use the
@@ -79,9 +93,12 @@ your account.  Then you can fork the
 [Coq-std++ git repository](https://gitlab.mpi-sws.org/iris/stdpp), make your
 changes in your fork, and create a merge request.
 
+Please refer to [our style guide](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/docs/style_guide.md)
+for code formatting and naming policies.
+
 ## Common problems
 
-On Windows, differences in line endings may cause tests to fail. This can be 
+On Windows, differences in line endings may cause tests to fail. This can be
 fixed by setting Git's autocrlf option to true:
 
     git config --global core.autocrlf true

_CoqProject

--Q theories stdpp
-# "Declare Scope" does not exist yet in 8.9.
--arg -w -arg -undeclared-scope
-
-theories/base.v
-theories/tactics.v
-theories/option.v
-theories/fin_map_dom.v
-theories/boolset.v
-theories/fin_maps.v
-theories/fin.v
-theories/vector.v
-theories/pmap.v
-theories/stringmap.v
-theories/fin_sets.v
-theories/mapset.v
-theories/proof_irrel.v
-theories/hashset.v
-theories/pretty.v
-theories/countable.v
-theories/orders.v
-theories/natmap.v
-theories/strings.v
-theories/relations.v
-theories/sets.v
-theories/listset.v
-theories/streams.v
-theories/gmap.v
-theories/gmultiset.v
-theories/prelude.v
-theories/listset_nodup.v
-theories/finite.v
-theories/numbers.v
-theories/nmap.v
-theories/zmap.v
-theories/coPset.v
-theories/coGset.v
-theories/lexico.v
-theories/propset.v
-theories/decidable.v
-theories/list.v
-theories/list_numbers.v
-theories/functions.v
-theories/hlist.v
-theories/sorting.v
-theories/infinite.v
-theories/nat_cancel.v
-theories/namespaces.v
-theories/telescopes.v
-theories/binders.v

config/flags

+# Specification for custom Rocq compilation flags.
+# Syntax:
+# - One flag per line with no leading/trailing blanks.
+# - Empty lines and lines starting with '#' are ignored.
+
+# Fixing this one requires Coq 8.19
+-w
+-argument-scope-delimiter
+
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-w
+-notation-incompatible-prefix
+
+# We can't do this migration yet until we require Coq 9.0
+-w
+-deprecated-from-Coq
+-w
+-deprecated-dirpath-Coq

config/paths

+# Search paths for all packages.
+# Each line should be of the form "<PACKAGE> <LOGICAL_PATH>",
+# where <PACKAGE> is the name of a directory that matches the
+# corresponding package name.
+stdpp stdpp
+stdpp_bitvector stdpp.bitvector
+stdpp_unstable stdpp.unstable

config/source-list

+# List of source files included in the libraries.
+
+stdpp/options.v
+stdpp/base.v
+stdpp/tactics.v
+stdpp/option.v
+stdpp/fin_map_dom.v
+stdpp/boolset.v
+stdpp/fin_maps.v
+stdpp/fin.v
+stdpp/vector.v
+stdpp/pmap.v
+stdpp/stringmap.v
+stdpp/fin_sets.v
+stdpp/mapset.v
+stdpp/proof_irrel.v
+stdpp/hashset.v
+stdpp/pretty.v
+stdpp/countable.v
+stdpp/orders.v
+stdpp/natmap.v
+stdpp/strings.v
+stdpp/well_founded.v
+stdpp/relations.v
+stdpp/sets.v
+stdpp/listset.v
+stdpp/streams.v
+stdpp/gmap.v
+stdpp/gmultiset.v
+stdpp/prelude.v
+stdpp/listset_nodup.v
+stdpp/finite.v
+stdpp/numbers.v
+stdpp/nmap.v
+stdpp/zmap.v
+stdpp/coPset.v
+stdpp/coGset.v
+stdpp/lexico.v
+stdpp/propset.v
+stdpp/decidable.v
+stdpp/list.v
+stdpp/list_basics.v
+stdpp/list_relations.v
+stdpp/list_monad.v
+stdpp/list_misc.v
+stdpp/list_tactics.v
+stdpp/list_numbers.v
+stdpp/functions.v
+stdpp/hlist.v
+stdpp/sorting.v
+stdpp/infinite.v
+stdpp/nat_cancel.v
+stdpp/namespaces.v
+stdpp/telescopes.v
+stdpp/binders.v
+stdpp/ssreflect.v
+
+stdpp_bitvector/definitions.v
+stdpp_bitvector/tactics.v
+stdpp_bitvector/bitvector.v
+
+stdpp_unstable/bitblast.v

coq-lint.sh

+#!/bin/sh
+set -e
+## A simple shell script checking for some common Coq issues.
+
+FILE="$1"
+
+if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold|Rewrite)|(Open|Close)\s+Scope|Opaque|Transparent|Typeclasses (Opaque|Transparent))\b' "$FILE"; then
+    echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
+    echo "Please add 'Global' or 'Local' as appropriate."
+    echo
+    exit 1
+fi

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: "A library for bitvectors based on std++"
+description: """
+This library provides the `bv n` type for representing n-bit bitvectors (i.e.,
+fixed-size integers with n bits). It comes with definitions for the standard operations
+(e.g., the operations exposed by SMT-LIB) and some basic automation for solving bitvector
+goals based on the lia tactic.
+"""
+tags: [
+  "logpath:stdpp.bitvector"
+]
+
+depends: [
+  "coq-stdpp" {= version}
+]
+
+build: ["./make-package" "stdpp_bitvector" "-j%{jobs}%"]
+install: ["./make-package" "stdpp_bitvector" "install"]

coq-stdpp-unstable.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: "Unfinished std++ libraries"
+description: """
+This package contains libraries that have been proposed for inclusion in std++, but more
+work is needed before they are ready for this.
+"""
+tags: [
+  "logpath:stdpp.unstable"
+]
+
+depends: [
+  "coq-stdpp" {= version}
+  "coq-stdpp-bitvector" {= version}
+]
+
+build: ["./make-package" "stdpp_unstable" "-j%{jobs}%"]
+install: ["./make-package" "stdpp_unstable" "install"]

opam → coq-stdpp.opam

 opam-version: "2.0"
-name: "coq-stdpp"
 maintainer: "Ralf Jung <jung@mpi-sws.org>"
-authors: "Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung"
-license: "BSD"
+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++ is an extended \"Standard Library\" for Coq"
+synopsis: "An extended \"Standard Library\" for Coq"
 description: """
 The key features of this library are as follows:
 
@@ -28,10 +28,13 @@ The key features of this library are as follows:
   `set_solver` for goals involving set operations.
 - It is entirely dependency- and axiom-free.
 """
+tags: [
+  "logpath:stdpp"
+]
 
 depends: [
-  "coq" { (= "8.8.2") | (>= "8.9.1" & < "8.13~") | (= "dev") }
+  "coq" { (>= "8.18" & < "9.1~") | (= "dev") }
 ]
 
-build: [make "-j%{jobs}%"]
-install: [make "install"]
+build: ["./make-package" "stdpp" "-j%{jobs}%"]
+install: ["./make-package" "stdpp" "install"]

docs/dune.md

+Support for the dune build system
+=================================
+
+**NOTE:** in case of problem with the dune build, you can ask @lepigre or
+@Blaisorblade for help.
+
+The library can be built using dune by running `dune build`. Note that `dune`
+needs to be installed separately with `opam install dune`, as it is currently
+not part of the dependencies of the project.
+
+Useful links:
+- [dune documentation](https://dune.readthedocs.io)
+- [coq zulip channel](https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users)
+
+
+Editor support
+--------------
+
+Editors relying on `_CoqProject` files for their configuration are supported.
+A suitable `_CoqProject` file is generated by `dune build`. Note that you must
+invoke `dune` manually to make sure that the dependencies of the file you are
+stepping through are up-to-date. To build a single file, you can use, e.g.,
+`dune build stdpp/options.vo`. To build only the `stdpp` folder, you can do
+`dune build stdpp`.
+
+Alternatively, you can configure your editor to invoke `dune coq top` instead
+of `coqtop`, but that is non-trivial for most editors.
+
+### Extra `_CoqProject` flags
+
+If file `config/local-flags` exists, then its contents is added at the end of
+the generated `_CoqProject` file. This can be useful when the library is built
+together with its dependencies (e.g., the Rocq standard library) as part of a
+dune workspace build. Note that the file can be generated with a dune rule.

dune

+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   ; Configure coqc flags.
+   (flags (:standard %{read-lines:flags.dune})))))
+
+(rule
+ (action
+  (with-stdout-to flags.dune
+   (pipe-stdout
+    (cat config/flags)
+    (bash "grep '^[^#]\\+'")))))
+
+(rule
+ (deps
+  (glob_files config/*))
+ (mode promote)
+ (action
+  (with-stdout-to _CoqProject
+   (run ./gen_CoqProject.sh))))

dune-project

+(lang dune 3.8)
+(using coq 0.8)