From 06fc6caa49b67526cf3521d1b5885aae6710358b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 8 Mar 2018 18:22:50 +0100
Subject: 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.
---
 dev/doc/changes.md | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'dev')

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
-- 
cgit v1.2.3