Typo in the documentation of the `pattern` tactic

1 files changed, 1 insertions, 1 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 66a5f107a5..9635b3ab1a 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