Documenting Hint Resolve -> and <- variants.

These variants are from 8.3 but were never documented except in CHANGES.

1 files changed, 11 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 263766b27..11de4f35e 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}}