diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2013-12-20 01:22:45 +0100 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2013-12-20 01:22:45 +0100 |
| commit | ca1305a0187653edcf63e46b84c65130ac78d117 (patch) | |
| tree | 3a50c809ff3f33b722fb1377a5290162c4f09a8a /doc/refman/Micromega.tex | |
| parent | 631298df172c1e034d6898ff13d5d5aabb9a5098 (diff) | |
micromega: removal of spurious Export; addition of Lia.v encapsulating lia and nia.
Diffstat (limited to 'doc/refman/Micromega.tex')
| -rw-r--r-- | doc/refman/Micromega.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 5f9ed443c..7bdbd6d84 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. |