From 17ec7a0c875014e5322f6098dcd2014072cde9d8 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 18 Oct 2016 14:23:23 +0200
Subject: 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.
---
 doc/refman/RefMan-tac.tex | 7 +++----
 1 file 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}
 
-- 
cgit v1.2.3