Document two new variants of refine

They allow to call refine without doing typeclass resolution, allowing
to use refine in typeclass hints.

1 files changed, 10 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 0aa179d627..695b0b883f 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -263,6 +263,16 @@ Defined.
 
   This tactic behaves like {\tt refine}, but it does not shelve any
   subgoal. It does not perform any beta-reduction either.
+\item {\tt notypeclasses refine \term}\tacindex{notypeclasses refine}
+
+  This tactic behaves like {\tt refine} except it performs typechecking
+  without resolution of typeclasses.
+
+\item {\tt simple notypeclasses refine \term}\tacindex{simple
+    notypeclasses refine}
+
+  This tactic behaves like {\tt simple refine} except it performs typechecking
+  without resolution of typeclasses.
 \end{Variants}
 
 \subsection{\tt apply \term}