Manual implicit arguments: more robustness tests.

- 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.

0 files changed, 0 insertions, 0 deletions