diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-24 21:14:43 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:07 +0100 |
commit | b176959335a8cc097c254ea10b910e8ecbcde54b (patch) | |
tree | 3f4e97333b49df88a3be64ed61f4b30876dbe8f5 /CHANGES | |
parent | 5b2f29e461d7dfb1336117050cc8c5d510025bf1 (diff) |
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)
Diffstat (limited to 'CHANGES')
-rw-r--r-- | CHANGES | 2 |
1 files changed, 2 insertions, 0 deletions
@@ -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 |