This one works for setoid rewriting under binders.

This way, we will be compabile with Iris's heap_lang, which puts ;;
at level 100.

This allows for more control over `Hint Mode`.

This provides significant robustness against looping type class search.

As a consequence, at many places throughout the library we had to add
additional typing information to lemmas. This was to be expected, since
most of the old lemmas were ambiguous. For example:

  Section fin_collection.
    Context `{FinCollection A C}.

    size_singleton (x : A) : size {[ x ]} = 1.

In this case, the lemma does not tell us which `FinCollection` with
elements `A` we are talking about. So, `{[ x ]}` could not only refer to
the singleton operation of the `FinCollection A C` in the section, but
also to any other `FinCollection` in the development. To make this lemma
unambigious, it should be written as:

  Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.

In similar spirit, lemmas like the one below were also ambiguous:

  Lemma lookup_alter_None {A} (f : A → A) m i j :
    alter f i m !! j = None ↔ m !! j = None.

It is not clear which finite map implementation we are talking about.
To make this lemma unambigious, it should be written as:

  Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
    alter f i m !! j = None ↔ m !! j = None.

That is, we have to specify the type of `m`.

See also Coq bug #5712.

This is needed to use coq-stdpp in developments with -type-in-type
as set_unfold will otherwise unify with any hyp, causing the
set_solver tactic to break.

To be consistent with Iris, see Iris commit 9ee62b3a.

To make it consistent with Forall_impl and map_Forall_impl. Also, put
the premises in the same order as those lemmas.

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing

This also solves a name clash with the extension order of CMRAs.

With Coq 8.6, you can no longer have intro patterns that give more names than
the constructor has.  Also, patterns with too few names are now interpreted as
filling up with "?", rather than putting the unnamed parts into the goal again.

Furthermore, it seems the behavior of "simplify_eq/=" changed, I guess
hypotheses are considered in different order now.  I managed to work around
this, but it all seem kind of fragile.

The next compilation failure is an "Anyomaly: ... Please report", so that's what I will do.

There was not really a need for the lattice type classes, so I removed
these.

These just make things more complicated, it would be more useful to
declare (efficient) decision procedures for each instance, so that
we can properly predict which instance we will get.

This class whose name is horrible and purpose is arbitrary seems to be a
leftover of some experiment with ch2o, a long time a ago.