diff options
| author |  fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-25 20:02:48 +0000 |
|---|---|---|
| committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-08-25 20:02:48 +0000 |
| commit | 3e55afd7a92e8a58f278d94fe459fda273d2e78d (patch) | |
| tree | d0edd54fc3947a6f676c34b8db8ebb87d059ba9e /doc/refman | |
| parent | 2228cfd26f92c383c795fb6e34d641d3c4e9b83a (diff) | |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/Micromega.tex | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex index 00e7c0413..a43cd15b0 100644 --- a/doc/refman/Micromega.tex +++ b/doc/refman/Micromega.tex @@ -8,7 +8,8 @@ Section~\ref{sec:psatz-back} presents some background explaining the proof princ % Section~\ref{sec:lia} explains how to get a complete procedure for linear integer arithmetic. -\section{The {\tt psatz} tactic in a hurry} +\asection{The {\tt psatz} tactic in a hurry} +\tacindex{psatz} \label{sec:psatz-hurry} Load the {\tt Psatz} module ({\tt Require Psatz}.). This module defines the tactics: {\tt lia}, {\tt psatzl D}, %{\tt sos D} @@ -54,7 +55,7 @@ The following table details for each domain $D \in \{\mathbb{Z},\mathbb{Q},\math \end{array} \] -\section{\emph{Positivstellensatz} refutations} +\asection{\emph{Positivstellensatz} refutations} \label{sec:psatz-back} The name {\tt psatz} is an abbreviation for \emph{positivstellensatz} -- literally positivity theorem -- which @@ -121,7 +122,8 @@ refutation. %% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. % -\section{ {\tt lia} : the linear integer arithmetic tactic } +\asection{ {\tt lia} : the linear integer arithmetic tactic } +\tacindex{lia} \label{sec:lia} The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt romega} tactic (see |