3 files changed, 20 insertions, 3 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 5ba3c308a6..9fbff7181e 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1277,7 +1277,7 @@ Prints the profile
 Prints a profile for all tactics that start with {\qstring}. Append a period (.) to the string if you only want exactly that name.
 
 \begin{quote}
-{\tt Reset Profile}.
+{\tt Reset Ltac Profile}.
 \end{quote}
 Resets the profile, that is, deletes all accumulated information
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 6a8bda35d6..919e7b5cdc 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -87,7 +87,7 @@ is restored when the current \emph{section} ends.
 \item {\tt Global Unset {\rm\sl flag}.\comindex{Global Unset}}\\
 This command switches {\rm\sl flag} off.  The original state of
 {\rm\sl flag} is \emph{not} restored at the end of the module. Additionally,
-if set in a file, {\rm\sl flag} is switched on when the file is
+if set in a file, {\rm\sl flag} is switched off when the file is
 {\tt Require}-d.
 \end{Variants}
 
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index e91480ded3..92107b750b 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -589,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}).
@@ -634,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}