diff options
| -rw-r--r-- | doc/faq/FAQ.tex | 8 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 11 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
3 files changed, 5 insertions, 16 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index d6c605809..db3611c30 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. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 267226f3b..9f65c0ef0 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -68,7 +68,7 @@ form {\tt ltac :} {\qualid}. To force the resolution as a reference to a term, use the syntax {\tt ({\qualid})}. \item As shown by the figure, tactical {\tt ||} binds more than the -prefix tacticals {\tt try}, {\tt repeat}, {\tt do}, {\tt info} and +prefix tacticals {\tt try}, {\tt repeat}, {\tt do} and {\tt abstract} which themselves bind more than the postfix tactical ``{\tt \dots\ ;[ \dots\ ]}'' which binds more than ``\dots\ {\tt ;} \dots''. @@ -96,7 +96,6 @@ is understood as \\ {\tacexprpref} & ::= & {\tt do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\ -& | & {\tt info} {\tacexprpref}\\ & | & {\tt progress} {\tacexprpref}\\ & | & {\tt repeat} {\tacexprpref}\\ & | & {\tt try} {\tacexprpref}\\ @@ -839,14 +838,6 @@ The following returns the type of {\term}: {\tt type of} {\term} \end{quote} -\subsubsection[Accessing tactic decomposition]{Accessing tactic decomposition\tacindex{info} -\index{Tacticals!info@{\tt info}}} - -Tactical ``{\tt info} {\tacexpr}'' is not really a tactical. For -elementary tactics, this is equivalent to \tacexpr. For complex tactic -like \texttt{auto}, it displays the operations performed by the -tactic. - \subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract} \index{Tacticals!abstract@{\tt abstract}}} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index e318446a4..89d8df473 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3589,7 +3589,7 @@ Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. Goal forall a b:list (nat * nat), {a = b} + {a <> b}. -info auto with eqdec. +info_auto with eqdec. \end{coq_example} \begin{coq_eval} Abort. |