From 3e55afd7a92e8a58f278d94fe459fda273d2e78d Mon Sep 17 00:00:00 2001
From: fbesson
Date: Tue, 25 Aug 2009 20:02:48 +0000
Subject: git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294
 85f007b7-540e-0410-9357-904b9bb8a0f7

---
 doc/refman/Micromega.tex | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/Micromega.tex b/doc/refman/Micromega.tex
index 00e7c04138..a43cd15b06 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
-- 
cgit v1.2.3