From 50ad71374cbf1adc172022c86dec7a0b3ee7ea2b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 27 Feb 2018 23:52:20 -0500 Subject: Typo in the documentation of the `pattern` tactic --- doc/refman/RefMan-tac.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3