diff options
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index f5c3dfcaf..f63a5044c 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 |