Fixing some residual bugs of PR #10202 (manual implicit args in subterms).

- Implicit arguments in the return clause and in the branches
  of a match were not checked.
- Implicit arguments in each declaration of intern_context were not
  restarted.
- Additionally, in intern_context, we take into account ids from the
  env on top of which intern_context is called.
- A better approximation of the check for manual implicit in notations
  improved (though not fully correct because the exact context of
  interpretation of a binder in a notation with recursive binders is
  not known).

We also rename impl_binder_index into binder_block_names in anticipation of
checking redundancies also for non-implicit arguments.

0 files changed, 0 insertions, 0 deletions