From 3bf96f48739699da368bb872663945ebdb2d78a4 Mon Sep 17 00:00:00 2001
From: fbesson
Date: Wed, 2 Jul 2008 13:24:47 +0000
Subject: Improved robustness of micromega parser. Proof search of Micromega
 test-suites is now bounded -- ensure termination

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11200 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 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 11e3e8cce3..234d511344 100644
--- a/doc/refman/Micromega.tex
+++ b/doc/refman/Micromega.tex
@@ -17,11 +17,11 @@ Load the {\tt Psatz} module ({\tt Require Psatz}.).  This module defines the tac
   \begin{itemize}
   \item The {\tt psatzl} tactic solves linear goals using an embedded (naive) linear programming prover \emph{i.e.},
     fourier elimination.
-  \item The {\tt psatz} tactic solves polynomial goals using an external prover {\tt cspd}\footnote{Source and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} driver is generating 
+  \item The {\tt psatz} tactic solves polynomial goals using John Harrison's Hol light driver to the external prover {\tt cspd}\footnote{Source and binaries can be found at \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} driver is generating 
     a \emph{proof cache} thus allowing to rerun scripts even without {\tt csdp}. 
   \item The {\tt lia} (linear integer arithmetic) tactic is specialised to solve linear goals over $\mathbb{Z}$.
     It extends {\tt psatzl Z} and exploits the discreetness of $\mathbb{Z}$.
-  \item The {\tt sos} tactic is another driver to the {\tt csdp} prover.  In theory, it is less general than
+  \item The {\tt sos} tactic is another Hol light driver to the {\tt csdp} prover.  In theory, it is less general than
     {\tt psatz}. In practice, even when {\tt psatz} fails, it can be worth a try -- see
     Section~\ref{sec:psatz-back} for details.
   \end{itemize}
-- 
cgit v1.2.3