From eee95fec8763a6323f27b86a5ee115305d4f3d9d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 28 Apr 2011 07:11:43 +0000
Subject: Adding "Tactic Notation" in doc index.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14076 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-syn.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index f5c3dfcaff..f63a5044cd 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -345,7 +345,7 @@ Infix "/\" := and (at level 80, right associativity).
 
 \subsection{Reserving notations
 \label{ReservedNotation}
-\comindex{ReservedNotation}}
+\comindex{Reserved Notation}}
 
 A given notation may be used in different contexts. {\Coq} expects all
 uses of the notation to be defined at the same precedence and with the
@@ -1047,7 +1047,8 @@ at the time of use of the abbreviation.
 %except that abbreviations are used for printing (unless the modifier
 %\verb=(only parsing)= is given) while syntactic definitions were not.
 
-\section{Tactic Notations}
+\section{Tactic Notations
+\comindex{Tactic Notation}}
 
 Tactic notations allow to customize the syntax of the tactics of the
 tactic language\footnote{Tactic notations are just a simplification of
-- 
cgit v1.2.3