aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorherbelin2003-11-23 20:14:00 +0000
committerherbelin2003-11-23 20:14:00 +0000
commit9f052abd045f0d752857a5fecc2cb4aa2358fa80 (patch)
tree1a93d8776cc0bb9f5911b7f1be03eff563c354a6 /doc
parent48c28d5a12a13ef2cc04f4df0dd93b994749821a (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.tex16
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}