diff options
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index c924c02eb..267226f3b 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 |