Merge PR #13613: [changes] mark #12765 as experimental

Reviewed-by: Zimmi48
coq · Dec 14, 2020 · d0667eb · d0667eb
2 parents 2648803 + 92204c4
commit d0667eb
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git 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:**

diff --git 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