diff options
| author | Matthieu Sozeau | 2016-06-10 01:34:06 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | cad3fa50357d97e309e9d4fc2a877991c83649d8 (patch) | |
| tree | 4a2813f2f831a3058d6e8d99f38bbdf4ce074563 | |
| parent | 98703c8247fd86deab2d82a70c22d43797e4a548 (diff) | |
Document new Hint Mode option.
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 26 | ||||
| -rw-r--r-- | engine/evarutil.ml | 1 |
3 files changed, 22 insertions, 10 deletions
@@ -32,7 +32,10 @@ Tactics Hints - Revised the syntax of [Hint Cut] to follow standard notation for regexps. - +- Hint Mode now accepts "!" which means that the mode matches only if the + argument's head is not an evar (it goes under applications, casts, and + scrutinees of matches and projections). + Program - The "Shrink Obligations" flag now applies to all obligations, not only those diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 89b8107ed7..c4ea1f5f9c 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3862,25 +3862,33 @@ is to set the cut expression to $c | e$, the initial cut expression being \texttt{emp}. -\item \texttt{Mode} {\tt (+ | -)}$^*$ {\qualid} +\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. +hints associated to qualid can be applied or not. A mode specification +is a list of $n$ {\tt +}, {\tt !} or {\tt -} items that specify if an +argument of the identifier is to be treated as an input ({\tt +}), if +its head only is an input ({\tt !}) or an output ({\tt -}) of the +identifier. For a mode to match a list of arguments, input terms and +input heads \emph{must not} contain existential variables or be +existential variables respectively, 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. + +The head of a term is understood here as the applicative head, or the +match or projection scrutinee's head, recursively, casts being ignored. {\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. +to be driven by that index of the class, with {\tt !} giving more +flexibility by allowing existentials to still appear deeper in the index +but not at its head. \end{itemize} diff --git a/engine/evarutil.ml b/engine/evarutil.ml index c5dfe30332..4506fddb5f 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -192,6 +192,7 @@ let head_evar = | Case (_,_,c,_) -> hrec c | App (c,_) -> hrec c | Cast (c,_,_) -> hrec c + | Proj (p, c) -> hrec c | _ -> raise NoHeadEvar in hrec |