Merge branch 'v8.6'

5 files changed, 12 insertions, 10 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index df5ee405f..5abdecfc1 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -72,7 +72,8 @@
 %\newcommand{\spec}[1]{\{\,#1\,\}}
 
 % Building regular expressions
-\newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
+\newcommand{\zeroone}[1]{\mbox{\sl [}{#1}\mbox{\sl ]}}
+\newcommand{\zeroonelax}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
 %\newcommand{\zeroonemany}[1]{$\{$#1$\}$*}
 %\newcommand{\onemany}[1]{$\{$#1$\}$+}
 \newcommand{\nelistnosep}[1]{{#1} \mbox{\dots} {#1}}
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index bd8ee450e..acfc4bea9 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -380,6 +380,7 @@ use implicit generalization (see \ref{SectionContext}).
 
 \asubsection{\tt typeclasses eauto}
 \tacindex{typeclasses eauto}
+\label{typeclasseseauto}
 
 The {\tt typeclasses eauto} tactic uses a different resolution engine
 than {\tt eauto} and {\tt auto}. The main differences are the following:
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index c1e552a5d..bef0a1686 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -26,13 +26,13 @@ run by the command {\tt coqtop}.
 They are two different binary images of \Coq: the byte-code one and
 the native-code one (if {\ocaml} provides a native-code compiler
 for your platform, which is supposed in the following). By default,
-\verb!coqc! executes the native-code version; this can be overridden
-using the \verb!-byte! option.
+\verb!coqtop! executes the native-code version; run \verb!coqtop.byte! to
+get the byte-code version.
 
 The byte-code toplevel is based on an {\ocaml}
 toplevel (to allow the dynamic link of tactics).  You can switch to
 the {\ocaml} toplevel with the command \verb!Drop.!, and come back to the
-\Coq~toplevel with the command \verb!Toplevel.loop();;!.
+\Coq~toplevel with the command \verb!Coqloop.loop();;!.
 
 \section{Batch compilation ({\tt coqc})}
 The {\tt coqc} command takes a name {\em file} as argument.  Then it
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 99eee44e0..3814e4403 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -713,9 +713,9 @@ definition have a special syntax: ``{\tt let fix}~$f$~{\ldots}~{\tt
            {\tt Inductive} \nelist{\inductivebody}{with} {\tt .} \\
  & $|$ & {\tt CoInductive} \nelist{\inductivebody}{with} {\tt .} \\
            & & \\
-{\inductivebody} & ::= & 
-  {\ident} \zeroone{\binders} {\tt :} {\term} {\tt :=} \\
-   && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstrwithoutblank}}{|}} \\
+{\inductivebody} & ::= &
+  {\ident} \zeroone{\binders} {\typecstr} {\tt :=} \\
+   && ~~\zeroone{\zeroone{\tt |} \nelist{$\!${\ident}$\!$ \zeroone{\binders} {\typecstr}}{|}} \\
            & & \\  %% TODO: where ...
 %% Fixpoints
 {\fixpoint} & ::= & {\tt Fixpoint} \nelist{\fixpointbody}{with} {\tt .} \\
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 01dc1dec9..3f1241186 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -114,7 +114,7 @@ following syntax:
 \begin{tabular}{lcl}
 {\occclause} & ::= & {\tt in} {\occgoalset} \\
 {\occgoalset} & ::= &
-    \zeroone{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
+    \zeroonelax{{\ident$_1$} \zeroone{\atoccurrences} {\tt ,} \\
 &   & {\dots} {\tt ,}\\
 &   & {\ident$_m$} \zeroone{\atoccurrences}}\\
 &   & \zeroone{{\tt |-} \zeroone{{\tt *} \zeroone{\atoccurrences}}}\\
@@ -302,7 +302,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form
 {\tt (fun $x$ => $Q$)~$u_1$~\ldots~$u_n$}.
 
 \begin{ErrMsgs}
-\item \errindex{Impossible to unify \dots\ with \dots}
+\item \errindex{Unable to unify \dots\ with \dots}
 
   The {\tt apply}
   tactic failed to match the conclusion of {\term} and the current goal.
@@ -4621,7 +4621,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{Unable to unify \dots\ with \dots}
 \end{ErrMsgs}
 
 \subsection{\tt symmetry}