diff options
| author | herbelin | 2003-09-26 11:36:10 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-26 11:36:10 +0000 |
| commit | d926a11a23fd6fae8bfec9e8b163c1a83ac33ebf (patch) | |
| tree | 16a8943e5baf18c8f2eb9b254ce4e720f2c7243d | |
| parent | f87c74e95b89d61cc739bde85b95b3e5055d9b96 (diff) | |
About, Infix
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4486 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/syntax-v8.tex | 3 |
1 files changed, 2 insertions, 1 deletions
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}} |