Adopting the same rules for interpreting @, abbreviations and

notations in patterns than in terms, wrt implicit arguments and
scopes.

See file Notations2.v for the conventions in use in terms.

Somehow this could be put in 8.5 since it puts in agreement the
interpretation of abbreviations and notations in "symmetric patterns"
to what is done in terms (even though the interpretation rules for
terms are a bit ad hoc).

There is one exception: in terms, "(foo args) args'" deactivates the
implicit arguments and scopes in args'. This is a bit complicated to
implement in patterns so the syntax is not supported (and anyway, this
convention is a bit questionable).

0 files changed, 0 insertions, 0 deletions