1 files changed, 35 insertions, 13 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index aabc8a8995..21c39de967 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}}
 
@@ -358,7 +362,7 @@ state of {\Coq}.
 Reserved Notation "x = y" (at level 70, no associativity).
 \end{coq_example}
 
-Reserving a notation is also useful for simultaneously defined an
+Reserving a notation is also useful for simultaneously defining an
 inductive type or a recursive constant and a notation for it.
 
 \Rem The notations mentioned on Figure~\ref{init-notations} are
@@ -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}
@@ -584,6 +589,14 @@ Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c )  * u |]" :=
   (t at level 39).
 \end{coq_example*}
 
+Recursive patterns can occur several times on the right-hand side.
+Here is an example:
+
+\begin{coq_example*}
+Notation "[> a , .. , b <]" :=
+  (cons a .. (cons b nil) .., cons b .. (cons a nil) ..).
+\end{coq_example*}
+
 Notations with recursive patterns can be reserved like standard
 notations, they can also be declared within interpretation scopes (see
 section \ref{scopes}).
@@ -629,7 +642,16 @@ empty. Here is an example of recursive notation with closed binders:
 \begin{coq_example*}
 Notation "'mylet' f x .. y :=  t 'in' u":=
   (let f := fun x => .. (fun y => t) .. in u)
-  (x closed binder, y closed binder, at level 200, right associativity).
+  (at level 200, x closed binder, y closed binder, right associativity).
+\end{coq_example*}
+
+A recursive pattern for binders can be used in position of a recursive
+pattern for terms. Here is an example:
+
+\begin{coq_example*}
+Notation "'FUNAPP' x .. y , f" :=
+  (fun x => .. (fun y => (.. (f x) ..) y ) ..)
+  (at level 200, x binder, y binder, right associativity).
 \end{coq_example*}
 
 \subsection{Summary}
@@ -789,13 +811,13 @@ constant have to be interpreted in a given scope. The command is
 \begin{quote}
 {\tt Arguments} {\qualid} \nelist{\name {\tt \%}\scope}{}
 \end{quote}
-where the list is the list of the arguments of {\qualid} eventually
-annotated with their {\scope}. Grouping round parentheses can
-be used to decorate multiple arguments with the same scope.
-{\scope} can be either a scope name or its delimiting key. For example
-the following command puts the first two arguments of {\tt plus\_fct}
-in the scope delimited by the key {\tt F} ({\tt Rfun\_scope}) and the
-last argument in the scope delimited by the key {\tt R} ({\tt R\_scope}).
+where the list is a prefix of the list of the arguments of {\qualid} eventually
+annotated with their {\scope}. Grouping round parentheses can be used to
+decorate multiple arguments with the same scope.  {\scope} can be either a scope
+name or its delimiting key. For example the following command puts the first two
+arguments of {\tt plus\_fct} in the scope delimited by the key {\tt F} ({\tt
+  Rfun\_scope}) and the last argument in the scope delimited by the key {\tt R}
+({\tt R\_scope}).
 
 \begin{coq_example*}
 Arguments plus_fct (f1 f2)%F x%R.
@@ -860,11 +882,11 @@ statically. For instance, if {\tt f} is a polymorphic function of type
 {\scope}, then {\tt a} of type {\tt t} in {\tt f~t~a} is not
 recognized as an argument to be interpreted in scope {\scope}.
 
-\comindex{Bind Scope} 
-Any global reference can be bound by default to an
-interpretation scope. The command to do it is
+\comindex{Bind Scope}
+More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be
+bound to an interpretation scope. The command to do it is
 \begin{quote}
-{\tt Bind Scope} {\scope} \texttt{with} {\qualid}
+{\tt Bind Scope} {\scope} \texttt{with} {\class}
 \end{quote}
 
 \Example