Set Hint Mode for all classes in `base.v`.

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`.
4 jobs for master in 5 minutes and 53 seconds
Status Job ID Name Coverage
  Test
failed #3248
fp-timing
stdpp-coq8.5.3

00:00:55

passed #3247
fp-timing
stdpp-coq8.6

00:02:02

passed #3246
fp-timing
stdpp-coq8.6.1

00:03:00

passed #3245
fp-timing
stdpp-coq8.7

00:04:54

 
Name Stage Failure
failed
stdpp-coq8.5.3 Test There is an unknown failure, please try again
make[1]: Target 'all' not remade because of errors.
make[1]: Leaving directory '/builds/robbertkrebbers/coq-stdpp'
Makefile:19: recipe for target 'all' failed
make: *** [all] Error 2

real 0m0.361s
user 0m0.370s
sys 0m0.273s
ERROR: Build failed: exit code 1