.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,12 @@
 .coq-native/
 Makefile.coq
 Makefile.coq.conf
+_CoqProject.*
+Makefile.package.*
+.Makefile.package.*
 *.crashcoqide
 html/
-build-dep/
+builddep/
 _opam
+_build/
+*.install

.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,46 @@ variables:
 
 ## Build jobs
 
-build-coq.8.12.dev:
+# The newest version runs with timing.
+build-coq.8.20.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.12.dev"
+    OPAM_PINS: "coq version 8.20.1"
+    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.8.20.1-mr:
+  <<: *template
+  <<: *only_mr
+  variables:
+    OPAM_PINS: "coq version 8.20.1"
+    DENY_WARNINGS: "1"
+    MANGLE_NAMES: "1"
 
-build-coq.8.10.2:
+# Also ensure Dune works.
+build-coq.8.20.1-dune:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.10.2"
+    OPAM_PINS: "coq version 8.20.1   dune version 3.15.2"
+    MAKE_TARGET: "dune"
 
-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
+
+- 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)
+- Add tactic `notypeclasses apply` that works like `notypeclasses refine` but
+  automatically adds `_` until the given lemma takes no more arguments.
+- 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)
+
+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.
@@ -173,7 +1108,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:
 

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
+
+# 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/*
 .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 _CoqProject $(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
+
+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
+# Search paths for all packages. They must all match the regex
+# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
+-Q stdpp stdpp
+-Q stdpp_bitvector stdpp.bitvector
+-Q stdpp_unstable stdpp.unstable
 
-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
+# Custom flags (to be kept in sync with the dune file at the root of the repo).
+# Fixing this one requires Coq 8.19
+-arg -w -arg -argument-scope-delimiter
+# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
+-arg -w -arg -notation-incompatible-prefix
+# We can't do this migration yet until we require Coq 9.0
+-arg -w -arg -deprecated-from-Coq
+-arg -w -arg -deprecated-dirpath-Coq
+
+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_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/bash
+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: "The std++ team"
-license: "BSD"
+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
+--------------
+
+Good dune support in editors is lacking at the moment, but there are tricks you
+can play to make it work.
+
+One option is to configure your editor to invoke the `dune coq top` command
+instead of `coqtop`, but that is not easy to configure.
+
+Another option is to change the `_CoqProject` file to something like:
+```
+-Q stdpp stdpp
+-Q _build/default/stdpp stdpp
+-Q stdpp_bitvector stdpp.bitvector
+-Q _build/default/stdpp_bitvector stdpp.bitvector
+-Q stdpp_unstable stdpp.unstable
+-Q _build/default/stdpp_unstable stdpp.unstable
+```
+Note that this includes two bindings for each logical path: a binding to a
+folder in the source tree (where editors will find the `.v` files), and a
+binding to the same folder under `_build/default` (where editors will find
+the corresponding `.vo` files). The binding for a source folder must come
+before the binding for the corresponding build folder, so that editors know
+to jump to source files in the source tree (and not their read-only copy in
+the build folder).
+
+If you do this, you still need to 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 do, e.g., `dune build stdpp/options.vo`. To build only
+the `stdpp` folder, you can do `dune build stdpp`.

dune

+(env
+ (_ ; Applies to all profiles (dev, release, ...).
+  (coq
+   (flags ; Configure the coqc flags.
+    (:standard ; Keeping the default flags.
+     ; Add custom flags (to be kept in sync with _CoqProject).
+     -w -argument-scope-delimiter
+     -w -notation-incompatible-prefix)))))

dune-project

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

make-package

+#!/bin/sh
+set -e
+# Helper script to build and/or install just one package out of this repository.
+# Assumes that all the other packages it depends on have been installed already!
+
+# Make sure we get a GNU version of make.
+# This is exactly how opam determines which make executable to use.
+OS=$(uname)
+MAKE="make"
+if [ $OS == "FreeBSD" ] || [ $OS == "OpenBSD" ] ||\
+       [ $OS == "NetBSD" ] || [ $OS == "DragonFly" ]; then
+    MAKE="gmake"
+fi
+
+PROJECT="$1"
+shift
+
+COQFILE="_CoqProject.$PROJECT"
+MAKEFILE="Makefile.package.$PROJECT"
+
+if ! grep -E -q "^$PROJECT/" _CoqProject; then
+    echo "No files in $PROJECT/ found in _CoqProject; this does not seem to be a valid project name."
+    exit 1
+fi
+
+# Generate _CoqProject file and Makefile
+rm -f "$COQFILE"
+# Get the right "-Q" line.
+grep -E "^-Q $PROJECT[ /]" _CoqProject >> "$COQFILE"
+# Get everything until the first empty line except for the "-Q" lines.
+sed -n '/./!q;p' _CoqProject | grep -E -v "^-Q " >> "$COQFILE"
+# Get the files.
+grep -E "^$PROJECT/" _CoqProject >> "$COQFILE"
+# Now we can run coq_makefile.
+"${COQBIN}coq_makefile" -f "$COQFILE" -o "$MAKEFILE"
+
+# Run build
+$MAKE -f "$MAKEFILE" "$@"
+
+# Cleanup
+rm -f ".$MAKEFILE.d" "$MAKEFILE"*

theories/base.v → stdpp/base.v

@@ -6,12 +6,18 @@ structures. *)
 (* We want to ensure that [le] and [lt] refer to operations on [nat].
 These two functions being defined both in [Coq.Bool] and in [Coq.Peano],
 we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
-From Coq Require Export Morphisms RelationClasses List Bool Utf8 Setoid Peano.
+(* We also want to ensure that notations from [Coq.Utf8] take precedence
+over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
+From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
 From Coq Require Import Permutation.
-Set Default Proof Using "Type".
 Export ListNotations.
 From Coq.Program Require Export Basics Syntax.
 
+(* notations _.1 and _.2 below, TODO: remove when requiring Coq > 8.19 *)
+From Coq.ssr Require Import (notations) ssrfun.
+
+From stdpp Require Import options.
+
 (** This notation is necessary to prevent [length] from being printed
 as [strings.length] if strings.v is imported and later base.v. See
 also strings.v and
@@ -42,18 +48,35 @@ Global Unset Transparent Obligations.
 obligation tactic is [Tactics.program_simpl], which, among other things,
 introduces all variables and gives them fresh names. As such, it becomes
 impossible to refer to hypotheses in a robust way. *)
-Obligation Tactic := idtac.
+Global Obligation Tactic := idtac.
 
-(** 3. Hide obligations from the results of the [Search] commands. *)
+(** 3. Hide obligations and unsealing lemmas from the results of the [Search]
+commands. *)
 Add Search Blacklist "_obligation_".
+Add Search Blacklist "_unseal".
 
 (** * Sealing off definitions *)
-Section seal.
-  Local Set Primitive Projections.
-  Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
-End seal.
-Arguments unseal {_ _} _ : assert.
-Arguments seal_eq {_ _} _ : assert.
+#[projections(primitive=yes)]
+Record seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
+Global Arguments unseal {_ _} _ : assert.
+Global Arguments seal_eq {_ _} _ : assert.
+
+(** * Solving type class instances *)
+(** The tactic [tc_solve] is used to solve type class goals by invoking type
+class search. It is similar to [apply _], but it is more robust since it does
+not affect unrelated goals/evars due to https://github.com/coq/coq/issues/6583.
+
+The tactic [tc_solve] is particularly useful when building custom tactics that
+need tight control over when type class search is invoked. In Iris, many of the
+proof mode tactics make use of [notypeclasses refine] and use [tc_solve] to
+manually invoke type class search.
+
+Note that [typeclasses eauto] is multi-success. That means, whenever subsequent
+tactics fail, it will backtrack to [typeclasses eauto] to try the next type
+class instance. This is almost always undesired and can lead to poor performance
+and horrible error messages. Hence, we wrap it in a [once]. *)
+Ltac tc_solve :=
+  solve [once (typeclasses eauto)].
 
 (** * Non-backtracking type classes *)
 (** The type class [TCNoBackTrack P] can be used to establish [P] without ever
@@ -68,8 +91,9 @@ issue #6714.
 
 See https://gitlab.mpi-sws.org/FP/iris-coq/merge_requests/112 for a rationale
 of this type class. *)
-Class TCNoBackTrack (P : Prop) := { tc_no_backtrack : P }.
-Hint Extern 0 (TCNoBackTrack _) => constructor; apply _ : typeclass_instances.
+Class TCNoBackTrack (P : Prop) := TCNoBackTrack_intro { tc_no_backtrack : P }.
+Global Hint Extern 0 (TCNoBackTrack _) =>
+  notypeclasses refine (TCNoBackTrack_intro _ _); tc_solve : typeclass_instances.
 
 (* A conditional at the type class level. Note that [TCIf P Q R] is not the same
 as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
@@ -81,16 +105,16 @@ Inductive TCIf (P Q R : Prop) : Prop :=
   | TCIf_false : R → TCIf P Q R.
 Existing Class TCIf.
 
-Hint Extern 0 (TCIf _ _ _) =>
-  first [apply TCIf_true; [apply _|]
-        |apply TCIf_false] : typeclass_instances.
+Global Hint Extern 0 (TCIf _ _ _) =>
+  first [notypeclasses refine (TCIf_true _ _ _ _ _); [tc_solve|]
+        |notypeclasses refine (TCIf_false _ _ _ _)] : typeclass_instances.
 
 (** * Typeclass opaque definitions *)
 (** The constant [tc_opaque] is used to make definitions opaque for just type
 class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
 Definition tc_opaque {A} (x : A) : A := x.
-Typeclasses Opaque tc_opaque.
-Arguments tc_opaque {_} _ /.
+Global Typeclasses Opaque tc_opaque.
+Global Arguments tc_opaque {_} _ /.
 
 (** Below we define type class versions of the common logical operators. It is
 important to note that we duplicate the definitions, and do not declare the
@@ -112,26 +136,39 @@ Inductive TCOr (P1 P2 : Prop) : Prop :=
   | TCOr_l : P1 → TCOr P1 P2
   | TCOr_r : P2 → TCOr P1 P2.
 Existing Class TCOr.
-Existing Instance TCOr_l | 9.
-Existing Instance TCOr_r | 10.
-Hint Mode TCOr ! ! : typeclass_instances.
+Global Existing Instance TCOr_l | 9.
+Global Existing Instance TCOr_r | 10.
+Global Hint Mode TCOr ! ! : typeclass_instances.
 
 Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1 → P2 → TCAnd P1 P2.
 Existing Class TCAnd.
-Existing Instance TCAnd_intro.
-Hint Mode TCAnd ! ! : typeclass_instances.
+Global Existing Instance TCAnd_intro.
+Global Hint Mode TCAnd ! ! : typeclass_instances.
 
 Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
 Existing Class TCTrue.
-Existing Instance TCTrue_intro.
+Global Existing Instance TCTrue_intro.
+
+(** The class [TCFalse] is not stricly necessary as one could also use
+[False]. However, users might expect that TCFalse exists and if it
+does not, it can cause hard to diagnose bugs due to automatic
+generalization. *)
+Inductive TCFalse : Prop :=.
+Existing Class TCFalse.
+
+(** The class [TCUnless] can be used to check that search for [P]
+fails. This is useful as a guard for certain instances together with
+classes like [TCFastDone] (see [tactics.v]) to prevent infinite loops
+(e.g. when saturating the context). *)
+Notation TCUnless P := (TCIf P TCFalse TCTrue).
 
 Inductive TCForall {A} (P : A → Prop) : list A → Prop :=
   | TCForall_nil : TCForall P []
   | TCForall_cons x xs : P x → TCForall P xs → TCForall P (x :: xs).
 Existing Class TCForall.
-Existing Instance TCForall_nil.
-Existing Instance TCForall_cons.
-Hint Mode TCForall ! ! ! : typeclass_instances.
+Global Existing Instance TCForall_nil.
+Global Existing Instance TCForall_cons.
+Global Hint Mode TCForall ! ! ! : typeclass_instances.
 
 (** The class [TCForall2 P l k] is commonly used to transform an input list [l]
 into an output list [k], or the converse. Therefore there are two modes, either
@@ -141,37 +178,61 @@ Inductive TCForall2 {A B} (P : A → B → Prop) : list A → list B → Prop :=
   | TCForall2_cons x y xs ys :
      P x y → TCForall2 P xs ys → TCForall2 P (x :: xs) (y :: ys).
 Existing Class TCForall2.
-Existing Instance TCForall2_nil.
-Existing Instance TCForall2_cons.
-Hint Mode TCForall2 ! ! ! ! - : typeclass_instances.
-Hint Mode TCForall2 ! ! ! - ! : typeclass_instances.
+Global Existing Instance TCForall2_nil.
+Global Existing Instance TCForall2_cons.
+Global Hint Mode TCForall2 ! ! ! ! - : typeclass_instances.
+Global Hint Mode TCForall2 ! ! ! - ! : typeclass_instances.
+
+Inductive TCExists {A} (P : A → Prop) : list A → Prop :=
+  | TCExists_cons_hd x l : P x → TCExists P (x :: l)
+  | TCExists_cons_tl x l: TCExists P l → TCExists P (x :: l).
+Existing Class TCExists.
+Global Existing Instance TCExists_cons_hd | 10.
+Global Existing Instance TCExists_cons_tl | 20.
+Global Hint Mode TCExists ! ! ! : typeclass_instances.
 
 Inductive TCElemOf {A} (x : A) : list A → Prop :=
   | TCElemOf_here xs : TCElemOf x (x :: xs)
   | TCElemOf_further y xs : TCElemOf x xs → TCElemOf x (y :: xs).
 Existing Class TCElemOf.
-Existing Instance TCElemOf_here.
-Existing Instance TCElemOf_further.
-Hint Mode TCElemOf ! ! ! : typeclass_instances.
-
-(** We declare both arguments [x] and [y] of [TCEq x y] as outputs, which means
-[TCEq] can also be used to unify evars. This is harmless: since the only
-instance of [TCEq] is [TCEq_refl] below, it can never cause loops. See
-https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case. *)
+Global Existing Instance TCElemOf_here.
+Global Existing Instance TCElemOf_further.
+Global Hint Mode TCElemOf ! ! ! : typeclass_instances.
+
+(** The intended use of [TCEq x y] is to use [x] as input and [y] as output, but
+this is not enforced. We use output mode [-] (instead of [!]) for [x] to ensure
+that type class search succeed on goals like [TCEq (if ? then e1 else e2) ?y],
+see https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case.
+Mode [-] is harmless, the only instance of [TCEq] is [TCEq_refl] below, so we
+cannot create loops. *)
 Inductive TCEq {A} (x : A) : A → Prop := TCEq_refl : TCEq x x.
 Existing Class TCEq.
-Existing Instance TCEq_refl.
-Hint Mode TCEq ! - - : typeclass_instances.
+Global Existing Instance TCEq_refl.
+Global Hint Mode TCEq ! - - : typeclass_instances.
 
 Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 ↔ x1 = x2.
 Proof. split; destruct 1; reflexivity. Qed.
 
+(** The [TCSimpl x y] type class is similar to [TCEq] but performs [simpl]
+before proving the goal by reflexivity. Similar to [TCEq], the argument [x]
+is the input and [y] the output. When solving [TCEq x y], the argument [x]
+should be a concrete term and [y] an evar for the [simpl]ed result. *)
+Class TCSimpl {A} (x x' : A) := TCSimpl_TCEq : TCEq x x'.
+Global Hint Extern 0 (TCSimpl _ _) =>
+  (* Since the second argument should be an evar, we can call [simpl] on the
+  whole goal. *)
+  simpl; notypeclasses refine (TCEq_refl _) : typeclass_instances.
+Global Hint Mode TCSimpl ! - - : typeclass_instances.
+
+Lemma TCSimpl_eq {A} (x1 x2 : A) : TCSimpl x1 x2 ↔ x1 = x2.
+Proof. apply TCEq_eq. Qed.
+
 Inductive TCDiag {A} (C : A → Prop) : A → A → Prop :=
   | TCDiag_diag x : C x → TCDiag C x x.
 Existing Class TCDiag.
-Existing Instance TCDiag_diag.
-Hint Mode TCDiag ! ! ! - : typeclass_instances.
-Hint Mode TCDiag ! ! - ! : typeclass_instances.
+Global Existing Instance TCDiag_diag.
+Global Hint Mode TCDiag ! ! ! - : typeclass_instances.
+Global Hint Mode TCDiag ! ! - ! : typeclass_instances.
 
 (** Given a proposition [P] that is a type class, [tc_to_bool P] will return
 [true] iff there is an instance of [P]. It is often useful in Ltac programming,
@@ -181,6 +242,7 @@ Definition tc_to_bool (P : Prop)
 
 (** Throughout this development we use [stdpp_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
+Declare Scope stdpp_scope.
 Delimit Scope stdpp_scope with stdpp.
 Global Open Scope stdpp_scope.
 
@@ -212,10 +274,10 @@ Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope.
 Notation "X ≠@{ A } Y":= (¬X =@{ A } Y)
   (at level 70, only parsing, no associativity) : stdpp_scope.
 
-Hint Extern 0 (_ = _) => reflexivity : core.
-Hint Extern 100 (_ ≠ _) => discriminate : core.
+Global Hint Extern 0 (_ = _) => reflexivity : core.
+Global Hint Extern 100 (_ ≠ _) => discriminate : core.
 
-Instance: ∀ A, PreOrder (=@{A}).
+Global Instance: ∀ A, PreOrder (=@{A}).
 Proof. split; repeat intro; congruence. Qed.
 
 (** ** Setoid equality *)
@@ -223,8 +285,17 @@ Proof. split; repeat intro; congruence. Qed.
 "canonical" equivalence for a type. The typeclass is tied to the \equiv
 symbol. This is based on (Spitters/van der Weegen, 2011). *)
 Class Equiv A := equiv: relation A.
-(* No Hint Mode set because of Coq bug #5735
-Hint Mode Equiv ! : typeclass_instances. *)
+Global Hint Mode Equiv ! : typeclass_instances.
+
+(** We instruct setoid rewriting to infer [equiv] as a relation on
+type [A] when needed. This allows setoid_rewrite to solve constraints
+of shape [Proper (eq ==> ?R) f] using [Proper (eq ==> (equiv (A:=A))) f]
+when an equivalence relation is available on type [A]. We put this instance
+at level 150 so it does not take precedence over Coq's stdlib instances,
+favoring inference of [eq] (all Coq functions are automatically morphisms
+for [eq]). We have [eq] (at 100) < [≡] (at 150) < [⊑] (at 200). *)
+Global Instance equiv_rewrite_relation `{Equiv A} :
+  RewriteRelation (@equiv A _) | 150 := {}.
 
 Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
 Infix "≡@{ A }" := (@equiv A _)
@@ -246,13 +317,17 @@ Notation "X ≢@{ A } Y":= (¬X ≡@{ A } Y)
 (** The type class [LeibnizEquiv] collects setoid equalities that coincide
 with Leibniz equality. We provide the tactic [fold_leibniz] to transform such
 setoid equalities into Leibniz equalities, and [unfold_leibniz] for the
-reverse. *)
-Class LeibnizEquiv A `{Equiv A} := leibniz_equiv x y : x ≡ y → x = y.
-Hint Mode LeibnizEquiv ! - : typeclass_instances.
+reverse.
+
+Various std++ tactics assume that this class is only instantiated if [≡]
+is an equivalence relation. *)
+Class LeibnizEquiv A `{Equiv A} :=
+  leibniz_equiv (x y : A) : x ≡ y → x = y.
+Global Hint Mode LeibnizEquiv ! ! : typeclass_instances.
 
 Lemma leibniz_equiv_iff `{LeibnizEquiv A, !Reflexive (≡@{A})} (x y : A) :
   x ≡ y ↔ x = y.
-Proof. split. apply leibniz_equiv. intros ->; reflexivity. Qed.
+Proof. split; [apply leibniz_equiv|]. intros ->; reflexivity. Qed.
 
 Ltac fold_leibniz := repeat
   match goal with
@@ -274,14 +349,15 @@ Definition equivL {A} : Equiv A := (=).
 (** A [Params f n] instance forces the setoid rewriting mechanism not to
 rewrite in the first [n] arguments of the function [f]. We will declare such
 instances for all operational type classes in this development. *)
-Instance: Params (@equiv) 2 := {}.
+Global Instance: Params (@equiv) 2 := {}.
 
 (** The following instance forces [setoid_replace] to use setoid equality
 (for types that have an [Equiv] instance) rather than the standard Leibniz
 equality. *)
-Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3 := {}.
-Hint Extern 0 (_ ≡ _) => reflexivity : core.
-Hint Extern 0 (_ ≡ _) => symmetry; assumption : core.
+Global Instance equiv_default_relation `{Equiv A} :
+  DefaultRelation (≡@{A}) | 3 := {}.
+Global Hint Extern 0 (_ ≡ _) => reflexivity : core.
+Global Hint Extern 0 (_ ≡ _) => symmetry; assumption : core.
 
 
 (** * Type classes *)
@@ -289,8 +365,8 @@ Hint Extern 0 (_ ≡ _) => symmetry; assumption : core.
 (** This type class by (Spitters/van der Weegen, 2011) collects decidable
 propositions. *)
 Class Decision (P : Prop) := decide : {P} + {¬P}.
-Hint Mode Decision ! : typeclass_instances.
-Arguments decide _ {_} : simpl never, assert.
+Global Hint Mode Decision ! : typeclass_instances.
+Global Arguments decide _ {_} : simpl never, assert.
 
 (** Although [RelDecision R] is just [∀ x y, Decision (R x y)], we make this
 an explicit class instead of a notation for two reasons:
@@ -307,23 +383,23 @@ an explicit class instead of a notation for two reasons:
   Using the [RelDecision], the [f] is hidden under a lambda, which prevents
   unnecessary evaluation. *)
 Class RelDecision {A B} (R : A → B → Prop) :=
-  decide_rel x y :> Decision (R x y).
-Hint Mode RelDecision ! ! ! : typeclass_instances.
-Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
+  decide_rel x y :: Decision (R x y).
+Global Hint Mode RelDecision ! ! ! : typeclass_instances.
+Global Arguments decide_rel {_ _} _ {_} _ _ : simpl never, assert.
 Notation EqDecision A := (RelDecision (=@{A})).
 
 (** ** Inhabited types *)
 (** This type class collects types that are inhabited. *)
 Class Inhabited (A : Type) : Type := populate { inhabitant : A }.
-Hint Mode Inhabited ! : typeclass_instances.
-Arguments populate {_} _ : assert.
+Global Hint Mode Inhabited ! : typeclass_instances.
+Global Arguments populate {_} _ : assert.
 
 (** ** Proof irrelevant types *)
 (** This type class collects types that are proof irrelevant. That means, all
 elements of the type are equal. We use this notion only used for propositions,
 but by universe polymorphism we can generalize it. *)
 Class ProofIrrel (A : Type) : Prop := proof_irrel (x y : A) : x = y.
-Hint Mode ProofIrrel ! : typeclass_instances.
+Global Hint Mode ProofIrrel ! : typeclass_instances.
 
 (** ** Common properties *)
 (** These operational type classes allow us to refer to common mathematical
@@ -335,7 +411,7 @@ Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
     (S : relation C) (f : A → B → C) : Prop :=
   inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2.
 Class Cancel {A B} (S : relation B) (f : A → B) (g : B → A) : Prop :=
-  cancel : ∀ x, S (f (g x)) x.
+  cancel x : S (f (g x)) x.
 Class Surj {A B} (R : relation B) (f : A → B) :=
   surj y : ∃ x, R (f x) y.
 Class IdemP {A} (R : relation A) (f : A → A → A) : Prop :=
@@ -365,22 +441,22 @@ Lemma involutive {A} {R : relation A} (f : A → A) `{Involutive R f} x :
   R (f (f x)) x.
 Proof. auto. Qed.
 
-Arguments irreflexivity {_} _ {_} _ _ : assert.
-Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
-Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert.
-Arguments cancel {_ _ _} _ _ {_} _ : assert.
-Arguments surj {_ _ _} _ {_} _ : assert.
-Arguments idemp {_ _} _ {_} _ : assert.
-Arguments comm {_ _ _} _ {_} _ _ : assert.
-Arguments left_id {_ _} _ _ {_} _ : assert.
-Arguments right_id {_ _} _ _ {_} _ : assert.
-Arguments assoc {_ _} _ {_} _ _ _ : assert.
-Arguments left_absorb {_ _} _ _ {_} _ : assert.
-Arguments right_absorb {_ _} _ _ {_} _ : assert.
-Arguments anti_symm {_ _} _ {_} _ _ _ _ : assert.
-Arguments total {_} _ {_} _ _ : assert.
-Arguments trichotomy {_} _ {_} _ _ : assert.
-Arguments trichotomyT {_} _ {_} _ _ : assert.
+Global Arguments irreflexivity {_} _ {_} _ _ : assert.
+Global Arguments inj {_ _ _ _} _ {_} _ _ _ : assert.
+Global Arguments inj2 {_ _ _ _ _ _} _ {_} _ _ _ _ _: assert.
+Global Arguments cancel {_ _ _} _ _ {_} _ : assert.
+Global Arguments surj {_ _ _} _ {_} _ : assert.
+Global Arguments idemp {_ _} _ {_} _ : assert.
+Global Arguments comm {_ _ _} _ {_} _ _ : assert.
+Global Arguments left_id {_ _} _ _ {_} _ : assert.
+Global Arguments right_id {_ _} _ _ {_} _ : assert.
+Global Arguments assoc {_ _} _ {_} _ _ _ : assert.
+Global Arguments left_absorb {_ _} _ _ {_} _ : assert.
+Global Arguments right_absorb {_ _} _ _ {_} _ : assert.
+Global Arguments anti_symm {_ _} _ {_} _ _ _ _ : assert.
+Global Arguments total {_} _ {_} _ _ : assert.
+Global Arguments trichotomy {_} _ {_} _ _ : assert.
+Global Arguments trichotomyT {_} _ {_} _ _ : assert.
 
 Lemma not_symmetry `{R : relation A, !Symmetric R} x y : ¬R x y → ¬R y x.
 Proof. intuition. Qed.
@@ -399,9 +475,9 @@ Proof. intros HR' HR''. destruct (inj2 f x1 y1 x2 y2); auto. Qed.
 Lemma inj_iff {A B} {R : relation A} {S : relation B} (f : A → B)
   `{!Inj R S f} `{!Proper (R ==> S) f} x y : S (f x) (f y) ↔ R x y.
 Proof. firstorder. Qed.
-Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 f} y : Inj R1 R3 (λ x, f x y).
+Global Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 f} y : Inj R1 R3 (λ x, f x y).
 Proof. repeat intro; edestruct (inj2 f); eauto. Qed.
-Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x).
+Global Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 f} x : Inj R2 R3 (f x).
 Proof. repeat intro; edestruct (inj2 f); eauto. Qed.
 
 Lemma cancel_inj `{Cancel A B R1 f g, !Equivalence R1, !Proper (R2 ==> R1) f} :
@@ -434,18 +510,22 @@ Proof. auto. Qed.
 (** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary
 relation [R] instead of [⊆] to support multiple orders on the same type. *)
 Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y ∧ ¬R Y X.
-Instance: Params (@strict) 2 := {}.
+Global Instance: Params (@strict) 2 := {}.
+
 Class PartialOrder {A} (R : relation A) : Prop := {
-  partial_order_pre :> PreOrder R;
-  partial_order_anti_symm :> AntiSymm (=) R
+  partial_order_pre :: PreOrder R;
+  partial_order_anti_symm :: AntiSymm (=) R
 }.
+Global Hint Mode PartialOrder ! ! : typeclass_instances.
+
 Class TotalOrder {A} (R : relation A) : Prop := {
-  total_order_partial :> PartialOrder R;
-  total_order_trichotomy :> Trichotomy (strict R)
+  total_order_partial :: PartialOrder R;
+  total_order_trichotomy :: Trichotomy (strict R)
 }.
+Global Hint Mode TotalOrder ! ! : typeclass_instances.
 
 (** * Logic *)
-Instance prop_inhabited : Inhabited Prop := populate True.
+Global Instance prop_inhabited : Inhabited Prop := populate True.
 
 Notation "(∧)" := and (only parsing) : stdpp_scope.
 Notation "( A ∧.)" := (and A) (only parsing) : stdpp_scope.
@@ -459,8 +539,8 @@ Notation "(↔)" := iff (only parsing) : stdpp_scope.
 Notation "( A ↔.)" := (iff A) (only parsing) : stdpp_scope.
 Notation "(.↔ B )" := (λ A, A ↔ B) (only parsing) : stdpp_scope.
 
-Hint Extern 0 (_ ↔ _) => reflexivity : core.
-Hint Extern 0 (_ ↔ _) => symmetry; assumption : core.
+Global Hint Extern 0 (_ ↔ _) => reflexivity : core.
+Global Hint Extern 0 (_ ↔ _) => symmetry; assumption : core.
 
 Lemma or_l P Q : ¬Q → P ∨ Q ↔ P.
 Proof. tauto. Qed.
@@ -479,43 +559,43 @@ Lemma exist_proper {A} (P Q : A → Prop) :
   (∀ x, P x ↔ Q x) → (∃ x, P x) ↔ (∃ x, Q x).
 Proof. firstorder. Qed.
 
-Instance: Comm (↔) (=@{A}).
+Global Instance eq_comm {A} : Comm (↔) (=@{A}).
 Proof. red; intuition. Qed.
-Instance: Comm (↔) (λ x y, y =@{A} x).
+Global Instance flip_eq_comm {A} : Comm (↔) (λ x y, y =@{A} x).
 Proof. red; intuition. Qed.
-Instance: Comm (↔) (↔).
+Global Instance iff_comm : Comm (↔) (↔).
 Proof. red; intuition. Qed.
-Instance: Comm (↔) (∧).
+Global Instance and_comm : Comm (↔) (∧).
 Proof. red; intuition. Qed.
-Instance: Assoc (↔) (∧).
+Global Instance and_assoc : Assoc (↔) (∧).
 Proof. red; intuition. Qed.
-Instance: IdemP (↔) (∧).
+Global Instance and_idemp : IdemP (↔) (∧).
 Proof. red; intuition. Qed.
-Instance: Comm (↔) (∨).
+Global Instance or_comm : Comm (↔) (∨).
 Proof. red; intuition. Qed.
-Instance: Assoc (↔) (∨).
+Global Instance or_assoc : Assoc (↔) (∨).
 Proof. red; intuition. Qed.
-Instance: IdemP (↔) (∨).
+Global Instance or_idemp : IdemP (↔) (∨).
 Proof. red; intuition. Qed.
-Instance: LeftId (↔) True (∧).
+Global Instance True_and : LeftId (↔) True (∧).
 Proof. red; intuition. Qed.
-Instance: RightId (↔) True (∧).
+Global Instance and_True : RightId (↔) True (∧).
 Proof. red; intuition. Qed.
-Instance: LeftAbsorb (↔) False (∧).
+Global Instance False_and : LeftAbsorb (↔) False (∧).
 Proof. red; intuition. Qed.
-Instance: RightAbsorb (↔) False (∧).
+Global Instance and_False : RightAbsorb (↔) False (∧).
 Proof. red; intuition. Qed.
-Instance: LeftId (↔) False (∨).
+Global Instance False_or : LeftId (↔) False (∨).
 Proof. red; intuition. Qed.
-Instance: RightId (↔) False (∨).
+Global Instance or_False : RightId (↔) False (∨).
 Proof. red; intuition. Qed.
-Instance: LeftAbsorb (↔) True (∨).
+Global Instance True_or : LeftAbsorb (↔) True (∨).
 Proof. red; intuition. Qed.
-Instance: RightAbsorb (↔) True (∨).
+Global Instance or_True : RightAbsorb (↔) True (∨).
 Proof. red; intuition. Qed.
-Instance: LeftId (↔) True impl.
+Global Instance True_impl : LeftId (↔) True impl.
 Proof. unfold impl. red; intuition. Qed.
-Instance: RightAbsorb (↔) True impl.
+Global Instance impl_True : RightAbsorb (↔) True impl.
 Proof. unfold impl. red; intuition. Qed.
 
 
@@ -535,54 +615,54 @@ Notation "(∘)" := compose (only parsing) : stdpp_scope.
 Notation "( f ∘.)" := (compose f) (only parsing) : stdpp_scope.
 Notation "(.∘ f )" := (λ g, compose g f) (only parsing) : stdpp_scope.
 
-Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A → B) :=
+Global Instance impl_inhabited {A} `{Inhabited B} : Inhabited (A → B) :=
   populate (λ _, inhabitant).
 
 (** Ensure that [simpl] unfolds [id], [compose], and [flip] when fully
 applied. *)
-Arguments id _ _ / : assert.
-Arguments compose _ _ _ _ _ _ / : assert.
-Arguments flip _ _ _ _ _ _ / : assert.
-Arguments const _ _ _ _ / : assert.
-Typeclasses Transparent id compose flip const.
+Global Arguments id _ _ / : assert.
+Global Arguments compose _ _ _ _ _ _ / : assert.
+Global Arguments flip _ _ _ _ _ _ / : assert.
+Global Arguments const _ _ _ _ / : assert.
+Global Typeclasses Transparent id compose flip const.
 
 Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' :=
   g ∘ h ∘ f.
 
-Instance const_proper `{R1 : relation A, R2 : relation B} (x : B) :
+Global Instance const_proper `{R1 : relation A, R2 : relation B} (x : B) :
   Reflexive R2 → Proper (R1 ==> R2) (λ _, x).
 Proof. intros ? y1 y2; reflexivity. Qed.
 
-Instance id_inj {A} : Inj (=) (=) (@id A).
+Global Instance id_inj {A} : Inj (=) (=) (@id A).
 Proof. intros ??; auto. Qed.
-Instance compose_inj {A B C} R1 R2 R3 (f : A → B) (g : B → C) :
+Global Instance compose_inj {A B C} R1 R2 R3 (f : A → B) (g : B → C) :
   Inj R1 R2 f → Inj R2 R3 g → Inj R1 R3 (g ∘ f).
 Proof. red; intuition. Qed.
 
-Instance id_surj {A} : Surj (=) (@id A).
+Global Instance id_surj {A} : Surj (=) (@id A).
 Proof. intros y; exists y; reflexivity. Qed.
-Instance compose_surj {A B C} R (f : A → B) (g : B → C) :
+Global Instance compose_surj {A B C} R (f : A → B) (g : B → C) :
   Surj (=) f → Surj R g → Surj R (g ∘ f).
 Proof.
   intros ?? x. unfold compose. destruct (surj g x) as [y ?].
   destruct (surj f y) as [z ?]. exists z. congruence.
 Qed.
 
-Instance id_comm {A B} (x : B) : Comm (=) (λ _ _ : A, x).
+Global Instance const2_comm {A B} (x : B) : Comm (=) (λ _ _ : A, x).
 Proof. intros ?; reflexivity. Qed.
-Instance id_assoc {A} (x : A) : Assoc (=) (λ _ _ : A, x).
+Global Instance const2_assoc {A} (x : A) : Assoc (=) (λ _ _ : A, x).
 Proof. intros ???; reflexivity. Qed.
-Instance const1_assoc {A} : Assoc (=) (λ x _ : A, x).
+Global Instance id1_assoc {A} : Assoc (=) (λ x _ : A, x).
 Proof. intros ???; reflexivity. Qed.
-Instance const2_assoc {A} : Assoc (=) (λ _ x : A, x).
+Global Instance id2_assoc {A} : Assoc (=) (λ _ x : A, x).
 Proof. intros ???; reflexivity. Qed.
-Instance const1_idemp {A} : IdemP (=) (λ x _ : A, x).
+Global Instance id1_idemp {A} : IdemP (=) (λ x _ : A, x).
 Proof. intros ?; reflexivity. Qed.
-Instance const2_idemp {A} : IdemP (=) (λ _ x : A, x).
+Global Instance id2_idemp {A} : IdemP (=) (λ _ x : A, x).
 Proof. intros ?; reflexivity. Qed.
 
 (** ** Lists *)
-Instance list_inhabited {A} : Inhabited (list A) := populate [].
+Global Instance list_inhabited {A} : Inhabited (list A) := populate [].
 
 Definition zip_with {A B C} (f : A → B → C) : list A → list B → list C :=
   fix go l1 l2 :=
@@ -592,20 +672,20 @@ Notation zip := (zip_with pair).
 (** ** Booleans *)
 (** The following coercion allows us to use Booleans as propositions. *)
 Coercion Is_true : bool >-> Sortclass.
-Hint Unfold Is_true : core.
-Hint Immediate Is_true_eq_left : core.
-Hint Resolve orb_prop_intro andb_prop_intro : core.
+Global Hint Unfold Is_true : core.
+Global Hint Immediate Is_true_eq_left : core.
+Global Hint Resolve orb_prop_intro andb_prop_intro : core.
 Notation "(&&)" := andb (only parsing).
 Notation "(||)" := orb (only parsing).
 Infix "&&*" := (zip_with (&&)) (at level 40).
 Infix "||*" := (zip_with (||)) (at level 50).
 
-Instance bool_inhabated : Inhabited bool := populate true.
+Global Instance bool_inhabated : Inhabited bool := populate true.
 
 Definition bool_le (β1 β2 : bool) : Prop := negb β1 || β2.
 Infix "=.>" := bool_le (at level 70).
 Infix "=.>*" := (Forall2 bool_le) (at level 70).
-Instance: PartialOrder bool_le.
+Global Instance: PartialOrder bool_le.
 Proof. repeat split; repeat intros [|]; compute; tauto. Qed.
 
 Lemma andb_True b1 b2 : b1 && b2 ↔ b1 ∧ b2.
@@ -614,172 +694,295 @@ Lemma orb_True b1 b2 : b1 || b2 ↔ b1 ∨ b2.
 Proof. destruct b1, b2; simpl; tauto. Qed.
 Lemma negb_True b : negb b ↔ ¬b.
 Proof. destruct b; simpl; tauto. Qed.
-Lemma Is_true_false (b : bool) : b = false → ¬b.
-Proof. now intros -> ?. Qed.
+Lemma Is_true_true (b : bool) : b ↔ b = true.
+Proof. now destruct b. Qed.
+Lemma Is_true_true_1 (b : bool) : b → b = true.
+Proof. apply Is_true_true. Qed.
+Lemma Is_true_true_2 (b : bool) : b = true → b.
+Proof. apply Is_true_true. Qed.
+Lemma Is_true_false (b : bool) : ¬ b ↔ b = false.
+Proof. now destruct b; simpl. Qed.
+Lemma Is_true_false_1 (b : bool) : ¬b → b = false.
+Proof. apply Is_true_false. Qed.
+Lemma Is_true_false_2 (b : bool) : b = false → ¬b.
+Proof. apply Is_true_false. Qed.
 
 (** ** Unit *)
-Instance unit_equiv : Equiv unit := λ _ _, True.
-Instance unit_equivalence : Equivalence (≡@{unit}).
+Global Instance unit_equiv : Equiv unit := λ _ _, True.
+Global Instance unit_equivalence : Equivalence (≡@{unit}).
 Proof. repeat split. Qed.
-Instance unit_leibniz : LeibnizEquiv unit.
+Global Instance unit_leibniz : LeibnizEquiv unit.
 Proof. intros [] []; reflexivity. Qed.
-Instance unit_inhabited: Inhabited unit := populate ().
+Global Instance unit_inhabited: Inhabited unit := populate ().
 
 (** ** Empty *)
-Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True.
-Instance Empty_set_equivalence : Equivalence (≡@{Empty_set}).
+Global Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True.
+Global Instance Empty_set_equivalence : Equivalence (≡@{Empty_set}).
 Proof. repeat split. Qed.
-Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
+Global Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
 Proof. intros [] []; reflexivity. Qed.
 
 (** ** Products *)
 Notation "( x ,.)" := (pair x) (only parsing) : stdpp_scope.
 Notation "(., y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
 
-Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
-Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").
+Notation "p .1" := (fst p).
+Notation "p .2" := (snd p).
 
-Instance: Params (@pair) 2 := {}.
-Instance: Params (@fst) 2 := {}.
-Instance: Params (@snd) 2 := {}.
+Global Instance: Params (@pair) 2 := {}.
+Global Instance: Params (@fst) 2 := {}.
+Global Instance: Params (@snd) 2 := {}.
 
-Notation curry := prod_curry.
-Notation uncurry := prod_uncurry.
-Definition curry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=
+Global Instance: Params (@curry) 3 := {}.
+Global Instance: Params (@uncurry) 3 := {}.
+
+Definition uncurry3 {A B C D} (f : A → B → C → D) (p : A * B * C) : D :=
   let '(a,b,c) := p in f a b c.
-Definition curry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D) : E :=
+Global Instance: Params (@uncurry3) 4 := {}.
+Definition uncurry4 {A B C D E} (f : A → B → C → D → E) (p : A * B * C * D) : E :=
   let '(a,b,c,d) := p in f a b c d.
+Global Instance: Params (@uncurry4) 5 := {}.
 
-Definition uncurry3 {A B C D} (f : A * B * C → D) (a : A) (b : B) (c : C) : D :=
+Definition curry3 {A B C D} (f : A * B * C → D) (a : A) (b : B) (c : C) : D :=
   f (a, b, c).
-Definition uncurry4 {A B C D E} (f : A * B * C * D → E)
+Global Instance: Params (@curry3) 4 := {}.
+Definition curry4 {A B C D E} (f : A * B * C * D → E)
   (a : A) (b : B) (c : C) (d : D) : E := f (a, b, c, d).
+Global Instance: Params (@curry4) 5 := {}.
 
 Definition prod_map {A A' B B'} (f: A → A') (g: B → B') (p : A * B) : A' * B' :=
   (f (p.1), g (p.2)).
-Arguments prod_map {_ _ _ _} _ _ !_ / : assert.
+Global Instance: Params (@prod_map) 4 := {}.
+Global Arguments prod_map {_ _ _ _} _ _ !_ / : assert.
 
 Definition prod_zip {A A' A'' B B' B''} (f : A → A' → A'') (g : B → B' → B'')
     (p : A * B) (q : A' * B') : A'' * B'' := (f (p.1) (q.1), g (p.2) (q.2)).
-Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ / : assert.
+Global Instance: Params (@prod_zip) 6 := {}.
+Global Arguments prod_zip {_ _ _ _ _ _} _ _ !_ !_ / : assert.
+
+Definition prod_swap {A B} (p : A * B) : B * A := (p.2, p.1).
+Global Arguments prod_swap {_ _} !_ /.
+Global Instance: Params (@prod_swap) 2 := {}.
 
-Instance prod_inhabited {A B} (iA : Inhabited A)
+Global Instance prod_inhabited {A B} (iA : Inhabited A)
     (iB : Inhabited B) : Inhabited (A * B) :=
   match iA, iB with populate x, populate y => populate (x,y) end.
 
-Instance pair_inj : Inj2 (=) (=) (=) (@pair A B).
+(** Note that we need eta for products for the [uncurry_curry] lemmas to hold
+in non-applied form ([uncurry (curry f) = f]). *)
+Lemma curry_uncurry {A B C} (f : A → B → C) : curry (uncurry f) = f.
+Proof. reflexivity. Qed.
+Lemma uncurry_curry {A B C} (f : A * B → C) p : uncurry (curry f) p = f p.
+Proof. destruct p; reflexivity. Qed.
+Lemma curry3_uncurry3 {A B C D} (f : A → B → C → D) : curry3 (uncurry3 f) = f.
+Proof. reflexivity. Qed.
+Lemma uncurry3_curry3 {A B C D} (f : A * B * C → D) p :
+  uncurry3 (curry3 f) p = f p.
+Proof. destruct p as [[??] ?]; reflexivity. Qed.
+Lemma curry4_uncurry4 {A B C D E} (f : A → B → C → D → E) :
+  curry4 (uncurry4 f) = f.
+Proof. reflexivity. Qed.
+Lemma uncurry4_curry4 {A B C D E} (f : A * B * C * D → E) p :
+  uncurry4 (curry4 f) p = f p.
+Proof. destruct p as [[[??] ?] ?]; reflexivity. Qed.
+
+(** [pair_eq] as a name is more consistent with our usual naming. *)
+Lemma pair_eq {A B} (a1 a2 : A) (b1 b2 : B) :
+  (a1, b1) = (a2, b2) ↔ a1 = a2 ∧ b1 = b2.
+Proof. apply pair_equal_spec. Qed.
+
+Global Instance pair_inj {A B} : Inj2 (=) (=) (=) (@pair A B).
 Proof. injection 1; auto. Qed.
-Instance prod_map_inj {A A' B B'} (f : A → A') (g : B → B') :
+Global Instance prod_map_inj {A A' B B'} (f : A → A') (g : B → B') :
   Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (prod_map f g).
 Proof.
   intros ?? [??] [??] ?; simpl in *; f_equal;
     [apply (inj f)|apply (inj g)]; congruence.
 Qed.
 
+Global Instance prod_swap_cancel {A B} :
+  Cancel (=) (@prod_swap A B) (@prod_swap B A).
+Proof. intros [??]; reflexivity. Qed.
+Global Instance prod_swap_inj {A B} : Inj (=) (=) (@prod_swap A B).
+Proof. apply cancel_inj. Qed.
+Global Instance prod_swap_surj {A B} : Surj (=) (@prod_swap A B).
+Proof. apply cancel_surj. Qed.
+
 Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
   relation (A * B) := λ x y, R1 (x.1) (y.1) ∧ R2 (x.2) (y.2).
+
 Section prod_relation.
-  Context `{R1 : relation A, R2 : relation B}.
+  Context `{RA : relation A, RB : relation B}.
+
   Global Instance prod_relation_refl :
-    Reflexive R1 → Reflexive R2 → Reflexive (prod_relation R1 R2).
+    Reflexive RA → Reflexive RB → Reflexive (prod_relation RA RB).
   Proof. firstorder eauto. Qed.
   Global Instance prod_relation_sym :
-    Symmetric R1 → Symmetric R2 → Symmetric (prod_relation R1 R2).
+    Symmetric RA → Symmetric RB → Symmetric (prod_relation RA RB).
   Proof. firstorder eauto. Qed.
   Global Instance prod_relation_trans :
-    Transitive R1 → Transitive R2 → Transitive (prod_relation R1 R2).
+    Transitive RA → Transitive RB → Transitive (prod_relation RA RB).
   Proof. firstorder eauto. Qed.
   Global Instance prod_relation_equiv :
-    Equivalence R1 → Equivalence R2 → Equivalence (prod_relation R1 R2).
+    Equivalence RA → Equivalence RB → Equivalence (prod_relation RA RB).
   Proof. split; apply _. Qed.
 
-  Global Instance pair_proper' : Proper (R1 ==> R2 ==> prod_relation R1 R2) pair.
+  Global Instance pair_proper' : Proper (RA ==> RB ==> prod_relation RA RB) pair.
   Proof. firstorder eauto. Qed.
-  Global Instance pair_inj' : Inj2 R1 R2 (prod_relation R1 R2) pair.
+  Global Instance pair_inj' : Inj2 RA RB (prod_relation RA RB) pair.
   Proof. inversion_clear 1; eauto. Qed.
-  Global Instance fst_proper' : Proper (prod_relation R1 R2 ==> R1) fst.
+  Global Instance fst_proper' : Proper (prod_relation RA RB ==> RA) fst.
   Proof. firstorder eauto. Qed.
-  Global Instance snd_proper' : Proper (prod_relation R1 R2 ==> R2) snd.
+  Global Instance snd_proper' : Proper (prod_relation RA RB ==> RB) snd.
+  Proof. firstorder eauto. Qed.
+
+  Global Instance prod_swap_proper' :
+    Proper (prod_relation RA RB ==> prod_relation RB RA) prod_swap.
   Proof. firstorder eauto. Qed.
-End prod_relation.
 
-Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) := prod_relation (≡) (≡).
-Instance pair_proper `{Equiv A, Equiv B} :
-  Proper ((≡) ==> (≡) ==> (≡)) (@pair A B) := _.
-Instance pair_equiv_inj `{Equiv A, Equiv B} : Inj2 (≡) (≡) (≡) (@pair A B) := _.
-Instance fst_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@fst A B) := _.
-Instance snd_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@snd A B) := _.
-Typeclasses Opaque prod_equiv.
+  Global Instance curry_proper' `{RC : relation C} :
+    Proper ((prod_relation RA RB ==> RC) ==> RA ==> RB ==> RC) curry.
+  Proof. firstorder eauto. Qed.
+  Global Instance uncurry_proper' `{RC : relation C} :
+    Proper ((RA ==> RB ==> RC) ==> prod_relation RA RB ==> RC) uncurry.
+  Proof. intros f1 f2 Hf [x1 y1] [x2 y2] []; apply Hf; assumption. Qed.
 
-Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} : LeibnizEquiv (A * B).
+  Global Instance curry3_proper' `{RC : relation C, RD : relation D} :
+    Proper ((prod_relation (prod_relation RA RB) RC ==> RD) ==>
+            RA ==> RB ==> RC ==> RD) curry3.
+  Proof. firstorder eauto. Qed.
+  Global Instance uncurry3_proper' `{RC : relation C, RD : relation D} :
+    Proper ((RA ==> RB ==> RC ==> RD) ==>
+            prod_relation (prod_relation RA RB) RC ==> RD) uncurry3.
+  Proof. intros f1 f2 Hf [[??] ?] [[??] ?] [[??] ?]; apply Hf; assumption. Qed.
+
+  Global Instance curry4_proper' `{RC : relation C, RD : relation D, RE : relation E} :
+    Proper ((prod_relation (prod_relation (prod_relation RA RB) RC) RD ==> RE) ==>
+            RA ==> RB ==> RC ==> RD ==> RE) curry4.
+  Proof. firstorder eauto. Qed.
+  Global Instance uncurry4_proper' `{RC : relation C, RD : relation D, RE : relation E} :
+    Proper ((RA ==> RB ==> RC ==> RD ==> RE) ==>
+            prod_relation (prod_relation (prod_relation RA RB) RC) RD ==> RE) uncurry4.
+  Proof.
+    intros f1 f2 Hf [[[??] ?] ?] [[[??] ?] ?] [[[??] ?] ?]; apply Hf; assumption.
+  Qed.
+End prod_relation.
+
+Global Instance prod_equiv `{Equiv A,Equiv B} : Equiv (A * B) :=
+  prod_relation (≡) (≡).
+
+(** Below we make [prod_equiv] type class opaque, so we first lift all
+instances *)
+Section prod_setoid.
+  Context `{Equiv A, Equiv B}.
+
+  Global Instance prod_equivalence :
+    Equivalence (≡@{A}) → Equivalence (≡@{B}) → Equivalence (≡@{A * B}) := _.
+
+  Global Instance pair_proper : Proper ((≡) ==> (≡) ==> (≡@{A*B})) pair := _.
+  Global Instance pair_equiv_inj : Inj2 (≡) (≡) (≡@{A*B}) pair := _.
+  Global Instance fst_proper : Proper ((≡@{A*B}) ==> (≡)) fst := _.
+  Global Instance snd_proper : Proper ((≡@{A*B}) ==> (≡)) snd := _.
+
+  Global Instance prod_swap_proper :
+    Proper ((≡@{A*B}) ==> (≡@{B*A})) prod_swap := _.
+
+  Global Instance curry_proper `{Equiv C} :
+    Proper (((≡@{A*B}) ==> (≡@{C})) ==> (≡) ==> (≡) ==> (≡)) curry := _.
+  Global Instance uncurry_proper `{Equiv C} :
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡@{A*B}) ==> (≡@{C})) uncurry := _.
+
+  Global Instance curry3_proper `{Equiv C, Equiv D} :
+    Proper (((≡@{A*B*C}) ==> (≡@{D})) ==>
+            (≡) ==> (≡) ==> (≡) ==> (≡)) curry3 := _.
+  Global Instance uncurry3_proper `{Equiv C, Equiv D} :
+    Proper (((≡) ==> (≡) ==> (≡) ==> (≡)) ==>
+            (≡@{A*B*C}) ==> (≡@{D})) uncurry3 := _.
+
+  Global Instance curry4_proper `{Equiv C, Equiv D, Equiv E} :
+    Proper (((≡@{A*B*C*D}) ==> (≡@{E})) ==>
+            (≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) curry4 := _.
+  Global Instance uncurry4_proper `{Equiv C, Equiv D, Equiv E} :
+    Proper (((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) ==>
+            (≡@{A*B*C*D}) ==> (≡@{E})) uncurry4 := _.
+
+  Lemma pair_equiv (a1 a2 : A) (b1 b2 : B) :
+    (a1, b1) ≡ (a2, b2) ↔ a1 ≡ a2 ∧ b1 ≡ b2.
+  Proof. reflexivity. Qed.
+End prod_setoid.
+
+Global Typeclasses Opaque prod_equiv.
+
+Global Instance prod_leibniz `{LeibnizEquiv A, LeibnizEquiv B} :
+  LeibnizEquiv (A * B).
 Proof. intros [??] [??] [??]; f_equal; apply leibniz_equiv; auto. Qed.
 
 (** ** Sums *)
 Definition sum_map {A A' B B'} (f: A → A') (g: B → B') (xy : A + B) : A' + B' :=
   match xy with inl x => inl (f x) | inr y => inr (g y) end.
-Arguments sum_map {_ _ _ _} _ _ !_ / : assert.
+Global Arguments sum_map {_ _ _ _} _ _ !_ / : assert.
 
-Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
+Global Instance sum_inhabited_l {A B} (iA : Inhabited A) : Inhabited (A + B) :=
   match iA with populate x => populate (inl x) end.
-Instance sum_inhabited_r {A B} (iB : Inhabited A) : Inhabited (A + B) :=
-  match iB with populate y => populate (inl y) end.
+Global Instance sum_inhabited_r {A B} (iB : Inhabited B) : Inhabited (A + B) :=
+  match iB with populate y => populate (inr y) end.
 
-Instance inl_inj : Inj (=) (=) (@inl A B).
+Global Instance inl_inj {A B} : Inj (=) (=) (@inl A B).
 Proof. injection 1; auto. Qed.
-Instance inr_inj : Inj (=) (=) (@inr A B).
+Global Instance inr_inj {A B} : Inj (=) (=) (@inr A B).
 Proof. injection 1; auto. Qed.
 
-Instance sum_map_inj {A A' B B'} (f : A → A') (g : B → B') :
+Global Instance sum_map_inj {A A' B B'} (f : A → A') (g : B → B') :
   Inj (=) (=) f → Inj (=) (=) g → Inj (=) (=) (sum_map f g).
 Proof. intros ?? [?|?] [?|?] [=]; f_equal; apply (inj _); auto. Qed.
 
 Inductive sum_relation {A B}
-     (R1 : relation A) (R2 : relation B) : relation (A + B) :=
-  | inl_related x1 x2 : R1 x1 x2 → sum_relation R1 R2 (inl x1) (inl x2)
-  | inr_related y1 y2 : R2 y1 y2 → sum_relation R1 R2 (inr y1) (inr y2).
+     (RA : relation A) (RB : relation B) : relation (A + B) :=
+  | inl_related x1 x2 : RA x1 x2 → sum_relation RA RB (inl x1) (inl x2)
+  | inr_related y1 y2 : RB y1 y2 → sum_relation RA RB (inr y1) (inr y2).
 
 Section sum_relation.
-  Context `{R1 : relation A, R2 : relation B}.
+  Context `{RA : relation A, RB : relation B}.
   Global Instance sum_relation_refl :
-    Reflexive R1 → Reflexive R2 → Reflexive (sum_relation R1 R2).
+    Reflexive RA → Reflexive RB → Reflexive (sum_relation RA RB).
   Proof. intros ?? [?|?]; constructor; reflexivity. Qed.
   Global Instance sum_relation_sym :
-    Symmetric R1 → Symmetric R2 → Symmetric (sum_relation R1 R2).
+    Symmetric RA → Symmetric RB → Symmetric (sum_relation RA RB).
   Proof. destruct 3; constructor; eauto. Qed.
   Global Instance sum_relation_trans :
-    Transitive R1 → Transitive R2 → Transitive (sum_relation R1 R2).
+    Transitive RA → Transitive RB → Transitive (sum_relation RA RB).
   Proof. destruct 3; inversion_clear 1; constructor; eauto. Qed.
   Global Instance sum_relation_equiv :
-    Equivalence R1 → Equivalence R2 → Equivalence (sum_relation R1 R2).
+    Equivalence RA → Equivalence RB → Equivalence (sum_relation RA RB).
   Proof. split; apply _. Qed.
-  Global Instance inl_proper' : Proper (R1 ==> sum_relation R1 R2) inl.
+  Global Instance inl_proper' : Proper (RA ==> sum_relation RA RB) inl.
   Proof. constructor; auto. Qed.
-  Global Instance inr_proper' : Proper (R2 ==> sum_relation R1 R2) inr.
+  Global Instance inr_proper' : Proper (RB ==> sum_relation RA RB) inr.
   Proof. constructor; auto. Qed.
-  Global Instance inl_inj' : Inj R1 (sum_relation R1 R2) inl.
+  Global Instance inl_inj' : Inj RA (sum_relation RA RB) inl.
   Proof. inversion_clear 1; auto. Qed.
-  Global Instance inr_inj' : Inj R2 (sum_relation R1 R2) inr.
+  Global Instance inr_inj' : Inj RB (sum_relation RA RB) inr.
   Proof. inversion_clear 1; auto. Qed.
 End sum_relation.
 
-Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation (≡) (≡).
-Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B) := _.
-Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B) := _.
-Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _.
-Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _.
-Typeclasses Opaque sum_equiv.
+Global Instance sum_equiv `{Equiv A, Equiv B} : Equiv (A + B) := sum_relation (≡) (≡).
+Global Instance inl_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inl A B) := _.
+Global Instance inr_proper `{Equiv A, Equiv B} : Proper ((≡) ==> (≡)) (@inr A B) := _.
+Global Instance inl_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inl A B) := _.
+Global Instance inr_equiv_inj `{Equiv A, Equiv B} : Inj (≡) (≡) (@inr A B) := _.
+Global Typeclasses Opaque sum_equiv.
 
 (** ** Option *)
-Instance option_inhabited {A} : Inhabited (option A) := populate None.
+Global Instance option_inhabited {A} : Inhabited (option A) := populate None.
 
 (** ** Sigma types *)
-Arguments existT {_ _} _ _ : assert.
-Arguments projT1 {_ _} _ : assert.
-Arguments projT2 {_ _} _ : assert.
+Global Arguments existT {_ _} _ _ : assert.
+Global Arguments projT1 {_ _} _ : assert.
+Global Arguments projT2 {_ _} _ : assert.
 
-Arguments exist {_} _ _ _ : assert.
-Arguments proj1_sig {_ _} _ : assert.
-Arguments proj2_sig {_ _} _ : assert.
+Global Arguments exist {_} _ _ _ : assert.
+Global Arguments proj1_sig {_ _} _ : assert.
+Global Arguments proj2_sig {_ _} _ : assert.
 Notation "x ↾ p" := (exist _ x p) (at level 20) : stdpp_scope.
 Notation "` x" := (proj1_sig x) (at level 10, format "` x") : stdpp_scope.
 
@@ -797,7 +1000,7 @@ Section sig_map.
     apply (inj f) in Hxy; subst. rewrite (proof_irrel _ Hy). auto.
   Qed.
 End sig_map.
-Arguments sig_map _ _ _ _ _ _ !_ / : assert.
+Global Arguments sig_map _ _ _ _ _ _ !_ / : assert.
 
 Definition proj1_ex {P : Prop} {Q : P → Prop} (p : ∃ x, Q x) : P :=
   let '(ex_intro _ x _) := p in x.
@@ -810,74 +1013,63 @@ relations on sets: the empty set [∅], the union [(∪)],
 intersection [(∩)], and difference [(∖)], the singleton [{[_]}], the subset
 [(⊆)] and element of [(∈)] relation, and disjointess [(##)]. *)
 Class Empty A := empty: A.
-Hint Mode Empty ! : typeclass_instances.
+Global Hint Mode Empty ! : typeclass_instances.
 Notation "∅" := empty (format "∅") : stdpp_scope.
 
-Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
+Global Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
 
 Class Union A := union: A → A → A.
-Hint Mode Union ! : typeclass_instances.
-Instance: Params (@union) 2 := {}.
+Global Hint Mode Union ! : typeclass_instances.
+Global Instance: Params (@union) 2 := {}.
 Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
 Notation "(∪)" := union (only parsing) : stdpp_scope.
 Notation "( x ∪.)" := (union x) (only parsing) : stdpp_scope.
 Notation "(.∪ x )" := (λ y, union y x) (only parsing) : stdpp_scope.
 Infix "∪*" := (zip_with (∪)) (at level 50, left associativity) : stdpp_scope.
 Notation "(∪*)" := (zip_with (∪)) (only parsing) : stdpp_scope.
-Infix "∪**" := (zip_with (zip_with (∪)))
-  (at level 50, left associativity) : stdpp_scope.
-Infix "∪*∪**" := (zip_with (prod_zip (∪) (∪*)))
-  (at level 50, left associativity) : stdpp_scope.
 
 Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪) ∅.
-Arguments union_list _ _ _ !_ / : assert.
+Global Arguments union_list _ _ _ !_ / : assert.
 Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
 
-Class DisjUnion A := disj_union: A → A → A.
-Hint Mode DisjUnion ! : typeclass_instances.
-Instance: Params (@disj_union) 2 := {}.
-Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
-Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
-Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
-Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
-
 Class Intersection A := intersection: A → A → A.
-Hint Mode Intersection ! : typeclass_instances.
-Instance: Params (@intersection) 2 := {}.
+Global Hint Mode Intersection ! : typeclass_instances.
+Global Instance: Params (@intersection) 2 := {}.
 Infix "∩" := intersection (at level 40) : stdpp_scope.
 Notation "(∩)" := intersection (only parsing) : stdpp_scope.
 Notation "( x ∩.)" := (intersection x) (only parsing) : stdpp_scope.
 Notation "(.∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
 
 Class Difference A := difference: A → A → A.
-Hint Mode Difference ! : typeclass_instances.
-Instance: Params (@difference) 2 := {}.
+Global Hint Mode Difference ! : typeclass_instances.
+Global Instance: Params (@difference) 2 := {}.
 Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
 Notation "(∖)" := difference (only parsing) : stdpp_scope.
 Notation "( x ∖.)" := (difference x) (only parsing) : stdpp_scope.
 Notation "(.∖ x )" := (λ y, difference y x) (only parsing) : stdpp_scope.
 Infix "∖*" := (zip_with (∖)) (at level 40, left associativity) : stdpp_scope.
 Notation "(∖*)" := (zip_with (∖)) (only parsing) : stdpp_scope.
-Infix "∖**" := (zip_with (zip_with (∖)))
-  (at level 40, left associativity) : stdpp_scope.
-Infix "∖*∖**" := (zip_with (prod_zip (∖) (∖*)))
-  (at level 50, left associativity) : stdpp_scope.
+
+(** The operation [cprod X Y] gives the Cartesian product of set-like structures
+[X] and [Y], i.e., [cprod X Y := { (x,y) | x ∈ X, y ∈ Y }]. The implementation/
+instance depends on the representation of the set. *)
+Class CProd A B C := cprod : A → B → C.
+Global Hint Mode CProd ! ! - : typeclass_instances.
+Global Instance: Params (@cprod) 4 := {}.
+(** We do not have a notation for [cprod] (yet) since this operation seems
+not commonly enough used. *)
 
 Class Singleton A B := singleton: A → B.
-Hint Mode Singleton - ! : typeclass_instances.
-Instance: Params (@singleton) 3 := {}.
+Global Hint Mode Singleton - ! : typeclass_instances.
+Global Instance: Params (@singleton) 3 := {}.
 Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope.
 Notation "{[ x ; y ; .. ; z ]}" :=
   (union .. (union (singleton x) (singleton y)) .. (singleton z))
   (at level 1) : stdpp_scope.
-Notation "{[ x , y ]}" := (singleton (x,y))
-  (at level 1, y at next level) : stdpp_scope.
-Notation "{[ x , y , z ]}" := (singleton (x,y,z))
-  (at level 1, y at next level, z at next level) : stdpp_scope.
 
 Class SubsetEq A := subseteq: relation A.
-Hint Mode SubsetEq ! : typeclass_instances.
-Instance: Params (@subseteq) 2 := {}.
+Global Hint Mode SubsetEq ! : typeclass_instances.
+Global Instance: Params (@subseteq) 2 := {}.
 Infix "⊆" := subseteq (at level 70) : stdpp_scope.
 Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
 Notation "( X ⊆.)" := (subseteq X) (only parsing) : stdpp_scope.
@@ -892,15 +1084,9 @@ Notation "(⊆@{ A } )" := (@subseteq A _) (only parsing) : stdpp_scope.
 
 Infix "⊆*" := (Forall2 (⊆)) (at level 70) : stdpp_scope.
 Notation "(⊆*)" := (Forall2 (⊆)) (only parsing) : stdpp_scope.
-Infix "⊆**" := (Forall2 (⊆*)) (at level 70) : stdpp_scope.
-Infix "⊆1*" := (Forall2 (λ p q, p.1 ⊆ q.1)) (at level 70) : stdpp_scope.
-Infix "⊆2*" := (Forall2 (λ p q, p.2 ⊆ q.2)) (at level 70) : stdpp_scope.
-Infix "⊆1**" := (Forall2 (λ p q, p.1 ⊆* q.1)) (at level 70) : stdpp_scope.
-Infix "⊆2**" := (Forall2 (λ p q, p.2 ⊆* q.2)) (at level 70) : stdpp_scope.
 
-Hint Extern 0 (_ ⊆ _) => reflexivity : core.
-Hint Extern 0 (_ ⊆* _) => reflexivity : core.
-Hint Extern 0 (_ ⊆** _) => reflexivity : core.
+Global Hint Extern 0 (_ ⊆ _) => reflexivity : core.
+Global Hint Extern 0 (_ ⊆* _) => reflexivity : core.
 
 Infix "⊂" := (strict (⊆)) (at level 70) : stdpp_scope.
 Notation "(⊂)" := (strict (⊆)) (only parsing) : stdpp_scope.
@@ -919,22 +1105,65 @@ Notation "X ⊆ Y ⊂ Z" := (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level)
 Notation "X ⊂ Y ⊆ Z" := (X ⊂ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : stdpp_scope.
 Notation "X ⊂ Y ⊂ Z" := (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : stdpp_scope.
 
+(** We define type classes for multisets: disjoint union [⊎] and the multiset
+singleton [{[+ _ +]}]. Multiset literals [{[+ x1; ..; xn +]}] are defined in
+terms of iterated disjoint union [{[+ x1 +]} ⊎ .. ⊎ {[+ xn +]}], and are thus
+different from set literals [{[ x1; ..; xn ]}], which use [∪].
+
+Note that in principle we could reuse the set singleton [{[ _ ]}] for multisets,
+and define [{[+ x1; ..; xn +]}] as [{[ x1 ]} ⊎ .. ⊎ {[ xn ]}]. However, this
+would risk accidentally using [{[ x1; ..; xn ]}] for multisets (leading to
+unexpected results) and lead to ambigious pretty printing for [{[+ x +]}]. *)
+Class DisjUnion A := disj_union: A → A → A.
+Global Hint Mode DisjUnion ! : typeclass_instances.
+Global Instance: Params (@disj_union) 2 := {}.
+Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
+Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
+Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
+Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
+
+Definition disj_union_list `{Empty A} `{DisjUnion A} : list A → A := fold_right (⊎) ∅.
+Global Arguments disj_union_list _ _ _ !_ / : assert.
+(* There is no "big" version of [⊎] in unicode, we thus use [⋃+]. *)
+Notation "⋃+ l" := (disj_union_list l) (at level 20, format "⋃+  l") : stdpp_scope.
+
+Class SingletonMS A B := singletonMS: A → B.
+Global Hint Mode SingletonMS - ! : typeclass_instances.
+Global Instance: Params (@singletonMS) 3 := {}.
+Notation "{[+ x +]}" := (singletonMS x)
+  (at level 1, format "{[+  x  +]}") : stdpp_scope.
+Notation "{[+ x ; y ; .. ; z +]}" :=
+  (disj_union .. (disj_union (singletonMS x) (singletonMS y)) .. (singletonMS z))
+  (at level 1, format "{[+  x ;  y ;  .. ;  z  +]}") : stdpp_scope.
+
 Definition option_to_set `{Singleton A C, Empty C} (mx : option A) : C :=
   match mx with None => ∅ | Some x => {[ x ]} end.
 Fixpoint list_to_set `{Singleton A C, Empty C, Union C} (l : list A) : C :=
   match l with [] => ∅ | x :: l => {[ x ]} ∪ list_to_set l end.
-Fixpoint list_to_set_disj `{Singleton A C, Empty C, DisjUnion C} (l : list A) : C :=
-  match l with [] => ∅ | x :: l => {[ x ]} ⊎ list_to_set_disj l end.
+Fixpoint list_to_set_disj `{SingletonMS A C, Empty C, DisjUnion C} (l : list A) : C :=
+  match l with [] => ∅ | x :: l => {[+ x +]} ⊎ list_to_set_disj l end.
+
+Class ScalarMul N A := scalar_mul : N → A → A.
+Global Hint Mode ScalarMul - ! : typeclass_instances.
+(** The [N] arguments is typically [nat] or [Z], so we do not want to rewrite
+in that. Hence, the value of [Params] is 3. *)
+Global Instance: Params (@scalar_mul) 3 := {}.
+(** The notation [*:] and level is taken from ssreflect, see
+https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/ssrnotations.v *)
+Infix "*:" := scalar_mul (at level 40) : stdpp_scope.
+Notation "(*:)" :=  scalar_mul (only parsing) : stdpp_scope.
+Notation "( x *:.)" := (scalar_mul x) (only parsing) : stdpp_scope.
+Notation "(.*: x )" := (λ y, scalar_mul y x) (only parsing) : stdpp_scope.
 
 (** The class [Lexico A] is used for the lexicographic order on [A]. This order
 is used to create finite maps, finite sets, etc, and is typically different from
 the order [(⊆)]. *)
 Class Lexico A := lexico: relation A.
-Hint Mode Lexico ! : typeclass_instances.
+Global Hint Mode Lexico ! : typeclass_instances.
 
 Class ElemOf A B := elem_of: A → B → Prop.
-Hint Mode ElemOf - ! : typeclass_instances.
-Instance: Params (@elem_of) 3 := {}.
+Global Hint Mode ElemOf - ! : typeclass_instances.
+Global Instance: Params (@elem_of) 3 := {}.
 Infix "∈" := elem_of (at level 70) : stdpp_scope.
 Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
 Notation "( x ∈.)" := (elem_of x) (only parsing) : stdpp_scope.
@@ -951,8 +1180,8 @@ Notation "x ∉@{ B } X" := (¬x ∈@{B} X) (at level 80, only parsing) : stdpp_
 Notation "(∉@{ B } )" := (λ x X, x ∉@{B} X) (only parsing) : stdpp_scope.
 
 Class Disjoint A := disjoint : A → A → Prop.
- Hint Mode Disjoint ! : typeclass_instances.
-Instance: Params (@disjoint) 2 := {}.
+Global Hint Mode Disjoint ! : typeclass_instances.
+Global Instance: Params (@disjoint) 2 := {}.
 Infix "##" := disjoint (at level 70) : stdpp_scope.
 Notation "(##)" := disjoint (only parsing) : stdpp_scope.
 Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope.
@@ -963,58 +1192,15 @@ Notation "(##@{ A } )" := (@disjoint A _) (only parsing) : stdpp_scope.
 
 Infix "##*" := (Forall2 (##)) (at level 70) : stdpp_scope.
 Notation "(##*)" := (Forall2 (##)) (only parsing) : stdpp_scope.
-Infix "##**" := (Forall2 (##*)) (at level 70) : stdpp_scope.
-Infix "##1*" := (Forall2 (λ p q, p.1 ## q.1)) (at level 70) : stdpp_scope.
-Infix "##2*" := (Forall2 (λ p q, p.2 ## q.2)) (at level 70) : stdpp_scope.
-Infix "##1**" := (Forall2 (λ p q, p.1 ##* q.1)) (at level 70) : stdpp_scope.
-Infix "##2**" := (Forall2 (λ p q, p.2 ##* q.2)) (at level 70) : stdpp_scope.
-Hint Extern 0 (_ ## _) => symmetry; eassumption : core.
-Hint Extern 0 (_ ##* _) => symmetry; eassumption : core.
-
-Class DisjointE E A := disjointE : E → A → A → Prop.
-Hint Mode DisjointE - ! : typeclass_instances.
-Instance: Params (@disjointE) 4 := {}.
-Notation "X ##{ Γ } Y" := (disjointE Γ X Y)
-  (at level 70, format "X  ##{ Γ }  Y") : stdpp_scope.
-Notation "(##{ Γ } )" := (disjointE Γ) (only parsing, Γ at level 1) : stdpp_scope.
-Notation "Xs ##{ Γ }* Ys" := (Forall2 (##{Γ}) Xs Ys)
-  (at level 70, format "Xs  ##{ Γ }*  Ys") : stdpp_scope.
-Notation "(##{ Γ }* )" := (Forall2 (##{Γ}))
-  (only parsing, Γ at level 1) : stdpp_scope.
-Notation "X ##{ Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ3) X Y)
-  (at level 70, format "X  ##{ Γ1 , Γ2 , .. , Γ3 }  Y") : stdpp_scope.
-Notation "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
-  (Forall2 (disjoint (pair .. (Γ1, Γ2) .. Γ3)) Xs Ys)
-  (at level 70, format "Xs  ##{ Γ1 ,  Γ2 , .. , Γ3 }*  Ys") : stdpp_scope.
-Hint Extern 0 (_ ##{_} _) => symmetry; eassumption : core.
-
-Class DisjointList A := disjoint_list : list A → Prop.
-Hint Mode DisjointList ! : typeclass_instances.
-Instance: Params (@disjoint_list) 2 := {}.
-Notation "## Xs" := (disjoint_list Xs) (at level 20, format "##  Xs") : stdpp_scope.
-Notation "##@{ A } Xs" :=
-  (@disjoint_list A _ Xs) (at level 20, only parsing) : stdpp_scope.
-
-Section disjoint_list.
-  Context `{Disjoint A, Union A, Empty A}.
-  Implicit Types X : A.
-
-  Inductive disjoint_list_default : DisjointList A :=
-    | disjoint_nil_2 : ##@{A} []
-    | disjoint_cons_2 (X : A) (Xs : list A) : X ## ⋃ Xs → ## Xs → ## (X :: Xs).
-  Global Existing Instance disjoint_list_default.
-
-  Lemma disjoint_list_nil  : ##@{A} [] ↔ True.
-  Proof. split; constructor. Qed.
-  Lemma disjoint_list_cons X Xs : ## (X :: Xs) ↔ X ## ⋃ Xs ∧ ## Xs.
-  Proof. split. inversion_clear 1; auto. intros [??]. constructor; auto. Qed.
-End disjoint_list.
+
+Global Hint Extern 0 (_ ## _) => symmetry; eassumption : core.
+Global Hint Extern 0 (_ ##* _) => symmetry; eassumption : core.
 
 Class Filter A B := filter: ∀ (P : A → Prop) `{∀ x, Decision (P x)}, B → B.
-Hint Mode Filter - ! : typeclass_instances.
+Global Hint Mode Filter - ! : typeclass_instances.
 
 Class UpClose A B := up_close : A → B.
-Hint Mode UpClose - ! : typeclass_instances.
+Global Hint Mode UpClose - ! : typeclass_instances.
 Notation "↑ x" := (up_close x) (at level 20, format "↑ x").
 
 (** * Monadic operations *)
@@ -1023,20 +1209,29 @@ and fmap. We use these type classes merely for convenient overloading of
 notations and do not formalize any theory on monads (we do not even define a
 class with the monad laws). *)
 Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
-Arguments mret {_ _ _} _ : assert.
-Instance: Params (@mret) 3 := {}.
+Global Arguments mret {_ _ _} _ : assert.
+Global Instance: Params (@mret) 3 := {}.
+Global Hint Mode MRet ! : typeclass_instances.
+
 Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
-Arguments mbind {_ _ _ _} _ !_ / : assert.
-Instance: Params (@mbind) 4 := {}.
+Global Arguments mbind {_ _ _ _} _ !_ / : assert.
+Global Instance: Params (@mbind) 4 := {}.
+Global Hint Mode MBind ! : typeclass_instances.
+
 Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A.
-Arguments mjoin {_ _ _} !_ / : assert.
-Instance: Params (@mjoin) 3 := {}.
+Global Arguments mjoin {_ _ _} !_ / : assert.
+Global Instance: Params (@mjoin) 3 := {}.
+Global Hint Mode MJoin ! : typeclass_instances.
+
 Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
-Arguments fmap {_ _ _ _} _ !_ / : assert.
-Instance: Params (@fmap) 4 := {}.
+Global Arguments fmap {_ _ _ _} _ !_ / : assert.
+Global Instance: Params (@fmap) 4 := {}.
+Global Hint Mode FMap ! : typeclass_instances.
+
 Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B.
-Arguments omap {_ _ _ _} _ !_ / : assert.
-Instance: Params (@omap) 4 := {}.
+Global Arguments omap {_ _ _ _} _ !_ / : assert.
+Global Instance: Params (@omap) 4 := {}.
+Global Hint Mode OMap ! : typeclass_instances.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
 Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
@@ -1059,67 +1254,147 @@ Notation "ps .*1" := (fmap (M:=list) fst ps)
 Notation "ps .*2" := (fmap (M:=list) snd ps)
   (at level 2, left associativity, format "ps .*2").
 
-Class MGuard (M : Type → Type) :=
-  mguard: ∀ P {dec : Decision P} {A}, (P → M A) → M A.
-Arguments mguard _ _ _ !_ _ _ / : assert.
-Notation "'guard' P ; z" := (mguard P (λ _, z))
-  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
-Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
-  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
+(** For any monad that has a builtin way to throw an exception/error *)
+Class MThrow (E : Type) (M : Type → Type) := mthrow : ∀ {A}, E → M A.
+Global Arguments mthrow {_ _ _ _} _ : assert.
+Global Instance: Params (@mthrow) 4 := {}.
+Global Hint Mode MThrow ! ! : typeclass_instances.
+
+(** We use unit as the error content for monads that can only report an error
+    without any payload like an option *)
+Global Notation MFail := (MThrow ()).
+Global Notation mfail := (mthrow ()).
+
+Definition guard_or {E} (e : E) `{MThrow E M, MRet M} P `{Decision P} : M P :=
+  match decide P with
+  | left H => mret H
+  | right _ => mthrow e
+  end.
+Global Notation guard := (guard_or ()).
+
 
 (** * Operations on maps *)
 (** In this section we define operational type classes for the operations
 on maps. In the file [fin_maps] we will axiomatize finite maps.
 The function look up [m !! k] should yield the element at key [k] in [m]. *)
 Class Lookup (K A M : Type) := lookup: K → M → option A.
-Hint Mode Lookup - - ! : typeclass_instances.
-Instance: Params (@lookup) 4 := {}.
+Global Hint Mode Lookup - - ! : typeclass_instances.
+Global Instance: Params (@lookup) 5 := {}.
 Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
 Notation "(!!)" := lookup (only parsing) : stdpp_scope.
 Notation "( m !!.)" := (λ i, m !! i) (only parsing) : stdpp_scope.
 Notation "(.!! i )" := (lookup i) (only parsing) : stdpp_scope.
-Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
+Global Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [lookup_total] should be the total over-approximation
 of the partial [lookup] function. *)
 Class LookupTotal (K A M : Type) := lookup_total : K → M → A.
-Hint Mode LookupTotal - - ! : typeclass_instances.
-Instance: Params (@lookup_total) 4 := {}.
+Global Hint Mode LookupTotal - - ! : typeclass_instances.
+Global Instance: Params (@lookup_total) 5 := {}.
 Notation "m !!! i" := (lookup_total i m) (at level 20) : stdpp_scope.
 Notation "(!!!)" := lookup_total (only parsing) : stdpp_scope.
 Notation "( m !!!.)" := (λ i, m !!! i) (only parsing) : stdpp_scope.
 Notation "(.!!! i )" := (lookup_total i) (only parsing) : stdpp_scope.
-Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.
+Global Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The singleton map *)
 Class SingletonM K A M := singletonM: K → A → M.
-Hint Mode SingletonM - - ! : typeclass_instances.
-Instance: Params (@singletonM) 5 := {}.
+Global Hint Mode SingletonM - - ! : typeclass_instances.
+Global Instance: Params (@singletonM) 5 := {}.
 Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.
 
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
 Class Insert (K A M : Type) := insert: K → A → M → M.
-Hint Mode Insert - - ! : typeclass_instances.
-Instance: Params (@insert) 5 := {}.
+Global Hint Mode Insert - - ! : typeclass_instances.
+Global Instance: Params (@insert) 5 := {}.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope.
-Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
+Global Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
+
+(** Notation for more elements (up to 13) *)
+(* Defining a generic notation does not seem possible with Coq's
+   recursive notation system, so we define individual notations
+   for some cases relevant in practice. *)
+(* The "format" makes sure that linebreaks are placed after the separating semicolons [;] when printing. *)
+(* TODO : we are using parentheses in the "de-sugaring" of the notation instead of [$] because Coq 8.12
+   and earlier have trouble with using the notation for printing otherwise.
+   Once support for Coq 8.12 is dropped, this can be replaced with [$]. *)
+Notation "{[ k1 := a1 ; k2 := a2 ]}" :=
+  (<[ k1 := a1 ]>{[ k2 := a2 ]})
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ]}" :=
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]>{[ k3 := a3 ]}))
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ]}" :=
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]>{[ k4 := a4 ]})))
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ]}" :=
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]>{[ k5 := a5 ]}))))
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ]}" :=
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]>{[ k6 := a6 ]})))))
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ]}" :=
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]>{[ k7 := a7 ]}))))))
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ]}" :=
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]>{[ k8 := a8 ]})))))))
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ]}" :=
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]>{[ k9 := a9 ]}))))))))
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ]}" :=
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
+    <[ k9 := a9 ]>{[ k10 := a10 ]})))))))))
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ]}" :=
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
+    <[ k9 := a9 ]> ( <[ k10 := a10 ]>{[ k11 := a11 ]}))))))))))
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ; ']'  '/' '[' k11  :=  a11 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ]}" :=
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
+    <[ k9 := a9 ]> ( <[ k10 := a10 ]> ( <[ k11 := a11 ]>{[ k12 := a12 ]})))))))))))
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ; ']'  '/' '[' k11  :=  a11 ; ']'  '/' '[' k12  :=  a12 ']' ']' ]}") : stdpp_scope.
+Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k7 := a7 ; k8 := a8 ; k9 := a9 ; k10 := a10 ; k11 := a11 ; k12 := a12 ; k13 := a13 ]}" :=
+  (<[ k1 := a1 ]> ( <[ k2 := a2 ]> ( <[ k3 := a3 ]> ( <[ k4 := a4 ]> (
+    <[ k5 := a5 ]> ( <[ k6 := a6 ]> ( <[ k7 := a7 ]> ( <[ k8 := a8 ]> (
+    <[ k9 := a9 ]> ( <[ k10 := a10 ]> ( <[ k11 := a11 ]> ( <[ k12 := a12 ]>{[ k13 := a13 ]}))))))))))))
+  (at level 1, format
+  "{[ '[hv' '[' k1  :=  a1 ; ']'  '/' '[' k2  :=  a2 ; ']'  '/' '[' k3  :=  a3 ; ']'  '/' '[' k4  :=  a4 ; ']'  '/' '[' k5  :=  a5 ; ']'  '/' '[' k6  :=  a6 ; ']'  '/' '[' k7  :=  a7 ; ']'  '/' '[' k8  :=  a8 ; ']'  '/' '[' k9  :=  a9 ; ']'  '/' '[' k10  :=  a10 ; ']'  '/' '[' k11  :=  a11 ; ']'  '/' '[' k12  :=  a12 ; ']'  '/' '[' k13  :=  a13 ']' ']' ]}") : stdpp_scope.
 
 (** The function delete [delete k m] should delete the value at key [k] in
 [m]. If the key [k] is not a member of [m], the original map should be
 returned. *)
 Class Delete (K M : Type) := delete: K → M → M.
-Hint Mode Delete - ! : typeclass_instances.
-Instance: Params (@delete) 4 := {}.
-Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
+Global Hint Mode Delete - ! : typeclass_instances.
+Global Instance: Params (@delete) 4 := {}.
+Global Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
 Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
-Hint Mode Alter - - ! : typeclass_instances.
-Instance: Params (@alter) 5 := {}.
-Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
+Global Hint Mode Alter - - ! : typeclass_instances.
+Global Instance: Params (@alter) 4 := {}.
+Global Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [partial_alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value at key [k] or [None]
@@ -1127,74 +1402,60 @@ if [k] is not a member of [m]. The value at [k] should be deleted if [f]
 yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
-Hint Mode PartialAlter - - ! : typeclass_instances.
-Instance: Params (@partial_alter) 4 := {}.
-Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
-
-(** The function [dom C m] should yield the domain of [m]. That is a finite
-set of type [C] that contains the keys that are a member of [m]. *)
-Class Dom (M C : Type) := dom: M → C.
-Hint Mode Dom ! ! : typeclass_instances.
-Instance: Params (@dom) 3 := {}.
-Arguments dom : clear implicits.
-Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
+Global Hint Mode PartialAlter - - ! : typeclass_instances.
+Global Instance: Params (@partial_alter) 4 := {}.
+Global Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
+
+(** The function [dom m] should yield the domain of [m]. That is a finite
+set of type [D] that contains the keys that are a member of [m].
+[D] is an output of the typeclass, i.e., there can be only one instance per map
+type [M]. *)
+Class Dom (M D : Type) := dom: M → D.
+Global Hint Mode Dom ! - : typeclass_instances.
+Global Instance: Params (@dom) 3 := {}.
+Global Arguments dom : clear implicits.
+Global Arguments dom {_ _ _} !_ / : simpl nomatch, assert.
 
 (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
 Class Merge (M : Type → Type) :=
   merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C.
-Hint Mode Merge ! : typeclass_instances.
-Instance: Params (@merge) 4 := {}.
-Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
+Global Hint Mode Merge ! : typeclass_instances.
+Global Instance: Params (@merge) 4 := {}.
+Global Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [union_with f m1 m2] is supposed to yield the union of [m1]
 and [m2] using the function [f] to combine values of members that are in
 both [m1] and [m2]. *)
 Class UnionWith (A M : Type) :=
   union_with: (A → A → option A) → M → M → M.
-Hint Mode UnionWith - ! : typeclass_instances.
-Instance: Params (@union_with) 3 := {}.
-Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
+Global Hint Mode UnionWith - ! : typeclass_instances.
+Global Instance: Params (@union_with) 3 := {}.
+Global Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** Similarly for intersection and difference. *)
 Class IntersectionWith (A M : Type) :=
   intersection_with: (A → A → option A) → M → M → M.
-Hint Mode IntersectionWith - ! : typeclass_instances.
-Instance: Params (@intersection_with) 3 := {}.
-Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
+Global Hint Mode IntersectionWith - ! : typeclass_instances.
+Global Instance: Params (@intersection_with) 3 := {}.
+Global Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Class DifferenceWith (A M : Type) :=
   difference_with: (A → A → option A) → M → M → M.
-Hint Mode DifferenceWith - ! : typeclass_instances.
-Instance: Params (@difference_with) 3 := {}.
-Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
+Global Hint Mode DifferenceWith - ! : typeclass_instances.
+Global Instance: Params (@difference_with) 3 := {}.
+Global Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Definition intersection_with_list `{IntersectionWith A M}
   (f : A → A → option A) : M → list M → M := fold_right (intersection_with f).
-Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
-
-Class LookupE (E K A M : Type) := lookupE: E → K → M → option A.
-Hint Mode LookupE - - - ! : typeclass_instances.
-Instance: Params (@lookupE) 6 := {}.
-Notation "m !!{ Γ } i" := (lookupE Γ i m)
-  (at level 20, format "m  !!{ Γ }  i") : stdpp_scope.
-Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : stdpp_scope.
-Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
-
-Class InsertE (E K A M : Type) := insertE: E → K → A → M → M.
-Hint Mode InsertE - - - ! : typeclass_instances.
-Instance: Params (@insertE) 6 := {}.
-Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
-  (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : stdpp_scope.
-Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
-
+Global Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
 
 (** * Notations for lattices. *)
 (** SqSubsetEq registers the "canonical" partial order for a type, and is used
 for the \sqsubseteq symbol. *)
 Class SqSubsetEq A := sqsubseteq: relation A.
-Hint Mode SqSubsetEq ! : typeclass_instances.
-Instance: Params (@sqsubseteq) 2 := {}.
+Global Hint Mode SqSubsetEq ! : typeclass_instances.
+Global Instance: Params (@sqsubseteq) 2 := {}.
 Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
 Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
 Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope.
@@ -1203,32 +1464,35 @@ Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
 Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
 Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
 
-Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
+(** [sqsubseteq] does not take precedence over the stdlib's instances (like [eq],
+[impl], [iff]) or std++'s [equiv].
+We have [eq] (at 100) < [≡] (at 150) < [⊑] (at 200). *)
+Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 200 := {}.
 
-Hint Extern 0 (_ ⊑ _) => reflexivity : core.
+Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.
 
 Class Meet A := meet: A → A → A.
-Hint Mode Meet ! : typeclass_instances.
-Instance: Params (@meet) 2 := {}.
+Global Hint Mode Meet ! : typeclass_instances.
+Global Instance: Params (@meet) 2 := {}.
 Infix "⊓" := meet (at level 40) : stdpp_scope.
 Notation "(⊓)" := meet (only parsing) : stdpp_scope.
 Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
 Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
 
 Class Join A := join: A → A → A.
-Hint Mode Join ! : typeclass_instances.
-Instance: Params (@join) 2 := {}.
+Global Hint Mode Join ! : typeclass_instances.
+Global Instance: Params (@join) 2 := {}.
 Infix "⊔" := join (at level 50) : stdpp_scope.
 Notation "(⊔)" := join (only parsing) : stdpp_scope.
 Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
 Notation "(.⊔ y )" := (λ x, join x y) (only parsing) : stdpp_scope.
 
 Class Top A := top : A.
-Hint Mode Top ! : typeclass_instances.
+Global Hint Mode Top ! : typeclass_instances.
 Notation "⊤" := top (format "⊤") : stdpp_scope.
 
 Class Bottom A := bottom : A.
-Hint Mode Bottom ! : typeclass_instances.
+Global Hint Mode Bottom ! : typeclass_instances.
 Notation "⊥" := bottom (format "⊥") : stdpp_scope.
 
 
@@ -1248,31 +1512,36 @@ Class SemiSet A C `{ElemOf A C,
   elem_of_singleton (x y : A) : x ∈@{C} {[ y ]} ↔ x = y;
   elem_of_union (X Y : C) (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
 }.
+Global Hint Mode SemiSet - ! - - - - : typeclass_instances.
+
 Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
-  set_semi_set :> SemiSet A C;
+  set_semi_set :: SemiSet A C;
   elem_of_intersection (X Y : C) (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
   elem_of_difference (X Y : C) (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
 }.
+Global Hint Mode Set_ - ! - - - - - - : typeclass_instances.
+
 Class TopSet A C `{ElemOf A C, Empty C, Top C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
-  top_set_set :> Set_ A C;
+  top_set_set :: Set_ A C;
   elem_of_top' (x : A) : x ∈@{C} ⊤; (* We prove [elem_of_top : x ∈@{C} ⊤ ↔ True]
   in [sets.v], which is more convenient for rewriting. *)
 }.
+Global Hint Mode TopSet - ! - - - - - - - : typeclass_instances.
 
 (** We axiomative a finite set as a set whose elements can be
 enumerated as a list. These elements, given by the [elements] function, may be
 in any order and should not contain duplicates. *)
 Class Elements A C := elements: C → list A.
-Hint Mode Elements - ! : typeclass_instances.
-Instance: Params (@elements) 3 := {}.
+Global Hint Mode Elements - ! : typeclass_instances.
+Global Instance: Params (@elements) 3 := {}.
 
 (** We redefine the standard library's [In] and [NoDup] using type classes. *)
 Inductive elem_of_list {A} : ElemOf A (list A) :=
   | elem_of_list_here (x : A) l : x ∈ x :: l
   | elem_of_list_further (x y : A) l : x ∈ l → x ∈ y :: l.
-Existing Instance elem_of_list.
+Global Existing Instance elem_of_list.
 
 Lemma elem_of_list_In {A} (l : list A) x : x ∈ l ↔ In x l.
 Proof.
@@ -1296,27 +1565,31 @@ Qed.
 anyway so as to avoid cycles in type class search. *)
 Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
     Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
-  fin_set_set :> Set_ A C;
+  fin_set_set :: Set_ A C;
   elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X;
   NoDup_elements (X : C) : NoDup (elements X)
 }.
+Global Hint Mode FinSet - ! - - - - - - - - : typeclass_instances.
+
 Class Size C := size: C → nat.
-Hint Mode Size ! : typeclass_instances.
-Arguments size {_ _} !_ / : simpl nomatch, assert.
-Instance: Params (@size) 2 := {}.
+Global Hint Mode Size ! : typeclass_instances.
+Global Arguments size {_ _} !_ / : simpl nomatch, assert.
+Global Instance: Params (@size) 2 := {}.
 
 (** The class [MonadSet M] axiomatizes a type constructor [M] that can be
 used to construct a set [M A] with elements of type [A]. The advantage
 of this class, compared to [Set_], is that it also axiomatizes the
-the monadic operations. The disadvantage, is that not many inhabits are
-possible (we will only provide an inhabitant using unordered lists without
-duplicates). More interesting implementations typically need
+the monadic operations. The disadvantage is that not many inhabitants are
+possible: we will only provide as inhabitants [propset] and [listset], which are
+represented respectively using Boolean functions and lists with duplicates.
+
+More interesting implementations typically need
 decidable equality, or a total order on the elements, which do not fit
 in a type constructor of type [Type → Type]. *)
 Class MonadSet M `{∀ A, ElemOf A (M A),
     ∀ A, Empty (M A), ∀ A, Singleton A (M A), ∀ A, Union (M A),
     !MBind M, !MRet M, !FMap M, !MJoin M} : Prop := {
-  monad_set_semi_set A :> SemiSet A (M A);
+  monad_set_semi_set A :: SemiSet A (M A);
   elem_of_bind {A B} (f : A → M B) (X : M A) (x : B) :
     x ∈ X ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ X;
   elem_of_ret {A} (x y : A) : x ∈@{M A} mret y ↔ x = y;
@@ -1327,34 +1600,35 @@ Class MonadSet M `{∀ A, ElemOf A (M A),
 }.
 
 (** The [Infinite A] class axiomatizes types [A] with infinitely many elements.
-It contains a function [fresh : list A → A] that given a list [xs] gives an
+It contains a function [fresh : list A → A] that, given a list [xs], gives an
 element [fresh xs ∉ xs].
 
 We do not directly make [fresh] a field of the [Infinite] class, but use a
 separate operational type class [Fresh] for it. That way we can overload [fresh]
-to pick fresh elements from other data structure like sets. See the file
+to pick fresh elements from other data structures like sets. See the file
 [fin_sets], where we define [fresh : C → A] for any finite set implementation
 [FinSet C A].
 
 Note: we require [fresh] to respect permutations, which is needed to define the
-aforementioned [fresh] function on finite sets that respects set equality.
+aforementioned [fresh] function on finite sets that respect set equality.
 
 Instead of instantiating [Infinite] directly, consider using [max_infinite] or
 [inj_infinite] from the [infinite] module. *)
 Class Fresh A C := fresh: C → A.
-Hint Mode Fresh - ! : typeclass_instances.
-Instance: Params (@fresh) 3 := {}.
-Arguments fresh : simpl never.
+Global Hint Mode Fresh - ! : typeclass_instances.
+Global Instance: Params (@fresh) 3 := {}.
+Global Arguments fresh : simpl never.
 
 Class Infinite A := {
-  infinite_fresh :> Fresh A (list A);
+  infinite_fresh :: Fresh A (list A);
   infinite_is_fresh (xs : list A) : fresh xs ∉ xs;
-  infinite_fresh_Permutation :> Proper (@Permutation A ==> (=)) fresh;
+  infinite_fresh_Permutation :: Proper (@Permutation A ==> (=)) fresh;
 }.
-Arguments infinite_fresh : simpl never.
+Global Hint Mode Infinite ! : typeclass_instances.
+Global Arguments infinite_fresh : simpl never.
 
 (** * Miscellaneous *)
 Class Half A := half: A → A.
-Hint Mode Half ! : typeclass_instances.
+Global Hint Mode Half ! : typeclass_instances.
 Notation "½" := half (format "½") : stdpp_scope.
 Notation "½*" := (fmap (M:=list) half) : stdpp_scope.

theories/binders.v → stdpp/binders.v

@@ -7,16 +7,29 @@ This library is used in various Iris developments, like heap-lang, LambdaRust,
 Iron, Fairis. *)
 From stdpp Require Export strings.
 From stdpp Require Import sets countable finite fin_maps.
+From stdpp Require Import options.
+
+(* Pick up extra assumptions from section parameters. *)
+Set Default Proof Using "Type*".
+
+Declare Scope binder_scope.
+Delimit Scope binder_scope with binder.
 
 Inductive binder := BAnon | BNamed :> string → binder.
 Bind Scope binder_scope with binder.
-Delimit Scope binder_scope with binder.
 Notation "<>" := BAnon : binder_scope.
 
-Instance binder_dec_eq : EqDecision binder.
+(** [binder_list] matches [option_list]. *)
+Definition binder_list (b : binder) : list string :=
+  match b with
+  | BAnon => []
+  | BNamed s => [s]
+  end.
+
+Global Instance binder_dec_eq : EqDecision binder.
 Proof. solve_decision. Defined.
-Instance binder_inhabited : Inhabited binder := populate BAnon.
-Instance binder_countable : Countable binder.
+Global Instance binder_inhabited : Inhabited binder := populate BAnon.
+Global Instance binder_countable : Countable binder.
 Proof.
  refine (inj_countable'
    (λ b, match b with BAnon => None | BNamed s => Some s end)
@@ -34,13 +47,13 @@ Fixpoint app_binder (bs : list binder) (ss : list string) : list string :=
   match bs with [] => ss | b :: bs => b :b: app_binder bs ss end.
 Infix "+b+" := app_binder (at level 60, right associativity).
 
-Instance set_unfold_cons_binder s b ss P :
+Global Instance set_unfold_cons_binder s b ss P :
   SetUnfoldElemOf s ss P → SetUnfoldElemOf s (b :b: ss) (BNamed s = b ∨ P).
 Proof.
   constructor. rewrite <-(set_unfold (s ∈ ss) P).
   destruct b; simpl; rewrite ?elem_of_cons; naive_solver.
 Qed.
-Instance set_unfold_app_binder s bs ss P Q :
+Global Instance set_unfold_app_binder s bs ss P Q :
   SetUnfoldElemOf (BNamed s) bs P → SetUnfoldElemOf s ss Q →
   SetUnfoldElemOf s (bs +b+ ss) (P ∨ Q).
 Proof.
@@ -56,13 +69,13 @@ Proof. induction ss1; by f_equal/=. Qed.
 Lemma app_binder_snoc bs s ss : bs +b+ (s :: ss) = (bs ++ [BNamed s]) +b+ ss.
 Proof. induction bs; by f_equal/=. Qed.
 
-Instance cons_binder_Permutation b : Proper ((≡ₚ) ==> (≡ₚ)) (cons_binder b).
+Global Instance cons_binder_Permutation b : Proper ((≡ₚ) ==> (≡ₚ)) (cons_binder b).
 Proof. intros ss1 ss2 Hss. destruct b; csimpl; by rewrite Hss. Qed.
 
-Instance app_binder_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
+Global Instance app_binder_Permutation : Proper ((≡ₚ) ==> (≡ₚ) ==> (≡ₚ)) app_binder.
 Proof.
   assert (∀ bs, Proper ((≡ₚ) ==> (≡ₚ)) (app_binder bs)).
-  { induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
+  { intros bs. induction bs as [|[]]; intros ss1 ss2; simpl; by intros ->. }
   induction 1 as [|[]|[] []|]; intros ss1 ss2 Hss; simpl;
     first [by eauto using perm_trans|by rewrite 1?perm_swap, Hss].
 Qed.
@@ -71,7 +84,7 @@ Definition binder_delete `{Delete string M} (b : binder) (m : M) : M :=
   match b with BAnon => m | BNamed s => delete s m end.
 Definition binder_insert `{Insert string A M} (b : binder) (x : A) (m : M) : M :=
   match b with BAnon => m | BNamed s => <[s:=x]> m end.
-Instance: Params (@binder_insert) 4 := {}.
+Global Instance: Params (@binder_insert) 4 := {}.
 
 Section binder_delete_insert.
   Context `{FinMap string M}.

theories/boolset.v → stdpp/boolset.v

 (** This file implements boolsets as functions into Prop. *)
 From stdpp Require Export prelude.
-Set Default Proof Using "Type".
+From stdpp Require Import options.
 
 Record boolset (A : Type) : Type := BoolSet { boolset_car : A → bool }.
-Arguments BoolSet {_} _ : assert.
-Arguments boolset_car {_} _ _ : assert.
+Global Arguments BoolSet {_} _ : assert.
+Global Arguments boolset_car {_} _ _ : assert.
 
-Instance boolset_top {A} : Top (boolset A) := BoolSet (λ _, true).
-Instance boolset_empty {A} : Empty (boolset A) := BoolSet (λ _, false).
-Instance boolset_singleton `{EqDecision A} : Singleton A (boolset A) := λ x,
+Global Instance boolset_top {A} : Top (boolset A) := BoolSet (λ _, true).
+Global Instance boolset_empty {A} : Empty (boolset A) := BoolSet (λ _, false).
+Global Instance boolset_singleton `{EqDecision A} : Singleton A (boolset A) := λ x,
   BoolSet (λ y, bool_decide (y = x)).
-Instance boolset_elem_of {A} : ElemOf A (boolset A) := λ x X, boolset_car X x.
-Instance boolset_union {A} : Union (boolset A) := λ X1 X2,
+Global Instance boolset_elem_of {A} : ElemOf A (boolset A) := λ x X, boolset_car X x.
+Global Instance boolset_union {A} : Union (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x || boolset_car X2 x).
-Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
+Global Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
-Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
+Global Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
-Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
+Global Instance boolset_cprod {A B} :
+  CProd (boolset A) (boolset B) (boolset (A * B)) := λ X1 X2,
+  BoolSet (λ x, boolset_car X1 x.1 && boolset_car X2 x.2).
+
+Global Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
 Proof.
   split; [split; [split| |]|].
   - by intros x ?.
   - by intros x y; rewrite <-(bool_decide_spec (x = y)).
-  - split. apply orb_prop_elim. apply orb_prop_intro.
-  - split. apply andb_prop_elim. apply andb_prop_intro.
+  - split; [apply orb_prop_elim | apply orb_prop_intro].
+  - split; [apply andb_prop_elim | apply andb_prop_intro].
   - intros X Y x; unfold elem_of, boolset_elem_of; simpl.
     destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
   - done.
 Qed.
-Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
+Global Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
 Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
 
-Typeclasses Opaque boolset_elem_of.
+Lemma elem_of_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) (x : A * B) :
+  x ∈ cprod X1 X2 ↔ x.1 ∈ X1 ∧ x.2 ∈ X2.
+Proof. apply andb_True. Qed.
+
+Global Instance set_unfold_boolset_cprod {A B} (X1 : boolset A) (X2 : boolset B) x P Q :
+  SetUnfoldElemOf x.1 X1 P → SetUnfoldElemOf x.2 X2 Q →
+  SetUnfoldElemOf x (cprod X1 X2) (P ∧ Q).
+Proof.
+  intros ??; constructor.
+  by rewrite elem_of_boolset_cprod, (set_unfold_elem_of x.1 X1 P),
+    (set_unfold_elem_of x.2 X2 Q).
+Qed.
+
+Global Typeclasses Opaque boolset_elem_of.
 Global Opaque boolset_empty boolset_singleton boolset_union
-  boolset_intersection boolset_difference.
+  boolset_intersection boolset_difference boolset_cprod.