2.64 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
This file lists "large-ish" changes to the std++ Coq library, but not every
2 3
API-breaking change is listed.

Ralf Jung's avatar
Ralf Jung committed
## std++ 1.1.0 (released 2017-12-19)

Ralf Jung's avatar
Ralf Jung committed
6 7 8
Coq 8.5 is no longer supported by this release of std++.  Use std++ 1.0 if you
have to use Coq 8.5.

9 10 11
New features:

- Many new lemmas about lists, vectors, sets, maps.
Ralf Jung's avatar
Ralf Jung committed
12 13 14
- Equivalence proofs between std++ functions and their alternative in the the
  Coq standard library, e.g. `List.nth`, `List.NoDop`.
- Typeclass versions of the logical connectives and list predicates:
  `TCOr`, `TCAnd`, `TCTrue`, `TCForall`, `TCForall2`.
Ralf Jung's avatar
Ralf Jung committed
- A function `tc_opaque` to make definitions type class opaque.
17 18 19 20 21 22 23 24 25
- 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.


- Get rid of `Automatic Coercions Import`, it is deprecated.
Ralf Jung's avatar
Ralf Jung committed
26 27
  Also get rid of `Set Asymmetric Patterns`.
- Various changes and improvements to `f_equiv` and `solve_proper`.
28 29 30 31 32 33 34 35 36 37 38 39 40 41 42
- `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.
Ralf Jung's avatar
Ralf Jung committed
- All notations are now in `stdpp_scope` with scope key `stdpp`
  (formerly `C_scope` and `C`).
Ralf Jung's avatar
Ralf Jung committed
45 46
- Higher precedence for `.1` and `.2` that is compatible with ssreflect.
- Various changes to monadic notations to improve compatibility with Mtac2:
47 48 49 50 51
  + Pattern matching notation for monadic bind `'pat ← x; y` where `pat` can
    be any Coq pattern.
  + Change the level of the do-notation.
  + `<$>` is left associative.
  + Notation `x ;; y` for `_ ← x; y`.
Ralf Jung's avatar
Ralf Jung committed
52 53 54 55 56 57 58 59

## History

Coq-std++ has originally been developed by Robbert Krebbers as part of his
formalization of the C programming language in his PhD thesis, called
[CH2O]( After that, Coq-std++ has been
part of the [Iris project](, and has continued to be
developed by Robbert Krebbers, Ralf Jung, and Jacques Henri-Jourdan.