diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 49a5b7983a..263766b272 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3709,11 +3709,12 @@ The {\hintdef} is one of the following expressions: the number of subgoals generated by {\tt simple apply {\term}}. %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false - % Is it really needed? - %% In case the inferred type of \term\ does not start with a product - %% the tactic added in the hint list is {\tt exact {\term}}. In case - %% this type can however be reduced to a type starting with a product, - %% the tactic {\tt apply {\term}} is also stored in the hints list. + In case the inferred type of \term\ does not start with a product + the tactic added in the hint list is {\tt exact {\term}}. +% Actually, a slightly restricted version is used (no conversion on the head symbol) + In case + this type can however be reduced to a type starting with a product, + the tactic {\tt simple apply {\term}} is also stored in the hints list. If the inferred type of \term\ contains a dependent quantification on a variable which occurs only in the premisses of the type and not |