aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorVincent Laporte2019-04-24 11:48:46 +0000
committerVincent Laporte2019-04-29 09:51:05 +0000
commit0e35f5f41b185309cbec3670ec8cfa8526e5fecf (patch)
tree3c1571974112898b93523b1f026755f9dc0b97a0 /dev
parent2c18da20b260c55d8da49b1bb4f53e72dbc75a87 (diff)
Revert #8187
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/changes.md6
1 files changed, 0 insertions, 6 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 4533a4dc01..9e0d47651e 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -203,12 +203,6 @@ 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