diff options
| author | Hugo Herbelin | 2018-03-08 18:22:50 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-12-04 11:50:02 +0100 |
| commit | 06fc6caa49b67526cf3521d1b5885aae6710358b (patch) | |
| tree | c893a474c67d9f569e1e19c7ccaedb1a02ada4f5 /dev | |
| parent | 74dfaaa8555f53bfc75216205823a8020e80b6a1 (diff) | |
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.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.md | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index acb0d80c18..c0f15f02a5 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -152,6 +152,12 @@ Termops - Internal printing functions have been placed under the `Termops.Internal` namespace. +Notations: + +- Notation.availability_of_notation is not anymore needed: if a + delimiter is needed, it is provided by Notation.uninterp_notation + which fails in case the notation is not available. + ### Unit testing The test suite now allows writing unit tests against OCaml code in the Coq |