diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-28 07:11:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-28 07:11:43 +0000 |
| commit | eee95fec8763a6323f27b86a5ee115305d4f3d9d (patch) | |
| tree | 7454a66d7a646bb030448a30ee730faa160e4504 | |
| parent | 39514550177a887a526a66b8ec080cae5c463a9d (diff) | |
Adding "Tactic Notation" in doc index.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14076 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |