diff options
| author | herbelin | 2003-11-23 20:14:00 +0000 |
|---|---|---|
| committer | herbelin | 2003-11-23 20:14:00 +0000 |
| commit | 9f052abd045f0d752857a5fecc2cb4aa2358fa80 (patch) | |
| tree | 1a93d8776cc0bb9f5911b7f1be03eff563c354a6 /doc | |
| parent | 48c28d5a12a13ef2cc04f4df0dd93b994749821a (diff) | |
Renommage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8366 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/RefMan-gal.tex | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/doc/RefMan-gal.tex b/doc/RefMan-gal.tex index 2e643e470f..ec4a221d71 100644 --- a/doc/RefMan-gal.tex +++ b/doc/RefMan-gal.tex @@ -24,19 +24,19 @@ An expression enclosed in square brackets \zeroone{\ldots} means at most one occurrence of this expression (this corresponds to an optional component). -The notation ``\nelist{\gensymbol}{sep}'' stands for a non empty -sequence of expressions parsed by the ``{\gensymbol}'' entry and +The notation ``\nelist{\entry}{sep}'' stands for a non empty +sequence of expressions parsed by {\entry} and separated by the literal ``{\tt sep}''\footnote{This is similar to the -expression ``{\gensymbol} $\{$ {\tt sep} {\gensymbol} $\}$'' in -standard BNF, or ``{\gensymbol} $($ {\tt sep} {\gensymbol} $)$*'' in +expression ``{\entry} $\{$ {\tt sep} {\entry} $\}$'' in +standard BNF, or ``{\entry} $($ {\tt sep} {\entry} $)$*'' in the syntax of regular expressions.}. -Similarly, the notation ``\nelist{\gensymbol}{}'' stands for a non -empty sequence of expressions parsed by the ``{\gensymbol}'' entry, +Similarly, the notation ``\nelist{\entry}{}'' stands for a non +empty sequence of expressions parsed by the ``{\entry}'' entry, without any separator between. -At the end, the notation ``\sequence{\gensymbol}{\tt sep}'' stands for a -possibly empty sequence of expressions parsed by the ``{\gensymbol}'' entry, +At the end, the notation ``\sequence{\entry}{\tt sep}'' stands for a +possibly empty sequence of expressions parsed by the ``{\entry}'' entry, separated by the literal ``{\tt sep}''. \section{Lexical conventions} |
