From 3a507c03c91efe67afa9f2dd51bf77c7af6df0f5 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Wed, 19 Oct 2016 18:09:36 +0200
Subject: Documenting Hint Resolve -> and <- variants.

These variants are from 8.3 but were never documented except in CHANGES.
---
 doc/refman/RefMan-tac.tex | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'doc')

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}}
-- 
cgit v1.2.3