diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Micromega.tex | 2 |
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}); |