diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 263766b272..11de4f35e0 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3744,6 +3744,17 @@ The {\hintdef} is one of the following expressions: Adds each \texttt{Resolve} {\term$_i$}. + \item {\tt Resolve -> \term} + + Adds the left-to-right implication of an equivalence as a hint + (informally the hint will be used as {\tt apply <- \term}, + although as mentionned before, the tactic actually used is + a restricted version of apply). + + \item {\tt Resolve <- \term} + + Adds the right-to-left implication of an equivalence as a hint. + \end{Variants} \item \texttt{Immediate {\term}} |