4 files changed, 10 insertions, 10 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index c1e552a5da..bef0a1686f 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 99eee44e03..3814e4403a 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-syn.tex b/doc/refman/RefMan-syn.tex
index 1fcc1c0df4..21c39de967 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -649,7 +649,7 @@ A recursive pattern for binders can be used in position of a recursive
 pattern for terms. Here is an example:
 
 \begin{coq_example*}
-Notation ``'FUNAPP' x .. y , f'' :=
+Notation "'FUNAPP' x .. y , f" :=
   (fun x => .. (fun y => (.. (f x) ..) y ) ..)
   (at level 200, x binder, y binder, right associativity).
 \end{coq_example*}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 01dc1dec9b..3f12411863 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}