diff options
| author | Pierre Boutillier | 2014-04-01 14:43:21 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-04-02 11:25:00 +0200 |
| commit | 98c1d1d8f37dbede1483a983e54ab91058f0c37a (patch) | |
| tree | 396b9e0baf6a768ec37c7d81506f1ef01121211b /doc/faq/FAQ.tex | |
| parent | c3feef4ed5dec126f1144dec91eee9c0f0522a94 (diff) | |
Fix Bug 3131 + Really drop mentions of info in refman.
Diffstat (limited to 'doc/faq/FAQ.tex')
| -rw-r--r-- | doc/faq/FAQ.tex | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index d6c6058095..db3611c305 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -1211,11 +1211,9 @@ Ltac assert_later t := cut t;[intro|idtac]. These two commands perform type checking, but when {\Defined} is used the new definition is set as transparent, otherwise it is defined as opaque (see \ref{opaque}). -\Question{How can I know what a tactic does?} - -You can use the {\tt info} command. - +\Question{How can I know what an automation tactic does in my example?} +You can use its {\tt info} variant: info\_auto, info\_trivial, info\_eauto. \Question{Why {\auto} does not work? How can I fix it?} @@ -1228,7 +1226,7 @@ This is the same tactic as \auto, but it relies on {\eapply} instead of \apply. \Question{How can I speed up {\auto}?} -You can use \texttt{info }{\auto} to replace {\auto} by the tactics it generates. +You can use \texttt{info\_}{\auto} to replace {\auto} by the tactics it generates. You can split your hint bases into smaller ones. |