diff options
| author | herbelin | 2003-09-12 19:37:34 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-12 19:37:34 +0000 |
| commit | 823173da1fb712d25c450ce7b48675d90af773eb (patch) | |
| tree | 148b5f4e6551fd51f23b2188c1b79d4bca30b961 | |
| parent | 03138f9be73a546345296c73409fc59a3a800d84 (diff) | |
Ajout nouvelles commandes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4389 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/syntax-v8.tex | 7 |
1 files 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}} |