More flexibility in locating or referring to a notation.

We generalize the possibility to refer to a notation not only by its
"_ U _" form but also using its "a 'U' b".

(Wish from EJGA)

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index d597bf7a6a..74e120a316 100644
--- a/CHANGES
+++ b/CHANGES
@@ -16,6 +16,8 @@ Notations
 - Recursive notations now support ".." patterns with several
   occurrences of the recursive term or binder, possibly mixing terms
   and binders, possibly in reverse left-to-right order.
+- "Locate" now working also on notations of the form "x + y" (rather
+  than "_ + _").
 
 Specification language