diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index c2407dce2c..a5d053a069 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4888,7 +4888,6 @@ proof script in a non-sequential order. \section{Simple tactic macros} \index{Tactic macros} -\comindex{Tactic Definition} \label{TacticDefinition} A simple example has more value than a long explanation: |