From 2cc7d0be16ce35f7c87fedde0228f08502f0250f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 17 Feb 2015 18:19:49 +0100
Subject: Remove non-existing Tactic Definition command from index.

---
 doc/refman/RefMan-tac.tex | 1 -
 1 file changed, 1 deletion(-)

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:
-- 
cgit v1.2.3