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.

3 files changed, 39 insertions, 2 deletions

diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out
index c142d28ebe..0a989646cf 100644
--- a/test-suite/output/Naming.out
+++ b/test-suite/output/Naming.out
@@ -61,3 +61,18 @@
   H : a = 0 -> forall a : nat, a = 0
   ============================
   a = 0
+File "stdin", line 101, characters 47-48:
+Warning: Ignoring implicit binder declaration in unexpected position.
+[unexpected-implicit-declaration,syntax]
+File "stdin", line 105, characters 36-37:
+Warning: Ignoring implicit binder declaration in unexpected position.
+[unexpected-implicit-declaration,syntax]
+File "stdin", line 106, characters 34-35:
+Warning: Ignoring implicit binder declaration in unexpected position.
+[unexpected-implicit-declaration,syntax]
+File "stdin", line 112, characters 22-23:
+Warning: Ignoring implicit binder declaration in unexpected position.
+[unexpected-implicit-declaration,syntax]
+File "stdin", line 112, characters 30-31:
+Warning: Ignoring implicit binder declaration in unexpected position.
+[unexpected-implicit-declaration,syntax]
diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v
index 7f3b332d7d..610fa48c0c 100644
--- a/test-suite/output/Naming.v
+++ b/test-suite/output/Naming.v
@@ -90,3 +90,25 @@ apply H with (a:=a). (* test compliance with printing *)
 Abort.
 
 End A.
+
+Module B.
+
+(* Check valid/invalid implicit arguments *)
+Definition f1 {x} (y:forall {x}, x=0) := x+0.
+Definition f2 := (((fun x => 0):forall {x:nat}, nat), 0).
+Definition f3 := fun {x} (y:forall {x}, x=0) => x+0.
+
+Definition g1 {x} := match x with true => fun {x:bool} => x | false => fun x:bool => x end.
+(* TODO: do not ignore the implicit here *)
+Definition g2 '(x,y) {z} := x+y+z.
+
+Definition h1 := fun x:nat => (fun {x} => x) 0.
+Definition h2 := let g := forall {y}, y=0 in g.
+
+Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity,
+  format "'[  ' '[  ' ∀  x  ..  y ']' ,  '/' P ']'") : type_scope.
+
+Definition l1 := ∀ {x:nat} {y:nat}, x=0.
+
+End B.
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index aeebc0f98b..839df99ea7 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -219,8 +219,8 @@ Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0.
 Module G.
 Generalizable Variables A R.
 Class Reflexive {A:Type} (R : A->A->Prop) := reflexivity : forall x : A, R x x.
-Check exists_true `{Reflexive A R}, forall x, R x x.
-Check exists_true x `{Reflexive A R} y, x+y=0 -> forall z, R z z.
+Check exists_true `(Reflexive A R), forall x, R x x.
+Check exists_true x `(Reflexive A R) y, x+y=0 -> forall z, R z z.
 End G.
 
 (* Allows recursive patterns for binders to be associative on the left *)