From b6227b96055836b8d0c78d918d67adf4f647e626 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 Sep 2003 17:09:37 +0000
Subject: MAJ

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

(limited to 'doc')

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}
-- 
cgit v1.2.3