diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-01 10:02:23 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-01 10:02:23 +0100 |
| commit | 73a5b7ad59999cdd60dc8a0f922ec606f4cb8d51 (patch) | |
| tree | 6bcada6d3763fbeafb92829a4cdaeb118ab39593 | |
| parent | bd713350ee5197c9411dbe356bc5e7a09af3be27 (diff) | |
| parent | 50ad71374cbf1adc172022c86dec7a0b3ee7ea2b (diff) | |
Merge PR #6861: Typo in the documentation of the `pattern` tactic
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 66a5f107a..9635b3ab1 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3611,7 +3611,7 @@ $\beta$-expansion (the inverse of $\bt$-reduction) of the current goal \item applying the abstracted goal to {\term} \end{enumerate} -For instance, if the current goal $T$ is expressible has $\phi(t)$ +For instance, if the current goal $T$ is expressible as $\phi(t)$ where the notation captures all the instances of $t$ in $\phi(t)$, then {\tt pattern $t$} transforms it into {\tt (fun x:$A$ => $\phi(${\tt x}$)$) $t$}. This command can be used, for instance, when the tactic |