Document Hint Mode, cleanup Hint doc.

1 files changed, 18 insertions, 22 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9a365b829..903e2e19a 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3669,9 +3669,6 @@ The {\hintdef} is one of the following expressions:
   the number of subgoals generated by {\tt simple apply {\term}}.
 %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false
 
-  The cost of that hint is the number of subgoals generated by that
-  tactic.
-
   % Is it really needed?
   %% In case the inferred type of \term\ does not start with a product
   %% the tactic added in the hint list is {\tt exact {\term}}. In case
@@ -3869,7 +3866,25 @@ is to set the cut expression to $c | e$, the initial cut expression
 being \texttt{emp}.
 
 
+\item \texttt{Mode} {\tt (+ | -)}$^*$ {\qualid}
+\label{HintMode}
+\comindex{Hint Mode}
+
+This sets an optional mode of use of the identifier {\qualid}.  When
+proof-search faces a goal that ends in an application of {\qualid} to
+arguments {\tt \term$_1$ \mbox{\dots} \term$_n$}, the mode tells if the
+hints associated to qualid can be applied or not. A mode specification 
+is a list of $n$ {\tt +} or {\tt -} items that specify if an argument is
+to be treated as an input {\tt +} or an output {\tt -} of the
+identifier. For a mode to match a list of arguments, input terms \emph{must
+not} contain existential variables, while outputs can be any term.
+Multiple modes can be declared for a single identifier, in that case 
+only one mode needs to match the arguments for the hints to be applied.
 
+{\tt Hint Mode} is especially useful for typeclasses, when one does not
+want to support default instances and avoid ambiguity in
+general. Setting a parameter of a class as an input forces proof-search
+to be driven by that index of the class.
 
 \end{itemize}
 
@@ -3877,25 +3892,6 @@ being \texttt{emp}.
 pattern-matching on hypotheses using \texttt{match goal with} inside
 the tactic.
 
-\begin{Variants}
-\item {\tt Hint \hintdef}
-
-  No database name is given: the hint is registered in the {\tt core}
-    database.
-
-\item {\tt Hint Local {\hintdef} : \ident$_1$ \mbox{\dots} \ident$_n$}
-
-  This is used to declare hints that must not be exported to the other
-  modules that require and import the current module. Inside a
-  section, the option {\tt Local} is useless since hints do not
-  survive anyway to the closure of sections.
-
-\item {\tt Hint Local \hintdef}
-
-  Idem for the {\tt core} database.
-
-\end{Variants}
-
 % There are shortcuts that allow to define several goal at once:
 
 % \begin{itemize}