.gitattributes

+# Enable syntax highlighting.
 *.v gitlab-language=coq
+
+# Convert to native line endings on checkout.
+*.ref text
+# Shell scripts need Linux line endings.
+*.sh eol=lf

.gitignore

 *.vo
+*.vos
+*.vok
 *.vio
 *.v.d
 .coqdeps.d
+.Makefile.coq.d
 *.glob
 *.cache
 *.aux
@@ -12,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,63 +36,60 @@ variables:
   cache:
     key: "$CI_JOB_NAME"
     paths:
-    - opamroot/
-  only:
-  - master
-  - /^ci/
+    - _opam/
   except:
   - triggers
   - schedules
+  - api
 
 ## Build jobs
 
-build-coq.dev:
+# The newest version runs with timing.
+build-coq.9.0.0:
   <<: *template
   variables:
-    OCAML: "ocaml-base-compiler.4.07.0"
-    OPAM_PINS: "coq version dev"
+    OPAM_PINS: "coq version 9.0.0"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
     CI_COQCHK: "1"
-
-build-coq.8.9.0:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.9.0"
-    OPAM_PKG: "coq-stdpp"
+    OPAM_PKG: "1"
     DOC_DIR: "coqdoc@center.mpi-sws.org:stdpp"
-    TIMING_CONF: "coq-8.9.0"
   tags:
   - fp-timing
+  interruptible: false
 
-build-coq.8.8.2:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.8.2"
-
-build-coq.8.8.1:
+# The newest version also runs in MRs, without timing.
+build-coq.9.0.0-mr:
   <<: *template
+  <<: *only_mr
   variables:
-    OPAM_PINS: "coq version 8.8.1"
+    OPAM_PINS: "coq version 9.0.0"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
 
-build-coq.8.8.0:
+# 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 8.8.0"
-    TIMING_CONF: "coq-8.8.0"
-  tags:
-  - fp-timing
+    OPAM_PINS: "coq version 9.0.0   dune version 3.18.1"
+    MAKE_TARGET: "dune"
 
-build-coq.8.7.2:
+build-coq.8.20.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.7.2"
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
 
-build-coq.8.7.1:
+build-coq.8.19.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.7.1"
+    OPAM_PINS: "coq version 8.19.1"
+    DENY_WARNINGS: "1"
 
-build-coq.8.7.0:
+# The oldest version runs in MRs, without name mangling.
+build-coq.8.18.0:
   <<: *template
+  <<: *branches_and_mr
   variables:
-    OPAM_PINS: "coq version 8.7.0"
-
+    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.
 
+## 1.12.0 (2025-06-04)
+
+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`. 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.
+- Add the `select` and `revert select` tactics for selecting and
+  reverting a hypothesis based on a pattern.
+- 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`.
+- 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.0 (released 2020-03-18)
+
+Coq 8.11 is supported by this release.
+
+This release of std++ received contributions by Amin Timany, Armaël Guéneau,
+Dan Frumin, David Swasey, Jacques-Henri Jourdan, Michael Sammler, Paolo G.
+Giarrusso, Pierre-Marie Pédrot, Ralf Jung, Robbert Krebbers, Simon Friis Vindum,
+Tej Chajed, and William Mansky
+
+Noteworthy additions and changes:
+
+- Rename `dom_map_filter` into `dom_map_filter_subseteq` and repurpose
+  `dom_map_filter` for the version with the equality. This follows the naming
+  convention for similar lemmas.
+- Generalize `list_find_Some` and `list_find_None` to become bi-implications.
+- Disambiguate Haskell-style notations for partially applied operators. For
+  example, change `(!! i)` into `(.!! x)` so that `!!` can also be used as a
+  prefix, as done in VST. A sed script to perform the renaming can be found at:
+  https://gitlab.mpi-sws.org/iris/stdpp/merge_requests/93
+- Add type class `TopSet` for sets with a `⊤` element. Provide instances for
+  `boolset`, `propset`, and `coPset`.
+- Add `set_solver` support for `dom`.
+- Rename `vec_to_list_of_list` into `vec_to_list_to_vec`, and add new lemma
+  `list_to_vec_to_list` for the converse.
+- Rename `fin_of_nat` into `nat_to_fin`, `fin_to_of_nat` into
+  `fin_to_nat_to_fin`, and `fin_of_to_nat` into `nat_to_fin_to_nat`, to follow
+  the conventions.
+- Add `Countable` instance for `vec`.
+- Introduce `destruct_or{?,!}` to repeatedly destruct disjunctions in
+  assumptions. The tactic can also be provided an explicit assumption name;
+  `destruct_and{?,!}` has been generalized accordingly and now can also be
+  provided an explicit assumption name.
+  Slight breaking change: `destruct_and` no longer handle `False`;
+  `destruct_or` now handles `False` while `destruct_and` handles `True`,
+  as the respective units of disjunction and conjunction.
+- Add tactic `set_unfold in H`.
+- Set `Hint Mode` for `TCAnd`, `TCOr`, `TCForall`, `TCForall2`, `TCElemOf`,
+  `TCEq`, and `TCDiag`.
+- Add type class `LookupTotal` with total lookup operation `(!!!) : M → K → A`.
+  Provide instances for `list`, `fin_map`, and `vec`, as well as corresponding
+  lemmas for the operations on these types. The instance for `vec` replaces the
+  ad-hoc `!!!` definition. As a consequence, arguments of `!!!` are no longer
+  parsed in `vec_scope` and `fin_scope`, respectively. Moreover, since `!!!`
+  is overloaded, coercions around `!!!` no longer work.
+- Make lemmas for `seq` and `seqZ` consistent:
+  + Rename `fmap_seq` → `fmap_S_seq`
+  + Add `fmap_add_seq`, and rename `seqZ_fmap` → `fmap_add_seqZ`
+  + Rename `lookup_seq` → `lookup_seq_lt`
+  + Rename `seqZ_lookup_lt` → `lookup_seqZ_lt`,
+    `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`
+
+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 '
+s/\bdom_map_filter\b/dom_map_filter_subseteq/g
+s/\bfmap_seq\b/fmap_S_seq/g
+s/\bseqZ_fmap\b/fmap_add_seqZ/g
+s/\blookup_seq\b/lookup_seq_lt/g
+s/\blookup_seq_inv\b/lookup_seq/g
+s/\bseqZ_lookup_lt\b/lookup_seqZ_lt/g
+s/\bseqZ_lookup_ge\b/lookup_seqZ_ge/g
+s/\bseqZ_lookup\b/lookup_seqZ/g
+s/\bvec_to_list_of_list\b/vec_to_list_to_vec/g
+s/\bfin_of_nat\b/nat_to_fin/g
+s/\bfin_to_of_nat\b/fin_to_nat_to_fin/g
+s/\bfin_of_to_nat\b/nat_to_fin_to_nat/g
+' $(find theories -name "*.v")
+```
+
+## std++ 1.2.1 (released 2019-08-29)
+
+This release of std++ received contributions by Dan Frumin, Michael Sammler,
+Paolo G. Giarrusso, Paulo Emílio de Vilhena, Ralf Jung, Robbert Krebbers,
+Rodolphe Lepigre, and Simon Spies.
+
+Noteworthy additions and changes:
+
+- Introduce `max` and `min` infix notations for `N` and `Z` like we have for `nat`.
+- Make `solve_ndisj` tactic more powerful.
+- Add type class `Involutive`.
+- Improve `naive_solver` performance in case the goal is trivially solvable.
+- Add a bunch of new lemmas for list, set, and map operations.
+- Rename `lookup_imap` into `map_lookup_imap`.
+
 ## std++ 1.2.0 (released 2019-04-26)
 
 Coq 8.9 is supported by this release, but Coq 8.6 is no longer supported. Use
@@ -49,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
 
-                            BSD LICENCE
+------------------------------------------------------------------------------
 
 Redistribution and use in source and binary forms, with or without
 modification, are permitted provided that the following conditions are met:
@@ -12,18 +12,17 @@ modification, are permitted provided that the following conditions are met:
     * Redistributions in binary form must reproduce the above copyright
       notice, this list of conditions and the following disclaimer in the
       documentation and/or other materials provided with the distribution.
-    * Neither the name of the <organization> nor the
-      names of its contributors may be used to endorse or promote products
-      derived from this software without specific prior written permission.
+    * Neither the name of the copyright holder nor the names of its contributors
+      may be used to endorse or promote products derived from this software
+      without specific prior written permission.
 
 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
 ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-DISCLAIMED. IN NO EVENT SHALL <COPYRIGHT HOLDER> BE LIABLE FOR ANY
-DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
-LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
-ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-

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 \( -name "*.d" -o -name "*.vo" -o -name "*.aux" -o -name "*.cache" -o -name "*.glob" -o -name "*.vio" \) -print -delete || true
-	rm -f Makefile.coq
+	+@$(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 "# Pinning build-dep package." && \
-	  if opam --version | grep "^1\." -q; then \
-	    BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
-	    opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
-	    opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
-	  else \
-	    opam install $(OPAMFLAGS) build-dep/; \
-	  fi
-
-# Some files that do *not* need to be forwarded to Makefile.coq
-Makefile: ;
-_CoqProject: ;
-opam: ;
-
-# Phony wildcard targets
-phony: ;
-.PHONY: phony
+	@echo "# Installing builddep packages."
+	@opam install $(OPAMFLAGS) $(BUILDDEPFILES)
+.PHONY: builddep
+
+# Backwards compatibility target
+build-dep: builddep
+.PHONY: build-dep
+
+# 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\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,30 +26,31 @@ 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.7.0 / 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2 / 8.9.0
+ - 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
 
-To obtain the latest stable release via opam (1.2.2 or newer), you have to add
+To obtain the latest stable release via opam (2.0.0 or newer), you have to add
 the Coq opam repository:
 
     opam repo add coq-released https://coq.inria.fr/opam/released
@@ -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,3 +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
+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/lexico.v
-theories/propset.v
-theories/decidable.v
-theories/list.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"]

descr → coq-stdpp.opam

-This project contains an extended "Standard Library" for Coq called coq-std++.
+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: "An extended \"Standard Library\" for Coq"
+description: """
 The key features of this library are as follows:
 
 - It provides a great number of definitions and lemmas for common data
@@ -17,3 +27,14 @@ The key features of this library are as follows:
   for proving compatibility of functions with respect to relations, and a solver
   `set_solver` for goals involving set operations.
 - It is entirely dependency- and axiom-free.
+"""
+tags: [
+  "logpath:stdpp"
+]
+
+depends: [
+  "coq" { (>= "8.18" & < "9.1~") | (= "dev") }
+]
+
+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)