diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 259f5e0546..f454f4313d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -857,7 +857,8 @@ example showing a notation for a chain of equalities. It relies on an artificial expansion of the intended denotation so as to expose a ``φ(x, .. φ(y,t) ..)`` structure, with the drawback that if ever the beta-redexes are contracted, the notations stops to be used for -printing. +printing. Support for notations defined in this way should be considered +experimental. .. coqtop:: in |