This is needed so that it can be used be used as a combinator for defining
induction schemes for mutually inductive types.

Add a Notation for `sn`: strongly normalizing.

See merge request robbertkrebbers/coq-stdpp!25

As we have for all classes for binary relations.

typeclass comments

See merge request robbertkrebbers/coq-stdpp!24

Lattices notation for order, join, meet, top and bot.

See merge request robbertkrebbers/coq-stdpp!23

Make x.1, x.2 notation compatible with ssrfun.

See merge request robbertkrebbers/coq-stdpp!21

Enable one to import both stdpp's base and ssrfun.

Note that (f x.1) now parses as (f (fst x)) rather than (fst (f x)).
(This change affects one proof in Iris.)

Allow compiling against "dev" version of Coq

See merge request robbertkrebbers/coq-stdpp!20

This matches e.g. Iris allowing a "dev" version of std++: You can install a
"dev" version to test stuff, but then you are responsible for making sure that
these versions actually work together.  We rely on that when testing things
against Iris master every night, for which purpose we install Iris master as
"dev" version.

Pattern matching notation for monadic binds

See merge request robbertkrebbers/coq-stdpp!18

This gets rid of the old hack to have specific notations for pairs
up to a fixed arity, and moreover allows to do fancy things like:

```
Record test := Test { t1 : nat; t2 : nat }.

Definition foo (x : option test) : option nat :=
  ''(Test a1 a2) ← x;
  Some a1.
```

This one works for setoid rewriting under binders.

Factor out solve_proper_prepare

See merge request robbertkrebbers/coq-stdpp!19