diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-11 16:29:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-11 16:29:54 +0200 |
| commit | bf39345125d66d3efd9f934be91200013f57841c (patch) | |
| tree | ddcde5ed56fe97a020fa6a4290bb1f5eebce207e | |
| parent | e9995f6e9f9523d4738d9ee494703b6f96bf995d (diff) | |
Documenting matching under binders.
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index d388840df..04c356e44 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -691,6 +691,13 @@ variables of the form {\tt @?id} that occur in head position of an application. For these variables, the matching is second-order and returns a functional term. +Alternatively, when a metavariable of the form {\tt ?id} occurs under +binders, say $x_1$, \ldots, $x_n$ and the expression matches, the +metavariable is instantiated by a term which can then be used in any +context which also binds the variables $x_1$, \ldots, $x_n$ with +same types. This provides with a primitive form of matching +under context which does not require manipulating a functional term. + If the matching with {\cpattern}$_1$ succeeds, then {\tacexpr}$_1$ is evaluated into some value by substituting the pattern matching instantiations to the metavariables. If {\tacexpr}$_1$ evaluates to a |