Commit 42f27beb63a629dcef514abb0b31dea193f35a38: Fix incorrect documentation
that prevents successful compilation (bug #5265).

--- doc/refman/RefMan-syn.tex.orig	2016-12-08 08:13:52.000000000 -0700
+++ doc/refman/RefMan-syn.tex	2016-12-16 10:43:42.840463129 -0700
@@ -649,7 +649,7 @@
 pattern for terms. Here is an example:
 
 \begin{coq_example*}
-Notation ``'FUNAPP' x .. y , f'' :=
+Notation "'FUNAPP' x .. y , f" :=
   (fun x => .. (fun y => (.. (f x) ..) y ) ..)
   (at level 200, x binder, y binder, right associativity).
 \end{coq_example*}