|
 |
06d597b |
Commit 42f27beb63a629dcef514abb0b31dea193f35a38: Fix incorrect documentation
|
|
|
06d597b |
that prevents successful compilation (bug #5265).
|
|
|
06d597b |
|
|
|
06d597b |
--- doc/refman/RefMan-syn.tex.orig 2016-12-08 08:13:52.000000000 -0700
|
|
|
06d597b |
+++ doc/refman/RefMan-syn.tex 2016-12-16 10:43:42.840463129 -0700
|
|
|
06d597b |
@@ -649,7 +649,7 @@
|
|
|
06d597b |
pattern for terms. Here is an example:
|
|
|
06d597b |
|
|
|
06d597b |
\begin{coq_example*}
|
|
|
06d597b |
-Notation ``'FUNAPP' x .. y , f'' :=
|
|
|
06d597b |
+Notation "'FUNAPP' x .. y , f" :=
|
|
|
06d597b |
(fun x => .. (fun y => (.. (f x) ..) y ) ..)
|
|
|
06d597b |
(at level 200, x binder, y binder, right associativity).
|
|
|
06d597b |
\end{coq_example*}
|