diff options
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 13ff9afb1..cba664f4c 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -975,7 +975,7 @@ without having to cut manually the proof in smaller lemmas. \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 +The tactic {\tt external} runs an executable outside the {\Coq} executable. The communication is done via an XML encoding of constructions. The syntax of the command is |