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.

1 files changed, 1 insertions, 1 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d011fb2e77..0fd47b8da1 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1589,7 +1589,7 @@ let query_command_selector ?loc = function
 let vernac_check_may_eval ~pstate ~atts redexp glopt rc =
   let glopt = query_command_selector glopt in
   let sigma, env = get_current_context_of_args ~pstate glopt in
-  let sigma, c = interp_open_constr env sigma rc in
+  let sigma, c = interp_open_constr ~expected_type:Pretyping.UnknownIfTermOrType env sigma rc in
   let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
   Evarconv.check_problems_are_solved env sigma;
   let sigma = Evd.minimize_universes sigma in