diff options
author | Théo Zimmermann <theo.zimmi@gmail.com> | 2016-10-18 14:23:23 +0200 |
---|---|---|
committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2016-10-18 14:48:53 +0200 |
commit | 17ec7a0c875014e5322f6098dcd2014072cde9d8 (patch) | |
tree | a889b41e2cec632260f6c5c6df6a3e94dd5e5244 | |
parent | 317ae3b327d201530730ed2cce5f44e8763814d4 (diff) |
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.
-rw-r--r-- | doc/refman/RefMan-tac.tex | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 5eb8cedd9..fc6d9c143 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} |