diff options
| author | herbelin | 2003-09-22 17:09:37 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-22 17:09:37 +0000 |
| commit | b6227b96055836b8d0c78d918d67adf4f647e626 (patch) | |
| tree | 286f6016fef99694318cf267b87d96be4cdefed1 /doc | |
| parent | 9c3f02a3a1f3e7ca96c5de44f3d4142268c9d96c (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4448 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/syntax-v8.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex index 9d18cfc913..5ce975e04b 100644 --- a/doc/syntax-v8.tex +++ b/doc/syntax-v8.tex @@ -187,7 +187,8 @@ Note that \TERM{struct} is not a reserved identifier. &&\RNAME{if-case} \SEPDEF \DEFNT{appl-arg} - \KWD{@}~\NT{int}~\!\KWD{:=}~\NTL{constr}{9} &&\RNAME{impl-arg} +% \KWD{@}~\NT{int}~\!\KWD{:=}~\NTL{constr}{9} &&\RNAME{impl-arg} + \KWD{(}~\NT{ident}~\!\KWD{:=}~\NTL{constr}~\KWD{)} &&\RNAME{impl-arg} \nlsep \NTL{constr}{9} \SEPDEF \DEFNT{atomic-constr} @@ -846,8 +847,7 @@ $$ ~\NT{class-rawexpr}~\TERM{$>->$}~\NT{class-rawexpr} \nlsep \TERM{Implicit}~\TERM{Arguments}~\NT{reference}~\TERM{[}~\STAR{\NT{int}}~\TERM{]} \nlsep \TERM{Implicit}~\TERM{Arguments}~\NT{reference} -\nlsep \TERM{Implicit}~\TERM{Variable}~\KWD{Type}~\PLUS{\NT{ident}} - ~\KWD{:}~\NT{constr} +\nlsep \TERM{Implicit}~\KWD{Type}~\PLUS{\NT{ident}}~\KWD{:}~\NT{constr} \SEPDEF \DEFNT{command} \TERM{Comments}~\STAR{\NT{comment}} @@ -1047,7 +1047,7 @@ $$ ~\OPT{\NT{in-scope}} \nlsep \TERM{Notation}~\OPT{\TERM{Local}}~\NT{ident}~\KWD{:=}~\NT{constr} ~\OPT{\NT{modifiers}}~\OPT{\NT{in-scope}} -\nlsep \TERM{Uninterpreted}~\TERM{Notation}~\OPT{\TERM{Local}}~\NT{string} +\nlsep \TERM{Reserved}~\TERM{Notation}~\OPT{\TERM{Local}}~\NT{string} ~\OPT{\NT{modifiers}} \SEPDEF \DEFNT{modifiers} |