Minor fix in documentation

1 files changed, 1 insertions, 1 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 656ae57b9..54393e46f 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1278,7 +1278,7 @@ in the list of subgoals remaining to prove.
 
   In particular, \texttt{pose proof {\term} as {\ident}} behaves as
   \texttt{assert ({\ident} := {\term})} and \texttt{pose proof {\term}
-    as {\intropattern}\tacindex{pose proof}} is the same as applying
+    as {\intropattern}} is the same as applying
   the {\intropattern} to {\term}.
 
 \item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough}