Fixes #3166.

Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>

- Warn in some places where {x:T} is not assumed to occur (e.g. in
  argument of an application, or of a match).
- Warn when an implicit argument occurs several times with the same name.
- Accept local anonymous {_:T} with explicitation possible using name `arg_k`.

We obtain this by using a flag (impl_binder_index) which tells if we
are in a position where implicit arguments matter and, if yes, the
index of the next binder.

This clean-up removes the dependency of the current proof mode (and hence
the parsing state) on unification.

The current proof mode can now be known simply by parsing and elaborating
attributes. We give access to attributes from the classifier for this purpose.

We remove the infamous `VtUnknown` code path in the STM which is known to
be buggy.

Fixes #3632 #3890 #4638.

I don't think there's a reason to treat such variables more severely
than unbound variables. This anomaly is often raised by debug printers
(e.g. when studying complex scenarios using `Set Unification Debug`),
and so makes debugging less convenient.

Fixes #3754, fixes #10026.