From 25a60b1fcfa2f6017bedd986b1f90fe923d0f3ad Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Nov 2016 14:50:56 +0100
Subject: Document two new variants of refine

They allow to call refine without doing typeclass resolution, allowing
to use refine in typeclass hints.
---
 doc/refman/RefMan-tac.tex | 10 ++++++++++
 1 file changed, 10 insertions(+)

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