diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-01-01 19:02:49 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-01-01 19:10:49 +0100 |
| commit | d207707c77fa7d1d66652260e9ad717b32610da3 (patch) | |
| tree | 81c99ee2f587f08d560c303fdb22912358360369 /doc | |
| parent | 73c57090f7509e8d076ec7445278404ddc87f31e (diff) | |
Reference the 'external' tactic.
Diffstat (limited to 'doc')
| -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 |