Indexation de pose proof, et par la même occasion du nouveau specialize

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10651 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index e7ee8b1a4..bac155bb5 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -556,12 +556,12 @@ in the list of subgoals remaining to prove.
 
    This tactic behaves like \texttt{assert ({\ident} : {\form})}.
 
-\item \texttt{pose proof {\term} as {\ident}}
+\item \texttt{pose proof {\term} as {\ident}\tacindex{pose proof}}
 
   This tactic behaves like \texttt{assert ({\ident:T}) by exact {\term}} where
   \texttt{T} is the type of {\term}. 
 
-\item {\tt specialize ({\ident} \term$_1$ {\ldots} \term$_n$)} \\
+\item {\tt specialize ({\ident} \term$_1$ {\ldots} \term$_n$)\tacindex{specialize}} \\
       {\tt specialize {\ident} with \bindinglist}
 
       The tactic {\tt specialize} works on local hypothesis \ident.