From ca1305a0187653edcf63e46b84c65130ac78d117 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Fri, 20 Dec 2013 01:22:45 +0100
Subject: micromega: removal of spurious Export; addition of Lia.v
 encapsulating lia and nia.

---
 doc/refman/Micromega.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
index 5f9ed443c4..7bdbd6d84e 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/refman/Micromega.tex
@@ -132,7 +132,7 @@ Theorem~\ref{thm:psatz}, the goal is valid.
 \tacindex{lia}
 \label{sec:lia}
 
-The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt romega} tactic (see
+The tactic {\tt lia} ({\tt Require Lia.}) offers an alternative to the {\tt omega} and {\tt romega} tactic (see
 Chapter~\ref{OmegaChapter}). 
 %
 Rougthly speaking, the deductive power of {\tt lia} is the combined deductive power of {\tt ring\_simplify} and {\tt omega}.
@@ -145,7 +145,7 @@ following so-called \emph{omega nightmare}~\cite{TheOmegaPaper}.
        -10 <= 7 * x - 9 * y <= 4 ->   False.
 \end{coq_example*}
 \begin{coq_eval}
-intro x; lia;
+intro x; lia.
 \end{coq_eval}
 The estimation of the relative efficiency of lia \emph{vs} {\tt omega}
 and {\tt romega} is under evaluation.
-- 
cgit v1.2.3