Fixing bug #3605.

1 files changed, 1 insertions, 1 deletions

diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
index c9180b40c5..2e4a8059ed 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/refman/Micromega.tex
@@ -6,7 +6,7 @@
 \asection{Short description of the tactics}
 \tacindex{psatz}  \tacindex{lra} 
 \label{sec:psatz-hurry}
-The {\tt Psatz} module ({\tt Require Psatz.}) gives access to several tactics for solving arithmetic goals over
+The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to several tactics for solving arithmetic goals over
  {\tt Z}\footnote{Support for {\tt nat} and {\tt N} is obtained by pre-processing the goal with the {\tt zify} tactic.}, {\tt Q} and {\tt R}:
 \begin{itemize}
 \item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia});