Remove superfluous spaces and commas in tactic documentation.

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

2 files changed, 26 insertions, 25 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 97a9b326b..b21e0e9e2 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -75,10 +75,11 @@
 \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{\nelistwithoutblank}[2]{#1{\tt #2}\ldots{\tt #2}#1}
-\newcommand{\sequencewithoutblank}[2]{$[$#1{\tt #2}\ldots{\tt #2}#1$]$}
+\newcommand{\nelistnosep}[1]{{#1} \mbox{\dots} {#1}}
+\newcommand{\nelist}[2]{{#1} {\tt #2} \mbox{\dots} {\tt #2} {#1}}
+\newcommand{\sequence}[2]{{\sl [}{#1} {\tt #2} \mbox{\dots} {\tt #2} {#1}{\sl ]}}
+\newcommand{\nelistwithoutblank}[2]{#1{\tt #2}\mbox{\dots}{\tt #2}#1}
+\newcommand{\sequencewithoutblank}[2]{$[$#1{\tt #2}\mbox{\dots}{\tt #2}#1$]$}
 
 % Used for RefMan-gal
 %\newcommand{\ml}[1]{\hbox{\tt{#1}}}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 140420f64..72b5593e9 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -301,7 +301,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form
   premises. Here, variables are referred by names and non-dependent
   products by increasing numbers (see syntax in Section~\ref{Binding-list}).
 
-\item {\tt apply} {\term$_1$} {\tt ,} \ldots {\tt ,} {\term$_n$}
+\item {\tt apply \term$_1$ , \mbox{\dots} , \term$_n$}
 
   This is a shortcut for {\tt apply} {\term$_1$} {\tt ; [ ..~|}
    \ldots~{\tt ; [ ..~| {\tt apply} {\term$_n$} ]} \ldots~{\tt ]}, i.e. for the
@@ -518,16 +518,16 @@ This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in
 {\ident}} but turns unresolved bindings into existential variables, if
 any, instead of failing.
 
-\item {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+\item {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
 
-This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in
+This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in
 {\ident}} then destructs the hypothesis {\ident} along
 {\disjconjintropattern} as {\tt destruct {\ident} as
 {\disjconjintropattern}} would.
 
-\item {\tt eapply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
+\item {\tt eapply \nelist{{\term} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}}
 
-This works as {\tt apply \nelist{{\term}{,} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}.
+This works as {\tt apply \nelist{{\term} with {\bindinglist}}{,} in {\ident} as {\disjconjintropattern}} but using {\tt eapply}.
 
 \item {\tt simple apply {\term} in {\ident}}
 \tacindex{simple apply \dots\ in}
@@ -1036,17 +1036,17 @@ be substituted in the context. The {\tt in {\occgoalset}} clause is an
 occurrence clause whose syntax and behavior are described in
 Section~\ref{Occurrences clauses}.
 
-\item {\tt set ( {\ident} \nelist{\binder}{} := {\term} )}
+\item {\tt set ( {\ident} \nelistnosep{\binder} := {\term} )}
 
   This is equivalent to {\tt set ( {\ident} := fun
-  \nelist{\binder}{} => {\term} )}.
+  \nelistnosep{\binder} => {\term} )}.
 
 \item {\tt set \term}
 
   This behaves as {\tt set (} {\ident} := {\term} {\tt )} but {\ident}
   is generated by {\Coq}. This variant also supports an occurrence clause.
 
-\item {\tt set ( {\ident$_0$} \nelist{\binder}{} := {\term} ) in {\occgoalset}}\\
+\item {\tt set ( {\ident$_0$} \nelistnosep{\binder} := {\term} ) in {\occgoalset}}\\
       {\tt set {\term} in {\occgoalset}}
 
   These are the general forms which combine the previous possibilities.
@@ -1073,10 +1073,10 @@ Section~\ref{Occurrences clauses}.
   hypotheses. It is equivalent to {\tt set ( {\ident} {\tt :=}
   {\term} {\tt ) in |-}}.
 
-\item {\tt pose ( {\ident} \nelist{\binder}{} := {\term} )}
+\item {\tt pose ( {\ident} \nelistnosep{\binder} := {\term} )}
 
   This is equivalent to {\tt pose (} {\ident} {\tt :=} {\tt fun}
-  \nelist{\binder}{} {\tt =>} {\term} {\tt )}.
+  \nelistnosep{\binder} {\tt =>} {\term} {\tt )}.
 
 \item{\tt pose {\term}}
 
@@ -2126,15 +2126,15 @@ introduced hypothesis.
 
   \ErrMsg \errindex{goal does not satisfy the expected preconditions}
 
-\item \texttt{injection {\term} \zeroone{with \bindinglist} as \nelist{\intropattern}{}}\\
+\item \texttt{injection {\term} \zeroone{with \bindinglist} as \nelistnosep{\intropattern}}\\
 \texttt{injection {\num} as {\intropattern} \dots\ \intropattern}\\
 \texttt{injection as {\intropattern} \dots\ \intropattern}\\
-\texttt{einjection {\term} \zeroone{with \bindinglist} as \nelist{\intropattern}{}}\\
+\texttt{einjection {\term} \zeroone{with \bindinglist} as \nelistnosep{\intropattern}}\\
 \texttt{einjection {\num} as {\intropattern} \dots\ \intropattern}\\
 \texttt{einjection as {\intropattern} \dots\ \intropattern}
 \tacindex{injection \dots\ as}
 
-These variants apply \texttt{intros} \nelist{\intropattern}{} after
+These variants apply \texttt{intros} \nelistnosep{\intropattern} after
 the call to \texttt{injection} or \texttt{einjection}.
 
 \end{Variants}
@@ -2448,14 +2448,14 @@ time of the interactive development of a proof, use the command {\tt
 
 \begin{Variants}
   \item {\tt fix \ident$_1$ {\num} with ( \ident$_2$
-    \nelist{\binder$_2$}{} \zeroone{\{ struct \ident$'_2$
+    \nelistnosep{\binder$_2$} \zeroone{\{ struct \ident$'_2$
       \}} :~\type$_2$ ) \dots\ ( \ident$_n$
-    \nelist{\binder$_n$}{} \zeroone{\{ struct \ident$'_n$ \}} :~\type$_n$ )}
+    \nelistnosep{\binder$_n$} \zeroone{\{ struct \ident$'_n$ \}} :~\type$_n$ )}
 
 This starts a proof by mutual induction. The statements to be
 simultaneously proved are respectively {\tt forall}
-  \nelist{{\binder}$_2$}{}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
-  \nelist{{\binder}$_n$}{}{\tt ,} {\type}$_n$.  The identifiers
+  \nelistnosep{{\binder}$_2$}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
+  \nelistnosep{{\binder}$_n$}{\tt ,} {\type}$_n$.  The identifiers
 {\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the induction
 hypotheses. The identifiers {\ident}$'_2$ {\ldots} {\ident}$'_n$ are the
 respective names of the premises on which the induction is performed
@@ -2480,13 +2480,13 @@ command {\tt Guarded} (see Section~\ref{Guarded}).
 
 \begin{Variants}
   \item {\tt cofix \ident$_1$ with ( \ident$_2$
-    \nelist{\binder$_2$}{} :~\type$_2$ ) \dots\ (
-    \ident$_n$ \nelist{\binder$_n$}{} :~\type$_n$ )}
+    \nelistnosep{\binder$_2$} :~\type$_2$ ) \dots\ (
+    \ident$_n$ \nelistnosep{\binder$_n$} :~\type$_n$ )}
 
 This starts a proof by mutual coinduction. The statements to be
 simultaneously proved are respectively {\tt forall}
-\nelist{{\binder}$_2$}{}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
-  \nelist{{\binder}$_n$}{}{\tt ,} {\type}$_n$. The identifiers
+\nelistnosep{{\binder}$_2$}{\tt ,} {\type}$_2$, {\ldots}, {\tt forall}
+  \nelistnosep{{\binder}$_n$}{\tt ,} {\type}$_n$. The identifiers
     {\ident}$_1$ {\ldots} {\ident}$_n$ are the names of the
     coinduction hypotheses.