4 files changed, 10 insertions, 10 deletions
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 32142112c..e34babaca 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -8,7 +8,7 @@
 This chapter presents the tactics dedicated to deal with ring and
 field equations.
 
-\asection{What does this tactic?}
+\asection{What does this tactic do?}
 
 \texttt{ring} does associative-commutative rewriting in ring and semi-ring
 structures. Assume you have two binary functions $\oplus$ and $\otimes$
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index 44a88034f..34bc4095a 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -262,7 +262,7 @@ some of the fields and give one of its possible implementations:
 \begin{coq_example}
 Module Type SIG2.
   Declare Module M1 : SIG.
-  Declare Module M2 <: SIG.
+  Module M2 <: SIG.
     Definition T := M1.T.
     Parameter x : T.
   End M2.
@@ -296,18 +296,18 @@ Reset Initial.
   also appear inside modules and module types. Note that in case of a
   module definition like:
 
-    \medskip
+    \smallskip
     \noindent
     {\tt Module N : SIG := M.} 
-    \medskip
+    \smallskip
 
     or
 
-    \medskip
+    \smallskip
     {\tt Module N : SIG.\\
       \ \ \dots\\
       End N.}
-    \medskip 
+    \smallskip 
     
     hints and the like valid for \texttt{N} are not those defined in
     \texttt{M} (or the module body) but the ones defined in
@@ -315,7 +315,7 @@ Reset Initial.
 
 \end{Remarks}
 
-\subsection{Import {\qualid}
+\subsection{\tt Import {\qualid}
 \comindex{Import}
 \label{Import}}
 
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 1fc5b5bf4..1a53adf69 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -769,12 +769,12 @@ and display the time needed to execute it.
 
 \section{Controlling display}
 
-\subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Begin Silent}
+\subsection[\tt Set Silent.]{\tt Set Silent.\comindex{Set Silent}
 \label{Begin-Silent}
 \index{Silent mode}}
 This command turns off the normal displaying.
 
-\subsection[\tt Unset Silent.]{\tt Unset Silent.\comindex{End Silent}}
+\subsection[\tt Unset Silent.]{\tt Unset Silent.\comindex{Unset Silent}}
 This command turns the normal display on.
 
 \subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\comindex{Set Printing Width}}
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index d4f76075c..cd3a786e7 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1003,7 +1003,7 @@ with its $\beta\iota$-normal form.
 
 This tactic applies to any goal. The term \term\ is reduced using the {\tt red}
 tactic. Every occurrence of the resulting term in the goal is then
-substituted for \term.
+replaced by \term.
 
 \begin{Variants}
 \item {\tt fold} \term$_1$ \dots\ \term$_n$