diff options
| author | Matthieu Sozeau | 2016-10-24 18:18:33 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-11-03 16:26:27 +0100 |
| commit | d6fe6773c959493ed97108e1032b1bd8c1e78081 (patch) | |
| tree | 69d1cb3e8aaf0b1800c0c09b22f70c162948f7d7 /doc | |
| parent | 6ec511721efc9235f6c2fa922a21dcb9b041bbfd (diff) | |
Lets Hints/Instances take an optional pattern
In addition to a priority, cleanup the interfaces for passing this
information as well. The pattern, if given, takes priority over the
inferred one.
We only allow Existing Instances gr ... gr | pri. for now, without
pattern, as before.
Make the API compatible to 8.5 as well.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Classes.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 6 |
2 files changed, 5 insertions, 3 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 144fc22b96..254fca28f7 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -379,7 +379,7 @@ Declares variables according to the given binding context, which might use implicit generalization (see \ref{SectionContext}). \asubsection{\tt typeclasses eauto} -\tacindex{typeclasseseauto} +\tacindex{typeclasses eauto} The {\tt typeclasses eauto} tactic uses a different resolution engine than {\tt eauto} and {\tt auto}. The main differences are the following: diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index c659e19e6b..0aa179d627 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3718,12 +3718,14 @@ command to add a hint to some databases \ident$_1$, \dots, \ident$_n$ is The {\hintdef} is one of the following expressions: \begin{itemize} -\item {\tt Resolve \term} +\item {\tt Resolve \term {\zeroone{{\tt |} \zeroone{\num} \zeroone{\pattern}}}} \comindex{Hint Resolve} This command adds {\tt simple apply {\term}} to the hint list with the head symbol of the type of \term. The cost of that hint is - the number of subgoals generated by {\tt simple apply {\term}}. + the number of subgoals generated by {\tt simple apply {\term}} or \num + if specified. The associated pattern is inferred from the conclusion + of the type of \term or the given \pattern if specified. %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false In case the inferred type of \term\ does not start with a product |