From 0b6bb113559381f05a101f4b288c359539f48a1a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 11 Sep 2014 11:53:57 +0200
Subject: Fixing bug #3605.

---
 doc/refman/Micromega.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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});
-- 
cgit v1.2.3