Notations can now accept dummy arguments. If ever a bound variable is not
used, they are automatically flagged as only parsing. CAVEAT: unused
arguments are not typechecked, because they are dropped before the
interpretation phase.
Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at
internalization time.