From 29ff821da57e35d37b41be34febb275306c4809f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Sat, 5 Nov 2016 11:33:42 +0100
Subject: Minor fix in documentation

---
 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 656ae57b95..54393e46f6 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}
-- 
cgit v1.2.3