diff options
| author | Enrico Tassi | 2020-12-11 11:15:23 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-12-11 11:15:23 +0100 |
| commit | 92204c4c964c1699f2ad3c25104e97ddfc4cc73c (patch) | |
| tree | 4e24d3b407a6ae82738f39c8f6655940fa0cf09e /doc/sphinx/changes.rst | |
| parent | 1918f19cb43d6d4313276b167af38316b27879f2 (diff) | |
[changes] mark #12765 as experimental
Diffstat (limited to 'doc/sphinx/changes.rst')
| -rw-r--r-- | doc/sphinx/changes.rst | 3 |
1 files changed, 2 insertions, 1 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 <https://github.com/coq/coq/pull/12765>`_, by Hugo Herbelin). - **Added:** |