From 92204c4c964c1699f2ad3c25104e97ddfc4cc73c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Dec 2020 11:15:23 +0100 Subject: [changes] mark #12765 as experimental --- doc/sphinx/changes.rst | 3 ++- doc/sphinx/user-extensions/syntax-extensions.rst | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 726a6309d4..fcb150e3da 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -370,7 +370,8 @@ Notations by Pierre Roux, review by Jason Gross and Jim Fehrle for the reference manual). - **Added:** - Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t` + Added support for encoding notations of the form :g:`x ⪯ y ⪯ .. ⪯ z ⪯ t`. + This feature is considered experimental. (`#12765 `_, by Hugo Herbelin). - **Added:** diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 73f90b0056..e9fe3e61bf 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 -- cgit v1.2.3