Improve the documentation of eauto.

Improve the description of what auto/eauto do.
These two tactics rely on the simple version of apply/eapply.
Since this simple version is available to the end user,
it is better to mention it. See also the confusion that such
description can create in the thread "Understanding auto" on Coq-Club.

1 files changed, 3 insertions, 4 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 5eb8cedd95..fc6d9c143c 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3513,8 +3513,8 @@ intact. \texttt{auto} and \texttt{trivial} never fail.
 
 This tactic generalizes {\tt auto}. While {\tt auto} does not try
 resolution hints which would leave existential variables in the goal,
-{\tt eauto} does try them (informally speaking, it uses {\tt eapply}
-where {\tt auto} uses {\tt apply}).
+{\tt eauto} does try them (informally speaking, it uses
+{\tt simple eapply} where {\tt auto} uses {\tt simple apply}).
 As a consequence, {\tt eauto} can solve such a goal:
 
 \begin{coq_eval}
@@ -3529,8 +3529,7 @@ eauto.
 Abort.
 \end{coq_eval}
 
-Note that {\tt ex\_intro} should be declared as an
-hint.
+Note that {\tt ex\_intro} should be declared as a hint.
 
 \SeeAlso Section~\ref{Hints-databases}