Beautify tactic documentation a bit more.

- Do not use \\ in place of empty lines.
- Fix missing spaces after some \dots.
- Do not use monospace slanted for clauses.

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

2 files changed, 122 insertions, 79 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index b21e0e9e2..2704a28af 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -140,6 +140,7 @@
 \newcommand{\idparams}{\nterm{ident\_with\_params}}
 \newcommand{\statkwd}{\nterm{assertion\_keyword}} % vernac
 \newcommand{\termarg}{\nterm{arg}}
+\newcommand{\hintdef}{\nterm{hint\_definition}}
 
 \newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}}
 \newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 72b5593e9..dce35c6d9 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2528,21 +2528,25 @@ solved by unification, and some of the types \texttt{A}$_1$, \dots,
 \begin{ErrMsgs}
 \item \errindex{The term provided does not end with an equation}
 
-\item \errindex{Tactic generated a subgoal identical to the original goal}\\
+\item \errindex{Tactic generated a subgoal identical to the original goal}
+
 This happens if \term$_1$ does not occur in the goal.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt rewrite -> {\term}}\tacindex{rewrite ->}\\
+\item {\tt rewrite -> \term}\tacindex{rewrite ->}
+
   Is equivalent to {\tt rewrite \term}
 
-\item {\tt rewrite <- {\term}}\tacindex{rewrite <-}\\
+\item {\tt rewrite <- \term}\tacindex{rewrite <-}
+
   Uses the equality \term$_1${\tt=}\term$_2$ from right to left
 
-\item {\tt rewrite {\term} in \textit{clause}}
-  \tacindex{rewrite \dots\ in}\\
+\item {\tt rewrite {\term} in \nterm{clause}}
+  \tacindex{rewrite \dots\ in}
+
   Analogous to {\tt rewrite {\term}} but rewriting is done following
-  \textit{clause} (similarly to \ref{Conversion-tactics}). For
+  \nterm{clause} (similarly to \ref{Conversion-tactics}). For
   instance:
   \begin{itemize}
   \item \texttt{rewrite H in H1} will rewrite \texttt{H} in the hypothesis
@@ -2575,12 +2579,13 @@ This happens if \term$_1$ does not occur in the goal.
   Use {\tac} to completely solve the side-conditions arising from the
   rewrite.
 
-\item {\tt rewrite} $\term_1${\tt ,} {\ldots}{\tt ,} $\term_n$\\
+\item {\tt rewrite \term$_1$ , \mbox{\dots} , \term$_n$}
+
   Is equivalent to the $n$ successive tactics {\tt rewrite $\term_1$}
   up to {\tt rewrite $\term_n$}, each one working on the first subgoal
   generated by the previous one.
   Orientation {\tt ->} or {\tt <-} can be
-  inserted before each term to rewrite. One unique \textit{clause}
+  inserted before each term to rewrite. One unique \nterm{clause}
   can be added at the end after the keyword {\tt in}; it will
   then affect all rewrite operations.
 
@@ -2631,25 +2636,39 @@ n}| assumption || symmetry; try assumption]}.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt replace {\term$_1$} with {\term$_2$} by \tac}\\ This acts
-  as {\tt replace {\term$_1$} with {\term$_2$}} but applies {\tt \tac}
+
+\item {\tt replace \term$_1$ with \term$_2$ by \tac}
+
+  This acts as {\tt replace \term$_1$ with \term$_2$} but applies {\tt \tac}
   to solve the generated subgoal {\tt \term$_2$=\term$_1$}.
-\item {\tt replace {\term}}\\ Replace {\term} with {\term'} using the
+
+\item {\tt replace {\term}}
+
+  Replaces {\term} with {\term'} using the
   first assumption whose type has the form {\tt \term=\term'} or {\tt
-    \term'=\term}
-\item {\tt replace -> {\term}}\\ Replace {\term} with {\term'} using the
+    \term'=\term}.
+
+\item {\tt replace -> {\term}}
+
+  Replaces {\term} with {\term'} using the
   first assumption whose type has the form {\tt \term=\term'}
-\item {\tt replace <- {\term}}\\ Replace {\term} with {\term'} using the
+
+\item {\tt replace <- {\term}}
+
+  Replaces {\term} with {\term'} using the
   first assumption whose type has the form {\tt \term'=\term}
-\item {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} }\\
-    {\tt replace {\term$_1$} with {\term$_2$} \textit{clause} by \tac }\\
-    {\tt replace {\term} \textit{clause}}\\
-    {\tt replace -> {\term} \textit{clause}}\\
-    {\tt replace <- {\term} \textit{clause}}\\
-    Act as before but the replacements take place in
-    \textit{clause}~(see Section~\ref{Conversion-tactics}) and not only
-    in the conclusion of the goal.\\
-    The  \textit{clause} argument must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
+
+\item {\tt replace {\term$_1$} with {\term$_2$} in \nterm{clause} }\\
+    {\tt replace {\term$_1$} with {\term$_2$} in \nterm{clause} by \tac }\\
+    {\tt replace {\term} in \nterm{clause}}\\
+    {\tt replace -> {\term} in \nterm{clause}}\\
+    {\tt replace <- {\term} in \nterm{clause}}
+
+    Acts as before but the replacements take place in
+    \nterm{clause}~(see Section~\ref{Conversion-tactics}) and not only
+    in the conclusion of the goal.
+    The \nterm{clause} argument must not contain any \texttt{type of} nor \texttt{value of}.
+
 \end{Variants}
 
 \subsection{\tt reflexivity}
@@ -2668,10 +2687,12 @@ It is equivalent to {\tt apply refl\_equal}.
 \subsection{\tt symmetry}
 \tacindex{symmetry}
 \tacindex{symmetry in}
+
 This tactic applies to a goal which has the form {\tt t=u} and changes it
 into {\tt u=t}.
 
-\variant {\tt symmetry in {\ident}}\\
+\variant {\tt symmetry in {\ident}}
+
 If the statement of the hypothesis {\ident} has the form {\tt t=u},
 the tactic changes it to {\tt u=t}.
 
@@ -2695,9 +2716,11 @@ When several hypotheses have the form {\tt \ident=t} or {\tt
   t=\ident}, the first one is used.
 
 \begin{Variants}
-  \item {\tt subst \ident$_1$ \dots \ident$_n$} \\
+  \item {\tt subst \ident$_1$ \dots \ident$_n$}
+
     Is equivalent to {\tt subst \ident$_1$; \dots; subst \ident$_n$}.
-  \item {\tt subst} \\
+  \item {\tt subst}
+
     Applies {\tt subst} repeatedly to all identifiers from the context
     for which an equality exists.
 \end{Variants}
@@ -2726,11 +2749,13 @@ accepted as regular setoids for {\tt rewrite} and {\tt
 \tacindex{stepr}
 \comindex{Declare Right Step}
 \begin{Variants}
-\item{\tt stepl {\term} by {\tac}}\\
+\item{\tt stepl {\term} by {\tac}}
+
 This applies {\tt stepl {\term}} then applies {\tac} to the second goal.
 
 \item{\tt stepr {\term}}\\
-     {\tt stepr {\term} by {\tac}}\\
+     {\tt stepr {\term} by {\tac}}
+
 This behaves as {\tt stepl} but on the right-hand-side of the binary relation.
 Lemmas are expected to be of the form
 ``{\tt forall} $x$ $y$
@@ -3145,7 +3170,7 @@ x}$)$) $t$}.  This command can be used, for instance, when the tactic
   Starting from a goal $\phi(t_1 \dots\ t_m)$, the tactic
    {\tt pattern $t_1$, \dots,\ $t_m$} generates the equivalent goal {\tt
    (fun (x$_1$:$A_1$) \dots\ (x$_m$:$A_m$) => $\phi(${\tt x$_1$\dots\
-   x$_m$}$)$) $t_1$ \dots\ $t_m$}.\\ If $t_i$ occurs in one of the
+   x$_m$}$)$) $t_1$ \dots\ $t_m$}. If $t_i$ occurs in one of the
    generated types $A_j$ these occurrences will also be considered and
    possibly abstracted.
 
@@ -3277,9 +3302,9 @@ This tactic unfolds constants that were declared through a {\tt Hint
   Unfold} in the given databases.
 
 \begin{Variants}
-\item {\tt autounfold with \ident$_1$ \dots\ \ident$_n$ in \textit{clause}}
+\item {\tt autounfold with \ident$_1$ \dots\ \ident$_n$ in \nterm{clause}}
 
-  Perform the unfolding in the given clause.
+  Performs the unfolding in the given clause.
 
 \item {\tt autounfold with *}
 
@@ -3311,21 +3336,24 @@ command.
 \Warning{} This tactic may loop if you build non terminating rewriting systems.
 
 \begin{Variant}
-\item {\tt autorewrite with \ident$_1$ \dots \ident$_n$ using \tac}\\
-Performs, in the same way, all the rewritings of the bases {\tt \ident$_1$ $...$
-\ident$_n$} applying {\tt \tac} to the main subgoal after each rewriting step.
+\item {\tt autorewrite with \ident$_1$ \mbox{\dots} \ident$_n$ using \tac}
 
-\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid}}
+Performs, in the same way, all the rewritings of the bases {\tt \ident$_1$
+\mbox{\dots} \ident$_n$} applying {\tt \tac} to the main subgoal after each
+rewriting step.
+
+\item {\tt autorewrite with \ident$_1$ \mbox{\dots} \ident$_n$ in \qualid}
 
   Performs all the rewritings in hypothesis {\qualid}.
-\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in {\qualid} using \tac}
+\item {\tt autorewrite with \ident$_1$ \mbox{\dots} \ident$_n$ in {\qualid} using \tac}
 
   Performs all  the rewritings  in hypothesis {\qualid}  applying {\tt
     \tac} to the main subgoal after each rewriting step.
 
-\item \texttt{autorewrite with {\ident$_1$} \dots \ident$_n$ in \textit{clause}}
-  Performs all  the rewritings  in the clause \textit{clause}. \\
-  The  \textit{clause} argument must  not contain  any \texttt{type  of} nor  \texttt{value  of}.
+\item {\tt autorewrite with \ident$_1$ \mbox{\dots} \ident$_n$ in \nterm{clause}}
+
+  Performs all the rewriting  in the clause \nterm{clause}.
+  The \nterm{clause} argument must not contain any \texttt{type of} nor \texttt{value of}.
 
 \end{Variant}
 
@@ -3381,35 +3409,34 @@ inserted, making this implementation observationally different from the
 legacy one.
 
 The general
-command to add a hint to some database \ident$_1$, \dots, \ident$_n$ is
+command to add a hint to some databases \ident$_1$, \dots, \ident$_n$ is
 \begin{tabbing}
-  \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ {\ldots} \ident$_n$
+  {\tt Hint {\hintdef} :~\ident$_1$ \mbox{\dots} \ident$_n$}
 \end{tabbing}
 
 \begin{Variants}
-\item \texttt{Hint} \textsl{hint\_definition}
+\item {\tt Hint \hintdef}
 
   No database name is given: the hint is registered in the {\tt core}
     database.
 
-\item\texttt{Local Hint} \textsl{hint\_definition} \texttt{:}
-  \ident$_1$ \ldots\ \ident$_n$
+\item {\tt Local Hint {\hintdef} :~\ident$_1$ \mbox{\dots} \ident$_n$}
 
   This is used to declare hints that must not be exported to the other
   modules that require and import the current module. Inside a
   section, the option {\tt Local} is useless since hints do not
   survive anyway to the closure of sections.
 
-\item\texttt{Local Hint} \textsl{hint\_definition}
+\item {\tt Local Hint \hintdef}
 
   Idem for the {\tt core} database.
 
 \end{Variants}
 
-The \textsl{hint\_definition} is one of the following expressions:
+The \hintdef is one of the following expressions:
 
 \begin{itemize}
-\item \texttt{Resolve} {\term}
+\item {\tt Resolve \term}
   \comindex{Hint Resolve}
 
   This command adds {\tt apply {\term}} to the hint list
@@ -3444,7 +3471,7 @@ The \textsl{hint\_definition} is one of the following expressions:
 
   \begin{Variants}
 
-  \item \texttt{Resolve} {\term$_1$} \dots {\term$_m$}
+  \item {\tt Resolve \term$_1$ \mbox{\dots} \term$_m$}
 
     Adds each \texttt{Resolve} {\term$_i$}.
 
@@ -3476,7 +3503,7 @@ The \textsl{hint\_definition} is one of the following expressions:
 
   \begin{Variants}
 
-    \item \texttt{Immediate} {\term$_1$} \dots {\term$_m$}
+    \item {\tt Immediate \term$_1$ \mbox{\dots} \term$_m$}
 
       Adds each \texttt{Immediate} {\term$_i$}.
 
@@ -3500,7 +3527,7 @@ The \textsl{hint\_definition} is one of the following expressions:
 
   \begin{Variants}
 
-    \item \texttt{Constructors} {\ident$_1$} \dots {\ident$_m$}
+    \item {\tt Constructors \ident$_1$ \mbox{\dots} \ident$_m$}
 
       Adds each \texttt{Constructors} {\ident$_i$}.
 
@@ -3515,7 +3542,7 @@ The \textsl{hint\_definition} is one of the following expressions:
 
   \begin{Variants}
 
-    \item \texttt{Unfold} {\ident$_1$} \dots {\ident$_m$}
+    \item {\tt Unfold \ident$_1$ \mbox{\dots} \ident$_m$}
 
       Adds each \texttt{Unfold} {\ident$_i$}.
 
@@ -3534,7 +3561,7 @@ The \textsl{hint\_definition} is one of the following expressions:
 
   \begin{Variants}
 
-    \item \texttt{Transparent}, \texttt{Opaque} {\ident$_1$} \dots {\ident$_m$}
+    \item \texttt{Transparent}, \texttt{Opaque} {\ident$_1$} \mbox{\dots} {\ident$_m$}
 
       Declares each {\ident$_i$} as a transparent or opaque constant.
 
@@ -3583,20 +3610,19 @@ pattern-matching on hypotheses using \texttt{match goal with} inside
 the tactic.
 
 \begin{Variants}
-\item \texttt{Hint} \textsl{hint\_definition}
+\item {\tt Hint \hintdef}
 
   No database name is given: the hint is registered in the {\tt core}
     database.
 
-\item\texttt{Hint Local} \textsl{hint\_definition} \texttt{:}
-   \ident$_1$ \ldots\ \ident$_n$
+\item {\tt Hint Local {\hintdef} : \ident$_1$ \mbox{\dots} \ident$_n$}
 
   This is used to declare hints that must not be exported to the other
   modules that require and import the current module. Inside a
   section, the option {\tt Local} is useless since hints do not
   survive anyway to the closure of sections.
 
-\item\texttt{Hint Local} \textsl{hint\_definition}
+\item {\tt Hint Local \hintdef}
 
   Idem for the {\tt core} database.
 
@@ -3689,7 +3715,7 @@ every moment.
 
 \begin{Variants}
 
-\item {\tt  Print Hint {\ident} }
+\item {\tt Print Hint \ident}
 
  This command displays only tactics associated with \ident\ in the
  hints list. This is independent of the goal being edited, so this
@@ -3699,7 +3725,7 @@ every moment.
 
   This command displays all declared hints.
 
-\item {\tt  Print HintDb {\ident} }
+\item {\tt Print HintDb \ident}
 \label{PrintHintDb}
 \comindex{Print HintDb}
 
@@ -3707,11 +3733,11 @@ every moment.
 
 \end{Variants}
 
-\subsection{\tt Hint Rewrite \term$_1$ \mbox{\dots} \term$_n$ : \ident}
+\subsection{\tt Hint Rewrite \term$_1$ \mbox{\dots} \term$_n$ :~\ident}
 \label{HintRewrite}
 \comindex{Hint Rewrite}
 
-This vernacular command adds the terms {\tt \term$_1$ \dots \term$_n$}
+This vernacular command adds the terms {\tt \term$_1$ \mbox{\dots} \term$_n$}
 (their types must be equalities) in the rewriting base {\tt \ident}
 with the default orientation (left to right). Notice that the
 rewriting bases are distinct from the {\tt auto} hint bases and that
@@ -3723,16 +3749,19 @@ section are lost. Conversely, when loading a module, all \texttt{Hint Rewrite}
 declarations at the global level of that module are loaded.
 
 \begin{Variants}
-\item {\tt Hint Rewrite -> \term$_1$ \dots \term$_n$ : \ident}\\
+\item {\tt Hint Rewrite -> \term$_1$ \mbox{\dots} \term$_n$ :~\ident}
+
 This is strictly equivalent to the command above (we only make explicit the
 orientation which otherwise defaults to {\tt ->}).
 
-\item {\tt Hint Rewrite <- \term$_1$ \dots \term$_n$ : \ident}\\
-Adds the rewriting rules {\tt \term$_1$ \dots \term$_n$} with a right-to-left
+\item {\tt Hint Rewrite <- \term$_1$ \mbox{\dots} \term$_n$ :~\ident}
+
+Adds the rewriting rules {\tt \term$_1$ \mbox{\dots} \term$_n$} with a right-to-left
 orientation in the base {\tt \ident}.
 
-\item {\tt Hint Rewrite \term$_1$ \dots \term$_n$ using {\tac} : {\ident}}\\
-When the rewriting rules {\tt \term$_1$ \dots \term$_n$} in {\tt \ident} will
+\item {\tt Hint Rewrite \term$_1$ \mbox{\dots} \term$_n$ using {\tac} :~\ident}
+
+When the rewriting rules {\tt \term$_1$ \mbox{\dots} \term$_n$} in {\tt \ident} will
 be used, the tactic {\tt \tac} will be applied to the generated subgoals, the
 main subgoal excluded.
 
@@ -3760,8 +3789,9 @@ e.g. \texttt{Require Import A.}).
 
 \subsection{Setting implicit automation tactics}
 
-\subsubsection[\tt Proof with {\tac}.]{\tt Proof with {\tac}.\label{ProofWith}
-\comindex{Proof with}}
+\subsubsection{\tt Proof with {\tac}}
+\label{ProofWith}
+\comindex{Proof with}
 
   This command may be used to start a proof. It defines a default
   tactic to be used each time a tactic command {\tac$_1$} is ended by
@@ -3771,16 +3801,17 @@ e.g. \texttt{Require Import A.}).
 \SeeAlso {\tt Proof.} in Section~\ref{BeginProof}.
 
 \begin{Variants}
-\item {\tt Proof with {\tac} using {\ident$_1$ \dots {\ident$_n$}}}
+\item {\tt Proof with {\tac} using \ident$_1$ \mbox{\dots} \ident$_n$}
   Combines in a single line {\tt Proof with} and {\tt Proof using},
   see~\ref{ProofUsing}
-\item {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}}
+\item {\tt Proof using \ident$_1$ \mbox{\dots} \ident$_n$ with {\tac}}
   Combines in a single line {\tt Proof with} and {\tt Proof using},
   see~\ref{ProofUsing}
 
 \end{Variants}
 
-\subsubsection[\tt Declare Implicit Tactic {\tac}.]{\tt Declare Implicit Tactic {\tac}.\comindex{Declare Implicit Tactic}}
+\subsubsection{\tt Declare Implicit Tactic {\tac}}
+\comindex{Declare Implicit Tactic}
 
 This command declares a tactic to be used to solve implicit arguments
 that {\Coq} does not know how to solve by unification. It is used
@@ -3885,7 +3916,8 @@ slightly changed to get clearer semantics. This may lead to some
 incompatibilities.
 
 \begin{Variants}
-\item {\tt intuition}\\
+\item {\tt intuition}
+
   Is equivalent to {\tt intuition auto with *}.
 \end{Variants}
 
@@ -3984,26 +4016,33 @@ congruence.
 \end{coq_example}
 
 \begin{Variants}
- \item {\tt congruence {\sl n}}\\
+ \item {\tt congruence {\sl n}}
+
   Tries to add at most {\tt \sl n} instances of hypotheses stating quantified equalities to the problem in order to solve it. A bigger value of {\tt \sl n} does not make success slower, only failure. You might consider adding some lemmas as hypotheses using {\tt assert} in order for congruence to use them.
 
 \end{Variants}
 
 \begin{Variants}
-\item {\tt congruence with \term$_1$ \dots\ \term$_n$}\\
+\item {\tt congruence with \term$_1$ \dots\ \term$_n$}
+
   Adds {\tt \term$_1$ \dots\ \term$_n$} to the pool of terms used by
   {\tt congruence}. This helps in case you have partially applied
   constructors in your goal.
 \end{Variants}
 
 \begin{ErrMsgs}
-  \item \errindex{I don't know how to handle dependent equality} \\
+  \item \errindex{I don't know how to handle dependent equality}
+
     The decision procedure managed to find a proof of the goal or of
     a discriminable equality but this proof couldn't be built in {\Coq}
     because of dependently-typed functions.
-  \item \errindex{I couldn't solve goal} \\
+
+  \item \errindex{I couldn't solve goal}
+
     The decision procedure didn't find any way to solve the goal.
-  \item \errindex{Goal is solvable by congruence but some arguments are missing. Try "congruence with \dots", replacing metavariables by arbitrary terms.} \\
+
+  \item \errindex{Goal is solvable by congruence but some arguments are missing. Try "congruence with \dots", replacing metavariables by arbitrary terms.}
+
     The decision procedure could solve the goal with the provision
     that additional arguments are supplied for some partially applied
     constructors. Any term of an appropriate type will allow the
@@ -4203,7 +4242,8 @@ and inversion tactics.
 
 \begin{Variants}
 \item{\tt dependent rewrite <- {\ident}}
-\tacindex{dependent rewrite <-} \\
+\tacindex{dependent rewrite <-}
+
 Analogous to {\tt dependent rewrite ->} but uses the equality from
 right to left.
 \end{Variants}
@@ -4257,12 +4297,14 @@ convertibility. In other words, it does inversion of the function
 datatype: see~\ref{quote-examples} for the full details.
 
 \begin{ErrMsgs}
-\item \errindex{quote: not a simple fixpoint}\\
+\item \errindex{quote: not a simple fixpoint}
+
   Happens when \texttt{quote} is not able to perform inversion properly.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item \texttt{quote {\ident} [ \ident$_1$ \dots \ident$_n$ ]}\\
+\item \texttt{quote {\ident} [ \ident$_1$ \dots \ident$_n$ ]}
+
   All terms that are built only with \ident$_1$ \dots \ident$_n$ will be
   considered by \texttt{quote} as constants rather than variables.
 \end{Variants}