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/user-extensions/syntax-extensions.rst | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/user-extensions')

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