Improving rendering of ...-separated lists and sequences in reference

manual (making style uniform: no {\tt \ldots}; using only one space
when there is no delimiters in the sequence).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15729 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 18 insertions, 18 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index ca43a81f1..d0512c852 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -75,8 +75,8 @@
 \newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
 %\newcommand{\zeroonemany}[1]{$\{$#1$\}$*}
 %\newcommand{\onemany}[1]{$\{$#1$\}$+}
-\newcommand{\nelist}[2]{{#1} {\tt #2}~{\ldots}~{\tt #2} {#1}}
-\newcommand{\sequence}[2]{{\sl [}{#1} {\tt #2}~{\ldots}~{\tt #2} {#1}{\sl ]}}
+\newcommand{\nelist}[2]{{#1} {\tt #2} {\ldots} {\tt #2} {#1}}
+\newcommand{\sequence}[2]{{\sl [}{#1} {\tt #2} {\ldots} {\tt #2} {#1}{\sl ]}}
 \newcommand{\nelistwithoutblank}[2]{#1{\tt #2}\ldots{\tt #2}#1}
 \newcommand{\sequencewithoutblank}[2]{$[$#1{\tt #2}\ldots{\tt #2}#1$]$}
 
@@ -168,7 +168,7 @@
 \newcommand{\flag}{\nterm{flag}}
 \newcommand{\form}{\nterm{form}}
 \newcommand{\entry}{\nterm{entry}} 
-\newcommand{\proditem}{\nterm{production\_item}} 
+\newcommand{\proditem}{\nterm{production\_item}}
 \newcommand{\taclevel}{\nterm{tactic\_level}}
 \newcommand{\tacargtype}{\nterm{tactic\_argument\_type}} 
 \newcommand{\scope}{\nterm{scope}} 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 2c4985c15..fa7c58de8 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -267,10 +267,10 @@ available. The command to activate it is
 The corresponding grammar rules are given Figure~\ref{fig:projsyntax}.
 When {\qualid} denotes a projection, the syntax {\tt
   {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax
-{\tt {\term}.({\qualid}~{\termarg}$_1$~ \ldots~ {\termarg}$_n$)} to
-{\qualid~{\termarg}$_1$ \ldots {\termarg}$_n$~\term}, and the syntax
-{\tt {\term}.(@{\qualid}~{\term}$_1$~\ldots~{\term}$_n$)} to
-{@\qualid~{\term}$_1$ \ldots {\term}$_n$~\term}. In each case, {\term}
+{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to
+{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax
+{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to
+{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term}
 is the object projected and the other arguments are the parameters of
 the inductive type.
 
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 6fa7596db..8af3a95d4 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -772,13 +772,13 @@ a postulate.
   {\tt Parameter {\ident} :{\term}.} \\
   Is equivalent to {\tt Axiom {\ident} : {\term}}
 
-\item {\tt Parameter {\ident$_1$}\ldots{\ident$_n$} {\tt :}{\term}.}\\
+\item {\tt Parameter {\ident$_1$} {\ldots} {\ident$_n$} {\tt :}{\term}.}\\
   Adds $n$ parameters with specification {\term}
 
 \item
  {\tt Parameter\,%
-(\,{\ident$_{1,1}$}\ldots{\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\,%
-\ldots\,{\tt (}\,{\ident$_{n,1}$}\ldots{\ident$_{n,k_n}$}\,{\tt :}\,%
+(\,{\ident$_{1,1}$} {\ldots} {\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\;%
+\ldots\;{\tt (}\,{\ident$_{n,1}$}{\ldots}{\ident$_{n,k_n}$}\,{\tt :}\,%
 {\term$_n$} {\tt )}.}\\ 
   Adds $n$ blocks of parameters with different specifications.
 
@@ -808,12 +808,12 @@ Variable} command out of any section is equivalent to using {\tt Parameter}.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt Variable {\ident$_1$}\ldots{\ident$_n$} {\tt :}{\term}.}\\
-  Links {\term} to names {\ident$_1$}\ldots{\ident$_n$}.
+\item {\tt Variable {\ident$_1$} {\ldots} {\ident$_n$} {\tt :}{\term}.}\\
+  Links {\term} to names {\ident$_1$} {\ldots} {\ident$_n$}.
 \item
  {\tt Variable\,%
-(\,{\ident$_{1,1}$}\ldots{\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\,%
-\ldots\,{\tt (}\,{\ident$_{n,1}$}\ldots{\ident$_{n,k_n}$}\,{\tt :}\,%
+(\,{\ident$_{1,1}$} {\ldots} {\ident$_{1,k_1}$}\,{\tt :}\,{\term$_1$} {\tt )}\;%
+\ldots\;{\tt (}\,{\ident$_{n,1}$} {\ldots}{\ident$_{n,k_n}$}\,{\tt :}\,%
 {\term$_n$} {\tt )}.}\\ 
   Adds $n$ blocks of variables with different specifications.
 \item \comindex{Hypothesis}
@@ -870,17 +870,17 @@ environment, provided that {\term} is well-typed.
   It checks that the type of {\term$_2$} is definitionally equal to
   {\term$_1$}, and registers {\ident} as being of type {\term$_1$},
   and bound to value {\term$_2$}.
-\item {\tt Definition {\ident} {\binder$_1$}\ldots{\binder$_n$}
+\item {\tt Definition {\ident} {\binder$_1$} {\ldots} {\binder$_n$}
        {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
   This is equivalent to \\
    {\tt Definition\,{\ident}\,{\tt :\,forall}\,%
-       {\binder$_1$}\ldots{\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}}\,%
-       {\tt fun}\,{\binder$_1$}\ldots{\binder$_n$}\,{\tt =>}\,{\term$_2$}\,%
+       {\binder$_1$} {\ldots} {\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}}\,%
+       {\tt fun}\,{\binder$_1$} {\ldots} {\binder$_n$}\,{\tt =>}\,{\term$_2$}\,%
        {\tt .}
 
 \item {\tt Example {\ident} := {\term}.}\\
 {\tt Example {\ident} {\tt :}{\term$_1$} := {\term$_2$}.}\\
-{\tt Example {\ident} {\binder$_1$}\ldots{\binder$_n$}
+{\tt Example {\ident} {\binder$_1$} {\ldots} {\binder$_n$}
        {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
 \comindex{Example}
 These are synonyms of the {\tt Definition} forms.