Addressing issues with PR#873: performance and use of abbreviation for printing.

We do a couple of changes:

- Splitting notation keys into more categories to make table smaller.
  This should (a priori) make printing faster (see #6416).

- Abbreviations are treated for printing like single notations: they
  are pushed to the scope stack, so that in a situation such as

  Open Scope foo_scope.
  Notation foo := term.
  Open Scope bar_scope.

  one looks for notations first in scope bar_scope, then try to use
  foo, they try for notations in scope foo_scope.

- We seize the opportunity of this commit to simplify
  availability_of_notation which is now integrated to
  uninterp_notation and which does not have to be called explicitly
  anymore.

0 files changed, 0 insertions, 0 deletions