From d207707c77fa7d1d66652260e9ad717b32610da3 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 1 Jan 2014 19:02:49 +0100
Subject: Reference the 'external' tactic.

---
 doc/refman/RefMan-ltac.tex | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index c924c02ebe..267226f3b7 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -867,7 +867,8 @@ without having to cut manually the proof in smaller lemmas.
 
 \ErrMsg \errindex{Proof is not complete}
 
-\subsubsection[Calling an external tactic]{Calling an external tactic\index{Ltac!external}}
+\subsubsection[Calling an external tactic]{Calling an external tactic\tacindex{external}
+\index{Ltac!external}}
 
 The tactic {\tt external} allows to run an executable outside the
 {\Coq} executable. The communication is done via an XML encoding of
-- 
cgit v1.2.3