aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/changes.md
diff options
context:
space:
mode:
Diffstat (limited to 'dev/doc/changes.md')
-rw-r--r--dev/doc/changes.md6
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