diff options
author | 2003-11-23 22:01:28 +0000 | |
---|---|---|
committer | 2003-11-23 22:01:28 +0000 | |
commit | 37f4d3ed71de4feff333f982eb3f6cd6d4efe36d (patch) | |
tree | ef67abbd0364f8779ac6f92a7f810b68125a91d9 | |
parent | d7737b222b1374645624159b4a2a6e8f0c569d57 (diff) |
MAJs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4975 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | doc/syntax-v8.tex | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex index f22ad3516..43536de0b 100644 --- a/doc/syntax-v8.tex +++ b/doc/syntax-v8.tex @@ -255,7 +255,7 @@ conflict can appear, $\NTL{constr}{200}$ is also used as entry point. \DEFNT{fix-kw} \KWD{fix} ~\mid~ \KWD{cofix} \SEPDEF \DEFNT{fix-decl} - \NT{ident}~\STAR{\NT{binder}}~\OPT{\NT{annot}}~\NT{type-cstr} + \NT{ident}~\STAR{\NT{binder-let}}~\OPT{\NT{annot}}~\NT{type-cstr} ~\KWD{:=}~\NTL{constr}{200} \SEPDEF \DEFNT{annot} @@ -876,7 +876,7 @@ $$ \NT{rec-definition}~\STARGR{\KWD{with}~\NT{rec-definition}} \SEPDEF \DEFNT{rec-definition} - \NT{ident}~\STAR{\NT{binder}}~\OPT{\NT{annot}}~\NT{type-cstr} + \NT{ident}~\STAR{\NT{binder-let}}~\OPT{\NT{annot}}~\NT{type-cstr} ~\KWD{:=}~\NT{constr} \SEPDEF \DEFNT{scheme} @@ -1018,13 +1018,14 @@ $$ \nlsep \TERM{Coercions} \nlsep \TERM{Coercion}~\TERM{Paths}~\NT{class-rawexpr}~\NT{class-rawexpr} \nlsep \TERM{Tables} -\nlsep \TERM{Proof}~\NT{reference} +% \nlsep \TERM{Proof}~\NT{reference} % Obsolete, useful in V6.3 ?? \nlsep \TERM{Hint}~\OPT{\NT{reference}} \nlsep \TERM{Hint}~\TERM{*} \nlsep \TERM{HintDb}~\NT{ident} \nlsep \TERM{Scopes} \nlsep \TERM{Scope}~\NT{ident} \nlsep \TERM{Visibility}~\OPT{\NT{ident}} +\nlsep \TERM{Implicit}~\NT{qualid} \SEPDEF \DEFNT{class-rawexpr} \TERM{Funclass}~\mid~\TERM{Sortclass}~\mid~\NT{reference} |