From d926a11a23fd6fae8bfec9e8b163c1a83ac33ebf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 26 Sep 2003 11:36:10 +0000
Subject: About, Infix

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4486 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/syntax-v8.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'doc')

diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 5ce975e04b..59d2a80e50 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -868,6 +868,7 @@ $$
 \nlsep \TERM{Print}~\OPT{\NT{printable}}
 \nlsep \TERM{Print}~\NT{reference}
 \nlsep \TERM{Inspect}~\NT{int}
+\nlsep \TERM{About}~\NT{reference}
 %%
 \nlsep \TERM{Search}~\NT{reference}~\OPT{\NT{in-out-modules}}
 \nlsep \TERM{SearchPattern}~\NT{constr-pattern}~\OPT{\NT{in-out-modules}}
@@ -1043,7 +1044,7 @@ $$
 \nlsep \TERM{Arguments}~\TERM{Scope}~\NT{reference}
        ~\TERM{[}~\PLUS{\NT{name}}~\TERM{]}
 \nlsep \TERM{Infix}~\OPT{\TERM{Local}} %%% ~\NT{prec}~\OPT{\NT{int}}
-       ~\NT{string}~\NT{reference}~\OPT{\NT{modifiers}}
+       ~\NT{string}~\KWD{:=}~\NT{reference}~\OPT{\NT{modifiers}}
        ~\OPT{\NT{in-scope}}
 \nlsep \TERM{Notation}~\OPT{\TERM{Local}}~\NT{ident}~\KWD{:=}~\NT{constr}
        ~\OPT{\NT{modifiers}}~\OPT{\NT{in-scope}}
-- 
cgit v1.2.3