One more step in fixing #5762 ("where" clause).

We improve one step further the heuristics to sort out if a variable
is a notation variable or a named variable.

This allows to support the following which was still failing.

Reserved Notation "# x" (at level 0).
Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I).

We rely here on the property that a binding variable of same name as a
notation variables is itself considered bound by the notation.

This becomes however to be a bit tricky for sorting out if the
variable has to be output to the glob file or not.

2 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5762.v b/test-suite/bugs/closed/5762.v
index edd5c8d73d..55d36bd722 100644
--- a/test-suite/bugs/closed/5762.v
+++ b/test-suite/bugs/closed/5762.v
@@ -26,3 +26,9 @@ Reserved Notation "%% a" (at level 70).
 Record R :=
   {g : forall {A} (a:A), a=a where "%% x" := (g x);
    k : %% 0 = eq_refl}.
+
+(* An extra example *)
+
+Module A.
+Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I) : I_scope.
+End A.
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 9505a56e3f..e86b3edb83 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -90,3 +90,9 @@ Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
 Notation "##### x" := (pair' x) (at level 0, x at level 1).
 Check ##### 0 _ 0%bool 0%bool : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
+
+(* 10. Check computation of binding variable through other notations *)
+(* i should be detected as binding variable and the scopes not being checked *)
+
+Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200).
+Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200).