diff options
author | 2016-11-07 14:50:56 +0100 | |
---|---|---|
committer | 2016-11-07 14:50:56 +0100 | |
commit | 25a60b1fcfa2f6017bedd986b1f90fe923d0f3ad (patch) | |
tree | a67e7204fc6d311da6eb39d9c7c25f8de7cd8764 /doc | |
parent | 1f36cdefd841526f804bd2dd51c1d88309333376 (diff) |
Document two new variants of refine
They allow to call refine without doing typeclass resolution, allowing
to use refine in typeclass hints.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-tac.tex | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 0aa179d62..695b0b883 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} |