Improving rendering of ldots in doc (partially done, there are too

much of them). Improving doc of conversion clauses.

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

8 files changed, 214 insertions, 209 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 1bae52617..97a9b326b 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -128,6 +128,7 @@
 \newcommand{\caseitem}{\nterm{match\_item}}
 \newcommand{\eqn}{\nterm{equation}}
 \newcommand{\ifitem}{\nterm{dep\_ret\_type}}
+\newcommand{\hyplocation}{\nterm{hyp\_location}}
 \newcommand{\convclause}{\nterm{conversion\_clause}}
 \newcommand{\occclause}{\nterm{occurrence\_clause}}
 \newcommand{\occgoalset}{\nterm{goal\_occurrences}}
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex
index 56b989b2e..888aba175 100644
--- a/doc/refman/Cases.tex
+++ b/doc/refman/Cases.tex
@@ -33,7 +33,7 @@ anything. It may occur an arbitrary number of times in a
 pattern. Alias patterns written \texttt{(}{\sl pattern} \texttt{as}
 {\sl identifier}\texttt{)} are also accepted. This pattern matches the
 same values as {\sl pattern} does and {\sl identifier} is bound to the
-matched value.  
+matched value.
 A pattern of the form {\pattern}{\tt |}{\pattern} is called
 disjunctive. A list of patterns separated with commas is also
 considered as a pattern and is called {\em multiple pattern}. However
@@ -53,7 +53,7 @@ The extended \texttt{match} still accepts an optional {\em elimination
 predicate} given after the keyword \texttt{return}.  Given a pattern
 matching expression, if all the right-hand-sides of \texttt{=>} ({\em
 rhs} in short) have the same type, then this type can be sometimes
-synthesized, and so we can omit the \texttt{return} part. Otherwise 
+synthesized, and so we can omit the \texttt{return} part. Otherwise
 the predicate after \texttt{return} has to be provided, like for the basic
 \texttt{match}.
 
@@ -175,9 +175,9 @@ Fixpoint lef (n m:nat) {struct m} : bool :=
 \end{coq_example}
 
 Here the last pattern superposes with the first two. Because
-of the priority rule, the last pattern 
+of the priority rule, the last pattern
 will be used only for values that do not match neither the  first nor
-the second one.  
+the second one.
 
 Terms with useless patterns are not accepted by the
 system. Here is an example:
@@ -303,7 +303,7 @@ Check
 
 \asection{Matching objects of dependent types}
 The previous examples illustrate pattern matching on objects of
-non-dependent types, but we can also 
+non-dependent types, but we can also
 use the expansion strategy to destructure objects of dependent type.
 Consider the type \texttt{listn} of lists of a certain length:
 \label{listn}
@@ -321,7 +321,7 @@ We can define the function \texttt{length} over \texttt{listn} by:
 Definition length (n:nat) (l:listn n) := n.
 \end{coq_example}
 
-Just for illustrating pattern matching, 
+Just for illustrating pattern matching,
 we can define it by case analysis:
 
 \begin{coq_example}
@@ -340,7 +340,7 @@ same notions of usual pattern matching.
 % Constraining of dependencies is not longer valid in V7
 %
 \iffalse
-Now suppose we split the second pattern  of \texttt{length} into two 
+Now suppose we split the second pattern  of \texttt{length} into two
 cases so to give an
 alternative definition using nested patterns:
 \begin{coq_example}
@@ -371,11 +371,11 @@ In fact, they are equivalent
 because the pattern \texttt{niln} implies that \texttt{n} can only match
 the value $0$ and analogously the pattern \texttt{consn} determines that \texttt{n} can
 only match  values of the form  $(S~v)$ where $v$ is the value matched by
-\texttt{m}. 
+\texttt{m}.
 
 The converse is also true. If
 we destructure the  length  value with the pattern \texttt{O} then the list
-value should be $niln$. 
+value should be $niln$.
 Thus, the following term \texttt{length3} corresponds to the function
 \texttt{length} but this time defined by case analysis on the dependencies instead of on the list:
 
@@ -392,7 +392,7 @@ When we have nested patterns of dependent types, the semantics of
 pattern matching becomes a little more difficult because
 the set of values that are matched by a sub-pattern may be conditioned by the
 values matched by another sub-pattern. Dependent nested patterns are
-somehow constrained patterns. 
+somehow constrained patterns.
 In the examples, the expansion of
 \texttt{length1} and \texttt{length2} yields exactly the same term
  but the
@@ -415,7 +415,7 @@ The examples  given so far do not need an explicit elimination predicate
  because all the rhs have the same type and the
 strategy succeeds to synthesize it.
 Unfortunately when dealing with dependent patterns it often happens
-that we need to write cases where the type of the rhs are 
+that we need to write cases where the type of the rhs are
 different  instances of the elimination  predicate.
 The function  \texttt{concat} for \texttt{listn}
 is an example where the branches have different type
@@ -430,14 +430,14 @@ Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} :
   end.
 \end{coq_example}
 The elimination predicate is {\tt fun (n:nat) (l:listn n) => listn~(n+m)}.
-In general if $m$ has type $(I~q_1\ldots q_r~t_1\ldots t_s)$ where 
-$q_1\ldots q_r$ are parameters, the elimination predicate should be of
+In general if $m$ has type {\tt (}$I$ $q_1$ {\ldots} $q_r$ $t_1$ {\ldots} $t_s${\tt )} where
+$q_1$, {\ldots}, $q_r$ are parameters, the elimination predicate should be of
 the form~:
-{\tt fun $y_1$\ldots $y_s$ $x$:($I$~$q_1$\ldots $q_r$~$y_1$\ldots
-  $y_s$) => Q}.
+{\tt fun} $y_1$ {\ldots} $y_s$ $x${\tt :}($I$~$q_1$ {\ldots} $q_r$ $y_1$ {\ldots}
+  $y_s${\tt ) =>} $Q$.
 
 In the concrete syntax, it should be written~:
-\[ \kw{match}~m~\kw{as}~x~\kw{in}~(I~\_\ldots \_~y_1\ldots y_s)~\kw{return}~Q~\kw{with}~\ldots~\kw{end}\]
+\[ \kw{match}~m~\kw{as}~x~\kw{in}~(I~\_~\mbox{\ldots}~\_~y_1~\mbox{\ldots}~y_s)~\kw{return}~Q~\kw{with}~\mbox{\ldots}~\kw{end}\]
 
 The variables which appear in the \kw{in} and \kw{as} clause are new
 and bounded in the property $Q$ in the \kw{return} clause. The
@@ -533,12 +533,12 @@ and {\tt tail n v} will be subterm of {\tt v}.
 
 \asection{Using pattern matching to write proofs}
 In all the previous examples the elimination predicate does not depend
-on the object(s) matched. But it may depend and the typical case 
+on the object(s) matched. But it may depend and the typical case
 is when we write a proof by induction or a function that yields an
 object of dependent type. An example of proof using \texttt{match} in
 given in Section~\ref{refine-example}.
 
-For example, we can write 
+For example, we can write
 the function \texttt{buildlist} that given a natural number
 $n$ builds a list of length $n$ containing zeros as follows:
 
@@ -550,7 +550,7 @@ Fixpoint buildlist (n:nat) : listn n :=
   end.
 \end{coq_example}
 
-We can also use multiple patterns. 
+We can also use multiple patterns.
 Consider the following definition of the predicate less-equal
 \texttt{Le}:
 
@@ -576,14 +576,14 @@ Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n :=
   end.
 \end{coq_example}
 In the example of \texttt{dec},
-the first \texttt{match} is dependent while 
+the first \texttt{match} is dependent while
 the second is not.
 
 % In general, consider the terms $e_1\ldots e_n$,
 % where  the type of $e_i$ is an instance of a family type
 % $\lb (\vec{d_i}:\vec{D_i}) \mto T_i$  ($1\leq i
 % \leq n$). Then, in expression \texttt{match}  $e_1,\ldots,
-% e_n$ \texttt{of} \ldots \texttt{end}, the 
+% e_n$ \texttt{of} \ldots \texttt{end}, the
 % elimination predicate ${\cal P}$ should be of the form:
 % $[\vec{d_1}:\vec{D_1}][x_1:T_1]\ldots [\vec{d_n}:\vec{D_n}][x_n:T_n]Q.$
 
@@ -664,9 +664,9 @@ Check (fun x => match x with
 
 \asection{When does the expansion strategy fail ?}\label{limitations}
 The strategy works very like in ML languages when treating
-patterns of non-dependent type.  
-But there are new cases of failure that are due to the presence of 
-dependencies. 
+patterns of non-dependent type.
+But there are new cases of failure that are due to the presence of
+dependencies.
 
 The error messages of the current implementation may be sometimes
 confusing.  When the tactic fails because patterns are somehow
@@ -676,11 +676,11 @@ well typed when the whole expression is not. In this situation the
 message makes reference to the expanded expression.  We encourage
 users, when they have patterns with the same outer constructor in
 different equations, to name the variable patterns in the same
-positions with the same name.  
-E.g. to write {\small\texttt{(cons n O x) => e1}} 
+positions with the same name.
+E.g. to write {\small\texttt{(cons n O x) => e1}}
 and {\small\texttt{(cons n \_ x) => e2}} instead of
-{\small\texttt{(cons n O x) => e1}} and 
-{\small\texttt{(cons n' \_ x') => e2}}. 
+{\small\texttt{(cons n O x) => e1}} and
+{\small\texttt{(cons n' \_ x') => e2}}.
 This helps to maintain certain name correspondence between the
 generated expression and the original.
 
@@ -689,10 +689,10 @@ Here is a summary of the error messages corresponding to each situation:
 \begin{ErrMsgs}
 \item \sverb{The constructor } {\sl
     ident} \sverb{ expects } {\sl num} \sverb{ arguments}
-  
+
  \sverb{The variable } {\sl ident} \sverb{ is bound several times
     in pattern } {\sl term}
-  
+
  \sverb{Found a constructor of inductive type } {\term}
  \sverb{ while a constructor of } {\term} \sverb{ is expected}
 
@@ -718,7 +718,7 @@ The elimination predicate provided to \texttt{match} has not the
 % , or the synthesis of
 %   implicit arguments fails (for example to find the elimination
 %   predicate or to resolve implicit arguments in the rhs).
- 
+
 %   There are {\em nested patterns of dependent type}, the elimination
 %   predicate corresponds to non-dependent case and has the form
 %   $[x_1:T_1]...[x_n:T_n]T$ and {\bf some} $x_i$ occurs {\bf free} in
@@ -726,15 +726,15 @@ The elimination predicate provided to \texttt{match} has not the
 %   predicate during some step of compilation.  In this situation we
 %   recommend the user to rewrite the nested dependent patterns into
 %   several \texttt{match} with {\em simple patterns}.
-  
+
 \item {\tt Unable to infer a match predicate\\
     Either there is a type incompatiblity or the problem involves\\
     dependencies}
- 
+
   There is a type mismatch between the different branches.
   The user should provide an elimination predicate.
 
-% Obsolete ?  
+% Obsolete ?
 % \item because of nested patterns, it may happen that even though all
 %   the rhs have the same type, the strategy needs dependent elimination
 %   and so an elimination predicate must be provided. The system warns
@@ -768,7 +768,7 @@ The elimination predicate provided to \texttt{match} has not the
 
 % \begin{coq_example}
 %   Fixpoint last [n:nat; l:(listn n)] : nat :=
-%    match l of 
+%    match l of
 %      (consn _ a niln) => a
 %    | (consn m _ x) => (last m x) | niln => O
 %    end.
@@ -813,7 +813,7 @@ The elimination predicate provided to \texttt{match} has not the
 \end{ErrMsgs}
 
 
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "Reference-Manual"
-%%% End: 
+%%% End:
diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex
index 3b6c949ba..dcff7fb8d 100644
--- a/doc/refman/Coercion.tex
+++ b/doc/refman/Coercion.tex
@@ -175,7 +175,7 @@ valid coercion paths are ignored; they are signaled by a warning.
 \begin{enumerate}
 \item \begin{tabbing}
 {\tt Ambiguous paths: }\= $[f_1^1;..;f_{n_1}^1] : C_1\mbox{\tt >->}D_1$\\
-                       \> ... \\
+                       \> {\ldots} \\
                        \>$[f_1^m;..;f_{n_m}^m] : C_m\mbox{\tt >->}D_m$
       \end{tabbing}
 \end{enumerate}
diff --git a/doc/refman/Helm.tex b/doc/refman/Helm.tex
index ed94dfc59..cbb097267 100644
--- a/doc/refman/Helm.tex
+++ b/doc/refman/Helm.tex
@@ -52,9 +52,9 @@ since the XML format is very verbose.
 For each {\Coq} logical object, several independent files associated
 to this object are created.  The structure of the long name of the
 object is reflected in the directory structure of the file system.
-E.g. an object of long name {\tt
-{\ident$_1$}.{\ldots}.{\ident$_n$}.{\ident}} is exported to files in the
-subdirectory {{\ident$_1$}/{\ldots}/{\ident$_n$}} of the directory 
+E.g. an object of long name 
+{\ident$_1$}{\tt .}{\ldots}{\tt .}{\ident$_n$}{\tt .}{\ident} is exported to files in the
+subdirectory {\ident$_1$}{\tt /}{\ldots}{\tt /}{\ident$_n$} of the directory 
 bound to the environment variable {\tt COQ\_XML\_LIBRARY\_ROOT}.
 
 \subsection{What is exported?}
@@ -74,29 +74,29 @@ Comments are pre-processed with {\sf coqdoc} (see section
 and {\tt *)} to be exported.
 
 For each inductive definition of name
-{\ident$_1$}.{\ldots}.{\ident$_n$}.{\ident}, a file named {\tt
-{\ident}.ind.xml} is created in the subdirectory {\tt
-{\ident$_1$}/{\ldots}/{\ident$_n$}} of the xml library root
+{\ident$_1$}{\tt .}{\ldots}{\tt .}{\ident$_n$}.{\ident}, a file named
+{\ident}{\tt .ind.xml} is created in the subdirectory
+{\ident$_1$}{\tt /}{\ldots}{\tt /}{\ident$_n$} of the xml library root
 directory. It contains the arities and constructors of the type. For mutual inductive definitions, the file is named after the
 name of the first inductive type of the block.
 
-For each global definition of base name {\tt
-{\ident$_1$}.{\ldots}.{\ident$_n$}.{\ident}}, files named
+For each global definition of base name
+{\ident$_1$}{\tt .}{\ldots}{\tt .}{\ident$_n$}.{\ident}, files named
 {\tt {\ident}.con.body.xml} and {\tt {\ident}.con.xml} are created in the
-subdirectory {\tt {\ident$_1$}/{\ldots}/{\ident$_n$}}. They
+subdirectory {\ident$_1$}{\tt /}{\ldots}{\tt /}{\ident$_n$}. They
 respectively contain the body and the type of the definition.
 
-For each global assumption of base name {\tt
-{\ident$_1$}.{\ident$_2$}.{\ldots}.{\ident$_n$}.{\ident}}, a file
-named {\tt {\ident}.con.xml} is created in the subdirectory {\tt
-{\ident$_1$}/{\ldots}/{\ident$_n$}}.  It contains the type of the
+For each global assumption of base name {\ident$_1$}{\tt .}{\ident$_2$}{\tt .}
+{\ldots}{\tt .}{\ident$_n$}{\tt .}{\ident}, a file
+named {\ident}{\tt .con.xml} is created in the subdirectory
+{\ident$_1$}{\tt /}{\ldots}{\tt /}{\ident$_n$}.  It contains the type of the
 global assumption.
 
 For each local assumption or definition of base name {\ident} located
-in sections {\ident$'_1$}, {\ldots}, {\ident$'_p$} of the module {\tt
-{\ident$_1$}.{\ident$_2$}.{\ldots}.{\ident$_n$}.{\ident}}, a file
-named {\tt {\ident}.var.xml} is created in the subdirectory {\tt
-{\ident$_1$}/{\ldots}/{\ident$_n$}/{\ident$'_1$}/\ldots/{\ident$'_p$}}.
+in sections {\ident$'_1$}, {\ldots}, {\ident$'_p$} of the module
+{\ident$_1$}.{\ident$_2$}{\tt .}{\ldots}{\tt .}{\ident$_n$}.{\ident}, a file
+named {\tt {\ident}.var.xml} is created in the subdirectory
+{\ident$_1$}{\tt /}{\ldots}{\tt /}{\ident$_n$}{\tt /}{\ident$'_1$}{\tt /}\ldots{\tt /}{\ident$'_p$}.
 It contains its type and, if a definition, its body.
 
 In order to do proof-rendering (for example in natural language), some
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 8af3a95d4..588016b0a 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -866,22 +866,22 @@ environment, provided that {\term} is well-typed.
 \end{ErrMsgs}
 
 \begin{Variants}
-\item {\tt Definition {\ident} {\tt :}{\term$_1$} := {\term$_2$}.}\\
+\item {\tt Definition} {\ident} {\tt :} {\term$_1$} {\tt :=} {\term$_2$}{\tt .}\\
   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$}
-       {\tt :}\term$_1$ {\tt :=} {\term$_2$}.}\\
+\item {\tt Definition} {\ident} {\binder$_1$} {\ldots} {\binder$_n$}
+       {\tt :} \term$_1$ {\tt :=} {\term$_2$}{\tt .}\\
   This is equivalent to \\
-   {\tt Definition\,{\ident}\,{\tt :\,forall}\,%
-       {\binder$_1$} {\ldots} {\binder$_n$}{\tt ,}\,\term$_1$\,{\tt :=}}\,%
+   {\tt Definition} {\ident} {\tt : forall}%
+       {\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 :}\term$_1$ {\tt :=} {\term$_2$}.}\\
+{\tt Example} {\ident} {\tt :} {\term$_1$} {\tt :=} {\term$_2$}{\tt .}\\
+{\tt Example} {\ident} {\binder$_1$} {\ldots} {\binder$_n$}
+       {\tt :} {\term$_1$} {\tt :=} {\term$_2$}{\tt .}\\
 \comindex{Example}
 These are synonyms of the {\tt Definition} forms.
 \end{Variants}
@@ -932,16 +932,14 @@ mutually inductive types. We explain also co-inductive types.
 The definition of a simple inductive type has the following form:
 
 \medskip
-{\tt 
 \begin{tabular}{l}
-Inductive {\ident} : {\sort} :=  \\
+{\tt Inductive} {\ident} {\tt :} {\sort} {\tt :=} \\
 \begin{tabular}{clcl}
-   & {\ident$_1$}  &:& {\type$_1$} \\
- | & {\ldots} && \\
- | & {\ident$_n$} &:& {\type$_n$}
+         & {\ident$_1$} & {\tt :} & {\type$_1$} \\
+ {\tt |} & {\ldots} && \\
+ {\tt |} & {\ident$_n$} & {\tt :} & {\type$_n$} \\
 \end{tabular}
 \end{tabular}
-}
 \medskip
 
 The name {\ident} is the name of the inductively defined type and
@@ -1184,24 +1182,22 @@ this reason, the parameters must be strictly the same for each
 inductive types The extended syntax is:
 
 \medskip
-{\tt 
 \begin{tabular}{l}
-Inductive {\ident$_1$} {\params} : {\type$_1$} :=  \\
+{\tt Inductive} {\ident$_1$} {\params} {\tt :} {\type$_1$} {\tt :=}  \\
 \begin{tabular}{clcl}
-   & {\ident$_1^1$}     &:& {\type$_1^1$} \\
- | & {\ldots} && \\
- | & {\ident$_{n_1}^1$} &:& {\type$_{n_1}^1$}
+         & {\ident$_1^1$}    &{\tt :}& {\type$_1^1$} \\
+ {\tt |} & {\ldots} && \\
+ {\tt |} & {\ident$_{n_1}^1$} &{\tt :}& {\type$_{n_1}^1$}
 \end{tabular}  \\
-with\\
+{\tt with}\\
 ~{\ldots} \\
-with {\ident$_m$} {\params} : {\type$_m$} := \\
+{\tt with} {\ident$_m$} {\params} {\tt :} {\type$_m$} {\tt :=} \\
 \begin{tabular}{clcl}
-   & {\ident$_1^m$}     &:& {\type$_1^m$} \\
- | & {\ldots} \\
- | & {\ident$_{n_m}^m$} &:& {\type$_{n_m}^m$}.
+         & {\ident$_1^m$}    &{\tt :}& {\type$_1^m$} \\
+ {\tt |} & {\ldots} \\
+ {\tt |} & {\ident$_{n_m}^m$} &{\tt :}& {\type$_{n_m}^m$}.
 \end{tabular}
 \end{tabular}
-}
 \medskip
 
 \Example
@@ -1433,9 +1429,9 @@ to define functions over mutually defined inductive types or more
 generally any mutually recursive definitions.
 
 \begin{Variants}
-\item {\tt Fixpoint {\ident$_1$} {\params$_1$} :{\type$_1$} := {\term$_1$}\\
-        with {\ldots} \\
-        with {\ident$_m$} {\params$_m$} :{\type$_m$} :=  {\term$_m$}}\\
+\item {\tt Fixpoint} {\ident$_1$} {\params$_1$} {\tt :} {\type$_1$} {\tt :=} {\term$_1$}\\
+        {\tt with} {\ldots} \\
+        {\tt with} {\ident$_m$} {\params$_m$} {\tt :} {\type$_m$} {\tt :=} {\term$_m$}\\
         Allows to define simultaneously {\ident$_1$}, {\ldots},
         {\ident$_m$}.
 \end{Variants}
@@ -1530,10 +1526,10 @@ Eval compute in (tl (from 0)).
 \item{\tt CoFixpoint {\ident$_1$} {\params} :{\type$_1$} :=
   {\term$_1$}}\\ As for most constructions, arguments of co-fixpoints
   expressions can be introduced before the {\tt :=} sign.
-\item{\tt CoFixpoint {\ident$_1$} :{\type$_1$} := {\term$_1$}\\
-     with\\
-        \mbox{}\hspace{0.1cm} $\ldots$  \\
-        with {\ident$_m$}   : {\type$_m$} := {\term$_m$}}\\
+\item{\tt CoFixpoint} {\ident$_1$} {\tt :} {\type$_1$} {\tt :=} {\term$_1$}\\
+     {\tt with}\\
+        \mbox{}\hspace{0.1cm} {\ldots} \\
+        {\tt with} {\ident$_m$} {\tt :} {\type$_m$} {\tt :=} {\term$_m$}\\
 As in the \texttt{Fixpoint} command (see Section~\ref{Fixpoint}), it
 is possible to introduce a block of mutually dependent methods.
 \end{Variants}
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 491e61c84..7b70e4cc6 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -22,7 +22,7 @@ global constant.
 \comindex{About}\\ 
 This displays various informations about the object denoted by {\qualid}:
 its kind (module, constant, assumption, inductive,
-constructor, abbreviation\ldots), long name, type, implicit
+constructor, abbreviation, \ldots), long name, type, implicit
 arguments and argument scopes. It does not print the body of
 definitions or proofs.
 
@@ -135,9 +135,9 @@ displayed in Objective Caml syntax, where global identifiers are still
 displayed as in \Coq\ terms.
 
 \begin{Variants}
-\item \texttt{Recursive Extraction {\qualid$_1$} \ldots{} {\qualid$_n$}.}\\
+\item \texttt{Recursive Extraction} {\qualid$_1$} \ldots{} {\qualid$_n$}{\tt .}\\
   Recursively extracts all the material needed for the extraction of 
-  globals {\qualid$_1$} \ldots{} {\qualid$_n$}.
+  globals {\qualid$_1$}, \ldots, {\qualid$_n$}.
 \end{Variants}
 
 \SeeAlso Chapter~\ref{Extraction}.
@@ -170,12 +170,12 @@ Search (@eq bool).
 
 \begin{Variants}
 \item
-{\tt Search {\term} inside {\module$_1$} \ldots{} {\module$_n$}.}
+{\tt Search} {\term} {\tt inside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
 
 This restricts the search to constructions defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
 
-\item {\tt Search {\term} outside {\module$_1$} \ldots{} {\module$_n$}.}
+\item {\tt Search} {\term} {\tt outside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
 
 This restricts the search to constructions not defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
@@ -240,8 +240,8 @@ search excludes the objects that mention that {\termpattern} or that
 {\str}.
 
 \item
-  {\tt SearchAbout \nelist{{\termpatternorstr}}{}
-    inside {\module$_1$} \ldots{} {\module$_n$}.}
+  {\tt SearchAbout} \nelist{{\termpatternorstr}}{}
+    {\tt inside} {\module$_1$} \ldots{} {\module$_n$}{\tt .}
 
 This restricts the search to constructions defined in modules
 {\module$_1$} \ldots{} {\module$_n$}.
@@ -559,7 +559,7 @@ with the mapping used to compile the file.
   Export} {\it B}, then the command {\tt Require Import} {\it A}
   also imports the module {\it B}.
 
-\item {\tt Require \zeroone{Import {\sl |} Export} {\qualid}$_1$ \ldots {\qualid}$_n$.}
+\item {\tt Require \zeroone{Import {\sl |} Export}} {\qualid}$_1$ {\ldots} {\qualid}$_n${\tt .}
 
   This loads the modules {\qualid}$_1$, \ldots, {\qualid}$_n$ and
   their recursive dependencies. If {\tt Import} or {\tt Export} is
@@ -618,7 +618,7 @@ This command displays the list of library files loaded in the current
 imported.
 
 \subsection[\tt Declare ML Module {\str$_1$} .. {\str$_n$}.]{\tt Declare ML Module {\str$_1$} .. {\str$_n$}.\comindex{Declare ML Module}}
-This commands loads the Objective Caml compiled files {\str$_1$} {\dots}
+This commands loads the Objective Caml compiled files {\str$_1$} {\ldots}
 {\str$_n$} (dynamic link). It is mainly used to load tactics
 dynamically.
 % (see Chapter~\ref{WritingTactics}).
@@ -974,13 +974,13 @@ computation of algebraic values, such as numbers, and for reflexion-based
 tactics. The commands to fine-tune the reduction strategies and the
 lazy conversion algorithm are described first.
 
-\subsection[\tt Opaque \qualid$_1$ {\dots} \qualid$_n$.]{\tt Opaque \qualid$_1$ {\dots} \qualid$_n$.\comindex{Opaque}\label{Opaque}} 
+\subsection[{\tt Opaque} \qualid$_1$ {\ldots} \qualid$_n${\tt .}]{{\tt Opaque} \qualid$_1$ {\ldots} \qualid$_n${\tt .}\comindex{Opaque}\label{Opaque}}
 This command has an effect on unfoldable constants, i.e. 
 on constants defined by {\tt Definition} or {\tt Let} (with an explicit
 body), or by a command assimilated to a definition such as {\tt
 Fixpoint}, {\tt Program Definition}, etc, or by a proof ended by {\tt
 Defined}. The command tells not to unfold
-the constants {\qualid$_1$} {\dots} {\qualid$_n$} in tactics using
+the constants {\qualid$_1$} {\ldots} {\qualid$_n$} in tactics using
 $\delta$-conversion (unfolding a constant is replacing it by its
 definition).
 
@@ -990,7 +990,7 @@ case {\Coq} has to check the conversion (see Section~\ref{conv-rules})
 of two distinct applied constants.
 
 The scope of {\tt Opaque} is limited to the current section, or
-current file, unless the variant {\tt Global Opaque \qualid$_1$ {\dots}
+current file, unless the variant {\tt Global Opaque \qualid$_1$ {\ldots}
 \qualid$_n$} is used.
 
 \SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
@@ -1004,7 +1004,7 @@ environment}\\
     and if \texttt{bar} does not exist, \texttt{foo} is set opaque.
 \end{ErrMsgs}
 
-\subsection[\tt Transparent \qualid$_1$ {\dots} \qualid$_n$.]{\tt Transparent \qualid$_1$ {\dots} \qualid$_n$.\comindex{Transparent}\label{Transparent}}
+\subsection[{\tt Transparent} \qualid$_1$ {\ldots} \qualid$_n${\tt .}]{{\tt Transparent} \qualid$_1$ {\ldots} \qualid$_n${\tt .}\comindex{Transparent}\label{Transparent}}
 This command is the converse of {\tt Opaque} and it applies on
 unfoldable constants to restore their unfoldability after an {\tt
 Opaque} command.
@@ -1018,8 +1018,8 @@ distinguishes lemmas from the usual defined constants, whose actual
 values are of course relevant in general.
 
 The scope of {\tt Transparent} is limited to the current section, or
-current file, unless the variant {\tt Global Transparent \qualid$_1$
-\dots \qualid$_n$} is used.
+current file, unless the variant {\tt Global Transparent} \qualid$_1$
+{\ldots} \qualid$_n$ is used.
 
 \begin{ErrMsgs}
 % \item \errindex{Can not set transparent.}\\
@@ -1032,12 +1032,12 @@ environment}\\
 \SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing},
 \ref{Theorem}
 
-\subsection{\tt Strategy {\it level} [ \qualid$_1$ {\dots} \qualid$_n$
-  ].\comindex{Strategy}\comindex{Local Strategy}\label{Strategy}}
+\subsection{{\tt Strategy} {\it level} {\tt [} \qualid$_1$ {\ldots} \qualid$_n$
+  {\tt ].}\comindex{Strategy}\comindex{Local Strategy}\label{Strategy}}
 This command generalizes the behavior of {\tt Opaque} and {\tt
   Transparent} commands. It is used to fine-tune the strategy for
 unfolding constants, both at the tactic level and at the kernel
-level. This command associates a level to \qualid$_1$ {\dots}
+level. This command associates a level to \qualid$_1$ {\ldots}
 \qualid$_n$. Whenever two expressions with two distinct head
 constants are compared (for instance, this comparison can be triggered
 by a type cast), the one with lower level is expanded first. In case
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index d69098d0b..054a3261a 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -130,8 +130,8 @@ one gulp, as a proof term (see Section~\ref{exact}).
 
 \SeeAlso {\tt Proof with {\tac}.} in Section~\ref{ProofWith}.
 
-\subsection[\tt Proof using {\ident$_1$ \dots {\ident$_n$}}.]
-{\tt Proof using {\ident$_1$ \dots {\ident$_n$}}.
+\subsection[{\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$}{\tt .}]
+{{\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$}{\tt .}
 \comindex{Proof using} \label{ProofUsing}}
 
 This command applies in proof editing mode. 
@@ -145,7 +145,7 @@ For example if {\tt T} is variable and {\tt a} is a variable of
 type {\tt T}, the commands {\tt Proof using a} and
 {\tt Proof using T a} are actually equivalent.
 
-\variant {\tt Proof using {\ident$_1$ \dots {\ident$_n$}} with {\tac}.} 
+\variant {\tt Proof using} {\ident$_1$} {\ldots} {\ident$_n$} {\tt with} {\tac}{\tt .} 
 in Section~\ref{ProofWith}.
 
 \subsection[\tt Abort.]{\tt Abort.\comindex{Abort}}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 124036afa..f35596f91 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -302,9 +302,9 @@ the tactic {\tt intro} applies the tactic {\tt red} until the tactic
   constant then the latter can still be referred to by a qualified name
   (see \ref{LongNames}).
 
-\item {\tt intros \ident$_1$ \dots\ \ident$_n$} 
+\item {\tt intros \ident$_1$ \mbox{\dots} \ident$_n$} 
   
-  Is equivalent to the composed tactic {\tt intro \ident$_1$; \dots\ ;
+  Is equivalent to the composed tactic {\tt intro \ident$_1$; \mbox{\dots} ;
     intro \ident$_n$}.
 
   More generally, the \texttt{intros} tactic takes a pattern as
@@ -418,18 +418,18 @@ Section~\ref{pattern} to transform the goal so that it gets the form
 
 \begin{Variants}
 
-\item{\tt apply {\term} with {\term$_1$} \dots\ {\term$_n$}} 
-  \tacindex{apply \dots\ with}
+\item{\tt apply {\term} with {\term$_1$} \mbox{\dots} {\term$_n$}} 
+  \tacindex{apply \mbox{\dots} with}
   
   Provides {\tt apply} with explicit instantiations for all dependent
   premises of the type of {\term} which do not occur in the conclusion
   and consequently cannot be found by unification. Notice that
-  {\term$_1$} \dots\ {\term$_n$} must be given according to the order
+  {\term$_1$} \mbox{\dots} {\term$_n$} must be given according to the order
   of these dependent premises of the type of {\term}.
 
   \ErrMsg \errindex{Not the right number of missing arguments}
 
-\item{\tt apply {\term} with ({\vref$_1$} := {\term$_1$}) \dots\ ({\vref$_n$}
+\item{\tt apply {\term} with ({\vref$_1$} := {\term$_1$}) \mbox{\dots} ({\vref$_n$}
     := {\term$_n$})} 
   
   This also provides {\tt apply} with values for instantiating
@@ -498,7 +498,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form
 \end{Variants}
 
 \subsection{{\tt apply {\term} in {\ident}}
-\tacindex{apply \ldots\ in}}
+\tacindex{apply {\ldots} in}}
 
 This tactic applies to any goal.  The argument {\term} is a term
 well-formed in the local context and the argument {\ident} is an
@@ -779,13 +779,13 @@ where $G'$ is obtained from $G$ by replacing all occurrences of $t$ by
 {\tt x}. The name of the variable (here {\tt n}) is chosen based on $T$.
 
 \begin{Variants}
-\item {\tt generalize {\term$_1$ , \dots\ , \term$_n$}}
+\item {\tt generalize {\term$_1$ , \mbox{\dots} , \term$_n$}}
   
-  Is equivalent to {\tt generalize \term$_n$; \dots\ ; generalize
+  Is equivalent to {\tt generalize \term$_n$; \mbox{\dots} ; generalize
     \term$_1$}. Note that the sequence of \term$_i$'s are processed
   from $n$ to $1$.
 
-\item {\tt generalize {\term} at {\num$_1$ \dots\ \num$_i$}}
+\item {\tt generalize {\term} at {\num$_1$ \mbox{\dots} \num$_i$}}
   
   Is equivalent to {\tt generalize \term} but generalizing only over
   the specified occurrences of {\term} (counting from left to right on the
@@ -796,10 +796,10 @@ where $G'$ is obtained from $G$ by replacing all occurrences of $t$ by
   Is equivalent to {\tt generalize \term} but use {\ident} to name the
   generalized hypothesis.
 
-\item {\tt generalize {\term$_1$} at {\num$_{11}$ \dots\ \num$_{1i_1}$} 
+\item {\tt generalize {\term$_1$} at {\num$_{11}$ \mbox{\dots} \num$_{1i_1}$} 
                       as {\ident$_1$}
                       , {\ldots} ,
-                      {\term$_n$} at {\num$_{n1}$ \dots\ \num$_{ni_n}$}
+                      {\term$_n$} at {\num$_{n1}$ \mbox{\dots} \num$_{ni_n}$}
                       as {\ident$_2$}}
   
   This is the most general form of {\tt generalize} that combines the
@@ -813,11 +813,11 @@ where $G'$ is obtained from $G$ by replacing all occurrences of $t$ by
 \end{Variants}
 
 
-\subsection{\tt revert  \ident$_1$ \dots\ \ident$_n$
+\subsection{\tt revert  \ident$_1$ \mbox{\dots} \ident$_n$
 \tacindex{revert}
 \label{revert}}
 
-This applies to any goal with variables \ident$_1$ \dots\ \ident$_n$.
+This applies to any goal with variables \ident$_1$ \mbox{\dots} \ident$_n$.
 It moves the hypotheses (possibly defined) to the goal, if this respects
 dependencies. This tactic is the inverse of {\tt intro}. 
 
@@ -847,7 +847,7 @@ This tactic applies to any goal. It implements the rule
 \item \errindex{Not convertible}
 \end{ErrMsgs}
 
-\tacindex{change \dots\ in}
+\tacindex{change \mbox{\dots} in}
 \begin{Variants}
 \item {\tt change \term$_1$ with \term$_2$} 
   
@@ -855,9 +855,9 @@ This tactic applies to any goal. It implements the rule
   current goal.  The terms \term$_1$ and \term$_2$ must be
   convertible.
 
-\item {\tt change \term$_1$ at \num$_1$ \dots\ \num$_i$ with \term$_2$} 
+\item {\tt change \term$_1$ at \num$_1$ \mbox{\dots} \num$_i$ with \term$_2$} 
   
-  This replaces the occurrences numbered \num$_1$ \dots\ \num$_i$ of
+  This replaces the occurrences numbered \num$_1$ \mbox{\dots} \num$_i$ of
   \term$_1$ by \term$_2$ in the current goal.
   The terms \term$_1$ and \term$_2$ must be convertible.
 
@@ -867,7 +867,7 @@ This tactic applies to any goal. It implements the rule
 
 \item {\tt change \term$_1$ with \term$_2$ in {\ident}}
   
-\item {\tt change \term$_1$ at  \num$_1$ \dots\ \num$_i$ with \term$_2$ in
+\item {\tt change \term$_1$ at  \num$_1$ \mbox{\dots} \num$_i$ with \term$_2$ in
     {\ident}}
   
   This applies the {\tt change} tactic not to the goal but to the
@@ -1067,7 +1067,7 @@ different forms:
 
 \begin{itemize}
 \item In a bindings list of the form {\tt (\vref$_1$ := \term$_1$)
-  \dots\ (\vref$_n$ := \term$_n$)}, {\vref} is either an {\ident} or a
+  \mbox{\dots} (\vref$_n$ := \term$_n$)}, {\vref} is either an {\ident} or a
   {\num}. The references are determined according to the type of
   {\term}. If \vref$_i$ is an identifier, this identifier has to be
   bound in the type of {\term} and the binding provides the tactic
@@ -1234,29 +1234,37 @@ Goal clauses are written after a conversion tactic (tactics
 are introduced by  the keyword \texttt{in}. If no goal clause is provided,
 the default is to perform the conversion only in the conclusion.
 
-The syntax and description of the various goal clauses is the following:
-\begin{description}
-\item[]\texttt{in {\ident}$_1$ $\ldots$ {\ident}$_n$ |- } only in hypotheses {\ident}$_1$
-  \ldots {\ident}$_n$
-\item[]\texttt{in {\ident}$_1$ $\ldots$ {\ident}$_n$ |- *} in hypotheses {\ident}$_1$ \ldots
-  {\ident}$_n$ and in the conclusion
-\item[]\texttt{in * |-} in every hypothesis
-\item[]\texttt{in *} (equivalent to \texttt{in * |- *}) everywhere
-\item[]\texttt{in (type of {\ident}$_1$) (value of {\ident}$_2$) $\ldots$ |-} in
-  type part of {\ident}$_1$, in the value part of {\ident}$_2$, etc. 
-\end{description}
-
-For backward compatibility, the notation \texttt{in}~{\ident}$_1$\ldots {\ident}$_n$
-performs the conversion in hypotheses {\ident}$_1$\ldots {\ident}$_n$.
+The syntax of goal clauses for conversion is the following:
+\begin{center}
+\begin{tabular}{rcl} 
+{\hyplocation} & ::= & {\ident} $\mid$ {\tt (type of} {\ident}{\tt )} $\mid$ {\tt (value of} {\ident}{\tt )}\\
+{\convclause} & ::= & \texttt{in} \sequence{\hyplocation}{,} {\tt |- \zeroone{*}}\\
+& $\mid$ & \texttt{in * |- \zeroone{*}}\\
+& $\mid$ & \texttt{in *}\\
+ \end{tabular}
+\end{center}
+
+If {\ident} refers to a local definition, then {\tt (type of}
+{\ident}{\tt )} refers to the type part of it only and {\tt (value of}
+{\ident}{\tt )} refers to the value part of it.  If {\tt *} is given
+on the right of {\tt |-}, then the conclusion is concerned
+too. Otherwise, only the listed names of hypotheses are concerned. If
+{\tt *} appears on the left of {\tt |-}, then all hypotheses are
+concerned. Finally, the expression {\tt in *} is an short-hand for
+\texttt{in * |- *}.
+
+For backward compatibility, the notation \texttt{in}~{\ident}$_1$ {\tt
+  ,} {\ldots} {\tt ,} {\ident}$_n$ performs the conversion in
+hypotheses {\ident}$_1$ {\ldots} {\ident}$_n$.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 %voir reduction__conv_x : histoires d'univers.
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\subsection[{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$
-\dots\ \flag$_n$} and {\tt compute}]
-{{\tt cbv \flag$_1$ \dots\ \flag$_n$}, {\tt lazy \flag$_1$
-\dots\ \flag$_n$} and {\tt compute}
+\subsection[{\tt cbv} \flag$_1$ \mbox{\ldots} \flag$_n$, {\tt lazy} \flag$_1$
+\mbox{\ldots} \flag$_n$ and {\tt compute}]
+{{\tt cbv} \flag$_1$ {\ldots} \flag$_n$, {\tt lazy} \flag$_1$
+{\ldots} \flag$_n$ and {\tt compute}
 \tacindex{cbv}
 \tacindex{lazy}
 \tacindex{compute}
@@ -1271,8 +1279,8 @@ pattern-matching over a constructed term, and unfolding of {\tt fix}
 and {\tt cofix} expressions) and $\zeta$ (contraction of local
 definitions), the flag are either {\tt beta}, {\tt delta}, {\tt iota}
 or {\tt zeta}. The {\tt delta} flag itself can be refined into {\tt
-delta [\qualid$_1$\ldots\qualid$_k$]} or {\tt delta
--[\qualid$_1$\ldots\qualid$_k$]}, restricting in the first case the
+delta [}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ]} or {\tt delta
+-[}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ]}, restricting in the first case the
 constants to unfold to the constants listed, and restricting in the
 second case the constant to unfold to all but the ones explicitly
 mentioned. Notice that the {\tt delta} flag does not apply to
@@ -1308,24 +1316,24 @@ computational expressions (i.e. with few dead code).
   
   This is a synonym for {\tt lazy beta delta iota zeta}.
 
-\item {\tt compute [\qualid$_1$\ldots\qualid$_k$]}\\
-      {\tt cbv [\qualid$_1$\ldots\qualid$_k$]}
+\item {\tt compute [}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ]}\\
+      {\tt cbv [}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ]}
 
   These are synonyms of {\tt cbv beta delta
-  [\qualid$_1$\ldots\qualid$_k$] iota zeta}.
+  [}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ] iota zeta}.
   
-\item {\tt compute -[\qualid$_1$\ldots\qualid$_k$]}\\
-      {\tt cbv -[\qualid$_1$\ldots\qualid$_k$]}
+\item {\tt compute -[}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ]}\\
+      {\tt cbv -[}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ]}
 
   These are synonyms of {\tt cbv beta delta
-  -[\qualid$_1$\ldots\qualid$_k$] iota zeta}.
+  -[}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ] iota zeta}.
 
-\item {\tt lazy [\qualid$_1$\ldots\qualid$_k$]}\\
-      {\tt lazy -[\qualid$_1$\ldots\qualid$_k$]}
+\item {\tt lazy [}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ]}\\
+      {\tt lazy -[}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ]}
 
   These are respectively synonyms of {\tt lazy beta delta
-  [\qualid$_1$\ldots\qualid$_k$] iota zeta} and {\tt lazy beta delta
-  -[\qualid$_1$\ldots\qualid$_k$] iota zeta}.
+  [}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ] iota zeta} and {\tt lazy beta delta
+  -[}{\qualid$_1$} {\ldots} {\qualid$_k$}{\tt ] iota zeta}.
 
 \item {\tt vm\_compute} \tacindex{vm\_compute}
 
@@ -1350,9 +1358,9 @@ computational expressions (i.e. with few dead code).
 \tacindex{red}}
 
 This tactic applies to a goal which has the form {\tt
-  forall (x:T1)\dots(xk:Tk), c t1 \dots\ tn} where {\tt c} is a constant.  If
+  forall (x:T1)} {\ldots} {\tt (xk:Tk), c t1} {\ldots} {\tt tn} where {\tt c} is a constant.  If
 {\tt c} is transparent then it replaces {\tt c} with its definition
-(say {\tt t}) and then reduces {\tt (t t1 \dots\ tn)} according to
+(say {\tt t}) and then reduces {\tt (t t1} {\ldots} {\tt tn)} according to
 $\beta\iota\zeta$-reduction rules.
 
 \begin{ErrMsgs}
@@ -1438,14 +1446,14 @@ expression {\tt (minus (S (S x)) (S y))} is simplified to
 {\tt (minus (S x) y)} even if an extra simplification is possible.
 \end{itemize}
 
-\tacindex{simpl \dots\ in}
+\tacindex{simpl \mbox{\dots} in}
 \begin{Variants}
 \item {\tt simpl {\term}}
   
   This applies {\tt simpl} only to the occurrences of {\term} in the
   current goal.
 
-\item {\tt simpl {\term} at \num$_1$ \dots\ \num$_i$}
+\item {\tt simpl {\term} at \num$_1$ \mbox{\dots} \num$_i$}
   
   This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$
   occurrences of {\term} in the current goal.
@@ -1457,7 +1465,7 @@ expression {\tt (minus (S (S x)) (S y))} is simplified to
   This applies {\tt simpl} only to the applicative subterms whose head
   occurrence is {\ident}.
 
-\item {\tt simpl {\ident} at \num$_1$ \dots\ \num$_i$}
+\item {\tt simpl {\ident} at \num$_1$ \mbox{\dots} \num$_i$}
   
   This applies {\tt simpl} only to the \num$_1$, \dots, \num$_i$
 applicative subterms whose head occurrence is {\ident}.
@@ -1481,14 +1489,14 @@ with its $\beta\iota$-normal form.
 
 \begin{Variants}
 \item {\tt unfold {\qualid}$_1$, \dots, \qualid$_n$}
-  \tacindex{unfold \dots\ in}
+  \tacindex{unfold \mbox{\dots} in}
   
   Replaces {\em simultaneously} {\qualid}$_1$, \dots, {\qualid}$_n$
   with their definitions and replaces the current goal with its
   $\beta\iota$ normal form.
 
 \item {\tt unfold {\qualid}$_1$ at \num$_1^1$, \dots, \num$_i^1$,
-\dots,\ \qualid$_n$ at \num$_1^n$ \dots\ \num$_j^n$}
+\dots,\ \qualid$_n$ at \num$_1^n$ \mbox{\dots} \num$_j^n$}
   
   The lists \num$_1^1$, \dots, \num$_i^1$ and \num$_1^n$, \dots,
   \num$_j^n$ specify the occurrences of {\qualid}$_1$, \dots,
@@ -1514,7 +1522,7 @@ with its $\beta\iota$-normal form.
   Section~\ref{scopechange}).
 
 \item {\tt unfold \qualidorstring$_1$ at \num$_1^1$, \dots, \num$_i^1$,
-\dots,\ \qualidorstring$_n$ at \num$_1^n$ \dots\ \num$_j^n$}
+\dots,\ \qualidorstring$_n$ at \num$_1^n$ \mbox{\dots} \num$_j^n$}
 
   This is the most general form, where {\qualidorstring} is either a
   {\qualid} or a {\qstring} referring to a notation.
@@ -1531,7 +1539,7 @@ replaced by \term.
 \begin{Variants}
 \item {\tt fold} \term$_1$ \dots\ \term$_n$ 
   
-  Equivalent to {\tt fold} \term$_1${\tt;}\ldots{\tt; fold} \term$_n$.
+  Equivalent to {\tt fold} \term$_1$ {\tt;} {\ldots} {\tt; fold} \term$_n$.
 \end{Variants}
 
 \subsection{{\tt pattern {\term}}
@@ -1555,13 +1563,13 @@ x}$)$) $t$}.  This command can be used, for instance, when the tactic
 {\tt apply} fails on matching.
 
 \begin{Variants}
-\item {\tt pattern {\term} at {\num$_1$} \dots\ {\num$_n$}}
+\item {\tt pattern {\term} at {\num$_1$} \mbox{\dots} {\num$_n$}}
   
   Only the occurrences {\num$_1$} \dots\ {\num$_n$} of {\term} are
   considered for $\beta$-expansion. Occurrences are located from left
   to right.
 
-\item {\tt pattern {\term} at - {\num$_1$} \dots\ {\num$_n$}}
+\item {\tt pattern {\term} at - {\num$_1$} \mbox{\dots} {\num$_n$}}
   
   All occurrences except the occurrences of indexes {\num$_1$} \dots\
   {\num$_n$} of {\term} are considered for
@@ -1569,15 +1577,15 @@ x}$)$) $t$}.  This command can be used, for instance, when the tactic
 
 \item {\tt pattern {\term$_1$}, \dots, {\term$_m$}}
   
-  Starting from a goal $\phi(t_1 \dots\ t_m)$, the tactic
+  Starting from a goal $\phi(t_1 \mbox{\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
+   (fun (x$_1$:$A_1$) \mbox{\dots} (x$_m$:$A_m$) => $\phi(${\tt x$_1$\dots\
+   x$_m$}$)$) $t_1$ \mbox{\dots} $t_m$}.\\ If $t_i$ occurs in one of the
    generated types $A_j$ these occurrences will also be considered and
    possibly abstracted.
 
-\item {\tt pattern {\term$_1$} at {\num$_1^1$} \dots\ {\num$_{n_1}^1$}, \dots,
-    {\term$_m$} at {\num$_1^m$} \dots\ {\num$_{n_m}^m$}}
+\item {\tt pattern {\term$_1$} at {\num$_1^1$} \mbox{\dots} {\num$_{n_1}^1$}, \dots,
+    {\term$_m$} at {\num$_1^m$} \mbox{\dots} {\num$_{n_m}^m$}}
   
   This behaves as above but processing only the occurrences \num$_1^1$,
   \dots, \num$_i^1$ of \term$_1$, \dots, \num$_1^m$, \dots, \num$_j^m$
@@ -1745,7 +1753,7 @@ induction n.
 \begin{ErrMsgs}
 \item \errindex{Not an inductive product}
 \item \errindex{Unable to find an instance for the variables
-{\ident} \ldots {\ident}}
+{\ident} {\ldots} {\ident}}
   
   Use in this case 
   the variant {\tt elim \dots\ with \dots} below.
@@ -1757,18 +1765,18 @@ induction n.
   This behaves as {\tt induction {\term}} but uses the names in
   {\disjconjintropattern} to name the variables introduced in the context.
   The {\disjconjintropattern} must typically be of the form
-  {\tt [} $p_{11}$ \ldots
-  $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
+  {\tt [} $p_{11}$ {\ldots}
+  $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ {\ldots} $p_{mn_m}$ {\tt
     ]} with $m$ being the number of constructors of the type of
   {\term}. Each variable introduced by {\tt induction} in the context
-  of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
+  of the $i^{th}$ goal gets its name from the list $p_{i1}$ {\ldots}
   $p_{in_i}$ in order. If there are not enough names, {\tt induction}
   invents names for the remaining variables to introduce. More
   generally, the $p_{ij}$ can be any disjunctive/conjunctive
   introduction pattern (see Section~\ref{intros-pattern}). For instance,
   for an inductive type with one constructor, the pattern notation
-  {\tt ($p_{1}$,\ldots,$p_{n}$)} can be used instead of
-  {\tt [} $p_{1}$ \ldots $p_{n}$ {\tt ]}.
+  {\tt (}$p_{1}$ {\tt ,} {\ldots} {\tt ,} $p_{n}${\tt )} can be used instead of
+  {\tt [} $p_{1}$ {\ldots} $p_{n}$ {\tt ]}.
 
 \item{\tt induction {\term} eqn:{\namingintropattern}}
 
@@ -1807,7 +1815,7 @@ induction n.
   This behaves as {\tt induction {\term$_1$} using {\term$_2$}} but
   also providing instances for the premises of the type of {\term$_2$}.
 
-\item \texttt{induction {\term}$_1$, $\ldots$, {\term}$_n$ using {\qualid}}
+\item \texttt{induction {\term}$_1$, {\ldots}, {\term}$_n$ using {\qualid}}
 
   This syntax is used for the case {\qualid} denotes an induction principle
   with complex predicates as the induction principles generated by
@@ -1959,11 +1967,11 @@ syntax {\tt destruct ({\num})} (not very interesting anyway).
   
   This behaves as {\tt destruct {\term}} but uses the names in
   {\intropattern} to name the variables introduced in the context.
-  The {\intropattern} must have the form {\tt [} $p_{11}$ \ldots
-  $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ \ldots $p_{mn_m}$ {\tt
+  The {\intropattern} must have the form {\tt [} $p_{11}$ {\ldots}
+  $p_{1n_1}$ {\tt |} {\ldots} {\tt |} $p_{m1}$ {\ldots} $p_{mn_m}$ {\tt
     ]} with $m$ being the number of constructors of the type of
   {\term}. Each variable introduced by {\tt destruct} in the context
-  of the $i^{th}$ goal gets its name from the list $p_{i1}$ \ldots
+  of the $i^{th}$ goal gets its name from the list $p_{i1}$ {\ldots}
   $p_{in_i}$ in order. If there are not enough names, {\tt destruct}
   invents names for the remaining variables to introduce. More
   generally, the $p_{ij}$ can be any disjunctive/conjunctive
@@ -2105,8 +2113,8 @@ introduction pattern $p$:
 \item introduction on \texttt{\ident} behaves as described in
   Section~\ref{intro};
 \item introduction over a disjunction of list of patterns {\tt
-  [$p_{11}$ {\ldots} $p_{1m_1}$ | {\ldots} | $p_{11}$ {\ldots}
-    $p_{nm_n}$]} expects the product to be over an inductive type
+  [}$p_{11}$ {\ldots} $p_{1m_1}$ {\tt |} {\ldots} {\tt |} $p_{11}$ {\ldots}
+    $p_{nm_n}${\tt ]} expects the product to be over an inductive type
   whose number of constructors is $n$ (or more generally over a type
   of conclusion an inductive type built from $n$ constructors,
   e.g. {\tt C -> A$\backslash$/B if $n=2$}): it destructs the introduced
@@ -2119,17 +2127,17 @@ introduction pattern $p$:
   introduced (for instance, the list of patterns {\tt [$\;$|$\;$] H}
   applied on goal {\tt forall x:nat, x=0 -> 0=x} behaves the same as
   the list of patterns {\tt [$\,$|$\,$?$\,$] H});
-\item introduction over a conjunction of patterns {\tt ($p_1$, \ldots,
-  $p_n$)} expects the goal to be a product over an inductive type $I$ with a
+\item introduction over a conjunction of patterns {\tt (}$p_1${\tt ,} {\ldots}{\tt ,}
+  $p_n${\tt )} expects the goal to be a product over an inductive type $I$ with a
   single constructor that itself has at least $n$ arguments: it
   performs a case analysis over the hypothesis, as {\tt destruct}
-  would, and applies the patterns $p_1$~\ldots~$p_n$ to the arguments
+  would, and applies the patterns $p_1$ {\ldots} $p_n$ to the arguments
   of the constructor of $I$ (observe that {\tt ($p_1$, {\ldots},
   $p_n$)} is an alternative notation for {\tt [$p_1$ {\ldots}
   $p_n$]});
-\item introduction via {\tt ( $p_1$ \& \ldots \& $p_n$ )}
+\item introduction via {\tt (} $p_1$ {\tt \&} {\ldots} {\tt \&} $p_n$ {\tt )}
   is a shortcut for introduction via
-  {\tt ($p_1$,(\ldots,(\dots,$p_n$)\ldots))}; it expects the
+  {\tt (}$p_1$ {\tt ,(}{\ldots}{\tt ,(}{\dots}{\tt ,}$p_n$){\ldots}{\tt ))}; it expects the
   hypothesis to be a sequence of right-associative binary inductive 
   constructors such as {\tt conj} or {\tt ex\_intro}; for instance, an
   hypothesis with type {\tt A\verb|/\|exists x, B\verb|/\|C\verb|/\|D} can be
@@ -2149,8 +2157,8 @@ introduction pattern $p$:
   removed.
 \end{itemize}
 
-\Rem {\tt intros $p_1~\ldots~p_n$} is not equivalent to \texttt{intros
-  $p_1$;\ldots; intros $p_n$} for the following reasons:
+\Rem {\tt intros} $p_1$ {\ldots} $p_n$ is not equivalent to \texttt{intros}
+  $p_1${\tt ;} {\ldots}{\tt ; intros} $p_n$ for the following reasons:
 \begin{itemize}
 \item A wildcard pattern never succeeds when applied isolated on a
   dependent product, while it succeeds as part of a list of
@@ -2494,7 +2502,7 @@ 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$, \ldots, $\term_n$}\\
+\item {\tt rewrite} $\term_1${\tt ,} {\ldots}{\tt ,} $\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.
@@ -2581,7 +2589,7 @@ It is equivalent to {\tt apply refl\_equal}.
 
 \begin{ErrMsgs}
 \item \errindex{The conclusion is not a substitutive equation}
-\item \errindex{Impossible to unify \dots\ with \dots.}
+\item \errindex{Impossible to unify \dots\ with \dots}
 \end{ErrMsgs}
 
 \subsection{\tt symmetry
@@ -2978,14 +2986,14 @@ latter is first introduced in the local context using
   The arguments of the $i^{th}$ constructor and the
   equalities that {\tt inversion} introduces in the context of the
   goal corresponding to the $i^{th}$ constructor, if it exists, get
-  their names from the list $p_{i1}$ \ldots $p_{in_i}$ in order. If
+  their names from the list $p_{i1}$ {\ldots} $p_{in_i}$ in order. If
   there are not enough names, {\tt induction} invents names for the
   remaining variables to introduce. In case an equation splits into
   several equations (because {\tt inversion} applies {\tt injection}
   on the equalities it generates), the corresponding name $p_{ij}$ in
   the list must be replaced by a sublist of the form {\tt [$p_{ij1}$
-  \ldots $p_{ijq}$]} (or, equivalently, {\tt ($p_{ij1}$,
-  \ldots, $p_{ijq}$)}) where $q$ is the number of subequalities
+  {\ldots} $p_{ijq}$]} (or, equivalently, {\tt ($p_{ij1}$,
+  {\ldots}, $p_{ijq}$)}) where $q$ is the number of subequalities
   obtained from splitting the original equation. Here is an example.
 
 \begin{coq_eval}
@@ -3030,19 +3038,19 @@ Abort.
   \texttt{inversion} {\ident} \texttt{in} \ident$_1$ \dots\ 
   \ident$_n$.
   
-\item \tacindex{inversion\_clear \dots\ in} \texttt{inversion\_clear}
-  {\ident} \texttt{in} \ident$_1$ \ldots \ident$_n$
+\item \tacindex{inversion\_clear {\ldots} in} \texttt{inversion\_clear}
+  {\ident} \texttt{in} \ident$_1$ {\ldots} \ident$_n$
  
   Let \ident$_1$ \dots\ \ident$_n$, be identifiers in the local context. This
-  tactic behaves as generalizing \ident$_1$ \dots\ \ident$_n$, and
+  tactic behaves as generalizing \ident$_1$ {\ldots} \ident$_n$, and
   then performing {\tt inversion\_clear}.
   
-\item \tacindex{inversion\_clear \dots\ as \dots\ in}
+\item \tacindex{inversion\_clear {\ldots} as \dots\ in}
   \texttt{inversion\_clear} {\ident} \texttt{as} {\intropattern}
-  \texttt{in} \ident$_1$ \ldots \ident$_n$
+  \texttt{in} \ident$_1$ {\ldots} \ident$_n$
 
   This allows to name the hypotheses introduced in the context by
-  \texttt{inversion\_clear} {\ident} \texttt{in} \ident$_1$ \ldots
+  \texttt{inversion\_clear} {\ident} \texttt{in} \ident$_1$ {\ldots}
   \ident$_n$.
 
 \item \tacindex{dependent inversion} \texttt{dependent inversion}
@@ -3274,14 +3282,14 @@ hints of the database named {\tt core}.
   Uses all existing hint databases, minus the special database
   {\tt v62}. See Section~\ref{Hints-databases}
 
-\item \texttt{auto using \nterm{lemma}$_1$ , \ldots , \nterm{lemma}$_n$}
+\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$
 
   Uses \nterm{lemma}$_1$, \ldots, \nterm{lemma}$_n$ in addition to
   hints (can be combined with the \texttt{with \ident} option). If
   $lemma_i$ is an inductive type, it is the collection of its
   constructors which is added as hints.
 
-\item \texttt{auto using \nterm{lemma}$_1$ , \ldots , \nterm{lemma}$_n$ with \ident$_1$ \dots\ \ident$_n$}
+\item \texttt{auto using} \nterm{lemma}$_1$ {\tt ,} {\ldots} {\tt ,} \nterm{lemma}$_n$ with \ident$_1$ {\ldots} \ident$_n$
 
   This combines the effects of the {\tt using} and {\tt with} options.
 
@@ -3897,7 +3905,7 @@ legacy one.
 
 \begin{Variants}
 \item\texttt{Local Hint} \textsl{hint\_definition} \texttt{:}
-  \ident$_1$ \ldots\ \ident$_n$
+  \ident$_1$ {\ldots} \ident$_n$
   
   This is used to declare a hint database that must not be exported to the other
   modules that require and import the current module. Inside a
@@ -3909,7 +3917,7 @@ legacy one.
 The general
 command to add a hint to some database \ident$_1$, \dots, \ident$_n$ is:
 \begin{tabbing}
-  \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ \ldots\ \ident$_n$
+  \texttt{Hint} \textsl{hint\_definition} \texttt{:} \ident$_1$ {\ldots} \ident$_n$
 \end{tabbing}
 where {\sl hint\_definition} is one of the following expressions:
 
@@ -4094,7 +4102,7 @@ the tactic.
     database. 
 
 \item\texttt{Local Hint} \textsl{hint\_definition} \texttt{:}
-   \ident$_1$ \ldots\ \ident$_n$
+   \ident$_1$ {\ldots} \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
@@ -4380,7 +4388,7 @@ Its syntax follows the schema :
 
 \noindent
 {\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}\\
-\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to
+\ident$_1$ {\ldots} \ident$_n$ are different inductive principles that must belong to
 the same package of mutual inductive principle definitions. This command
 generates {\ident$_0$} to be the conjunction of the principles: it is
 built from the common premises of the principles and concluded by the