diff options
| author | Pierre-Marie Pédrot | 2015-10-12 18:54:31 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-12 18:54:31 +0200 |
| commit | 10e5883fed21f9631e1aa65adb7a7e62a529987f (patch) | |
| tree | f04cfc472e6345585eb5f606e2957fcf0f2740ea /doc | |
| parent | 75c5e421e91d49eec9cd55c222595d2ef45325d6 (diff) | |
| parent | 26974a4a2301cc7b1188a3f2f29f3d3368eccc0b (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 7 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 13 |
2 files changed, 15 insertions, 5 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 7011f1ef89..bea25a92f6 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 diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index 5dbf315535..481afa8f87 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -165,14 +165,17 @@ in Section~\ref{ProofWith}. {\tt Type* } is the forward transitive closure of the entire set of section variables occurring in the statement. -\variant {\tt Proof using -(} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).} +\variant {\tt Proof using -( \ident$_1$} {\ldots} {\tt \ident$_n$ ).} Use all section variables except {\ident$_1$} {\ldots} {\ident$_n$}. -\variant {\tt Proof using } {\emph collection$_1$} {\tt + } {\emph collection$_2$} {\tt .} -\variant {\tt Proof using } {\emph collection$_1$} {\tt - } {\emph collection$_2$} {\tt .} -\variant {\tt Proof using } {\emph collection$_1$} {\tt - (} {\ident$_1$} {\ldots} {\ident$_n$} {\tt ).} -\variant {\tt Proof using } {\emph collection$_1$}{\tt* .} +\variant {\tt Proof using \nterm{collection}$_1$ + \nterm{collection}$_2$ .} + +\variant {\tt Proof using \nterm{collection}$_1$ - \nterm{collection}$_2$ .} + +\variant {\tt Proof using \nterm{collection} - ( \ident$_1$} {\ldots} {\tt \ident$_n$ ).} + +\variant {\tt Proof using \nterm{collection} * .} Use section variables being, respectively, in the set union, set difference, set complement, set forward transitive closure. |