This file lists "largeish" changes to the std++ Coq development, but not every
APIbreaking change is listed.
## std++ 1.1.0 (unfinished)
New features:
 Many new lemmas about lists, vectors, sets, maps.
 Equivalence proofs between coq++ functions that have a different definition in
the Coq standard library, e.g. `List.nth`, `List.NoDop`.
 Type versions of the logical connectives and list predicates:
`TCOr`, `TCAnd`, `TCTrue`, `TCForall`, `TCForall2`.
 A connective `tc_opaque` to make definitions type class opaque.
 A type class `Infinite` for infinite types.
 A generic implementation to obtain fresh elements of infinite types.
 More theory about curry and uncurry functions on `gmap`.
 A generic `filter` and `zip_with` operation on finite maps.
 A type of generic trees for showing that arbitrary types are countable.
Changes:
 Get rid of `Automatic Coercions Import`, it is deprecated.
 `Hint Mode` is now set for all operational type classes to make instance
search less likely to diverge.
 New type class `RelDecision` for decidable relations, and `EqDecision` is
defined in terms of it. This class allows to set `Hint Mode` properly.
 Use the flag `assert` of `Arguments` to make it more robust.
 The functions `imap` and `imap2` on lists are defined so that they enjoy more
definitional equalities.
 Theory about `fin` is moved to its own file `fin.v`.
 Rename `preserving` → `mono`.
Changes to notations:
 Operational type classes for lattice notations: `⊑`,`⊓`, `⊔`, `⊤` `⊥`.
 Replace `⊥` for disjointness with `##`, so that `⊥` can be used for the
bottom lattice element.
 All notations are now in `stdpp_scope` with scope `stdpp`
(formerly `C_scope` and `C`).
 Stronger binding for `.1` and `.2` that is compatible with ssreflect.
 Various changes to monadic notation to improve compatibility with Mtac2:
+ Pattern matching notation for monadic bind `'pat ← x; y` where `pat` can
be any Coq pattern.
+ Change the level of the donotation.
+ `<$>` is left associative.
+ Notation `x ;; y` for `_ ← x; y`.
