diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-02-17 18:19:49 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-02-17 18:19:49 +0100 |
| commit | 2cc7d0be16ce35f7c87fedde0228f08502f0250f (patch) | |
| tree | 7606f301960d4ed8efdbaa4ecf59c82b68a19db0 | |
| parent | 9bc5a2686497ff5e225510383ccce669bfc19bb9 (diff) | |
Remove non-existing Tactic Definition command from index.
| -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 c2407dce2..a5d053a06 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: |