From ee0d4870fb982877be7cf07c75e3d039b82ddfc0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 28 Jun 2016 01:10:05 +0200
Subject: Documenting the "only printing" notation flag.

---
 doc/refman/RefMan-syn.tex | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'doc/refman/RefMan-syn.tex')

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index 1f08b6a2f1..e91480ded3 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -321,6 +321,10 @@ Sometimes, a notation is expected only for the parser.
 To do so, the option {\em only parsing} is allowed in the list of modifiers of
 \texttt{Notation}.
 
+Conversely, the {\em only printing} can be used to declare
+that a notation should only be used for printing and should not declare a
+parsing rule. In particular, such notations do not modify the parser.
+
 \subsection{The \texttt{Infix} command
 \comindex{Infix}}
 
@@ -480,6 +484,7 @@ Locate "exists _ .. _ , _".
   & $|$ & {\ident} {\tt global} \\
   & $|$ & {\ident} {\tt bigint} \\
   & $|$ & {\tt only parsing} \\
+  & $|$ & {\tt only printing} \\
   & $|$ & {\tt format} {\str} 
 \end{tabular}
 \end{centerframe}
-- 
cgit v1.2.3

