From 53502fc2476af73aeaa805e77b15c22c40768810 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 16 Sep 2002 17:10:50 +0000
Subject: Correction typo d'un but Tauto

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8293 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-tac.tex | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/doc/RefMan-tac.tex b/doc/RefMan-tac.tex
index 6358bc1c8f..fb2240123d 100644
--- a/doc/RefMan-tac.tex
+++ b/doc/RefMan-tac.tex
@@ -1644,15 +1644,33 @@ would fail:
   Intros.
   Tauto. (* Auto would fail *)
 \end{coq_example}
+\begin{coq_eval}
+  Abort.
+\end{coq_eval}
 
 Moreover, if it has nothing else to do, {\tt Tauto} performs
 introductions. Therefore, the use of {\tt Intros} in the previous
 proof is unnecessary. {\tt Tauto} can for instance prove the
 following:
 \begin{coq_example}
-  Goal (A:Prop)(P:nat->Prop)(A \/ (x:nat) ~A -> (P x)) -> (x:nat) A -> (P x).
+  Goal (A:Prop)(P:nat->Prop)(A \/ (x:nat) ~A -> (P x)) -> (x:nat) ~A -> (P x).
   Tauto.
 \end{coq_example}
+\begin{coq_eval}
+  Abort.
+\end{coq_eval}
+
+\Rem In contrast, {\tt Tauto} cannot solve the following goal
+
+\begin{coq_example*}
+Goal (A:Prop)(P:nat->Prop)(A \/ (x:nat) ~A -> (P x)) -> (x:nat) ~~ (A \/ (P x)).
+\end{coq_example*}
+\begin{coq_eval}
+Abort.
+\end{coq_eval}
+
+because \verb=(x:nat) ~A -> (P x)= cannot be treated as atomic and an
+instantiation of \verb=x= is necessary.
 
 \subsection{\tt Intuition {\tac}}
 \tacindex{Intuition}\label{Intuition}
-- 
cgit v1.2.3