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.

0 files changed, 0 insertions, 0 deletions