From 823173da1fb712d25c450ce7b48675d90af773eb Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Sep 2003 19:37:34 +0000
Subject: Ajout nouvelles commandes

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

diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index c26c98c4e7..9d18cfc913 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -57,6 +57,7 @@
 \maketitle
 
 \section{Meta notations used in this document}
+$\xi$
 
 Non-terminals are printed between angle brackets (e.g. $\NT{non-terminal}$) and
 terminal symbols are printed in bold font (e.g. $\ETERM{terminal}$). Lexemes
@@ -491,6 +492,7 @@ Conflicts exists between integers and constrs.
        \TERM{using}~\NT{constr-with-bindings}
 \SEPDEF
 \DEFNT{constr-with-bindings}
+       % dangling ``with'' of ``fix'' can conflict with ``with''
        \NTL{constr}{100}~\OPT{\NT{with-binding-list}}
 \SEPDEF
 \DEFNT{with-binding-list}
@@ -537,7 +539,6 @@ Conflicts exists between integers and constrs.
        ~\TERM{]}}~\OPT{\TERM{destructuring}}~\OPTGR{\TERM{using}~\TERM{tdb}}
 \end{rules}
 
-
 \subsection{Ltac}
 
 Additional symbols are:
@@ -898,6 +899,7 @@ $$
 \nlsep \TERM{Hint}~\OPT{\NT{reference}}
 \nlsep \TERM{Hint}~\TERM{*}
 \nlsep \TERM{HintDb}~\NT{ident}
+\nlsep \TERM{Scopes}
 \nlsep \TERM{Scope}~\NT{ident}
 \SEPDEF
 \DEFNT{class-rawexpr}
@@ -1036,7 +1038,8 @@ $$
 \begin{rules}
 \DEFNT{syntax}
        \TERM{Open}~\TERM{Scope}~\NT{ident}
-\nlsep \TERM{Delimits}~\TERM{Scope}~\NT{ident}~\KWD{with}~\NT{ident}
+\nlsep \TERM{Delimit}~\TERM{Scope}~\NT{ident}~\KWD{with}~\NT{ident}
+\nlsep \TERM{Bind}~\TERM{Scope}~\NT{ident}~\KWD{with}~\PLUS{\NT{class-rawexpr}}
 \nlsep \TERM{Arguments}~\TERM{Scope}~\NT{reference}
        ~\TERM{[}~\PLUS{\NT{name}}~\TERM{]}
 \nlsep \TERM{Infix}~\OPT{\TERM{Local}} %%% ~\NT{prec}~\OPT{\NT{int}}
-- 
cgit v1.2.3