ajout d'une passe de latex our avoir un index correct

+ quelques petites retouches sur la doc


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8476 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 2 deletions

diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index 02e6f82784..a2132fb640 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -260,8 +260,8 @@ format} modifier. Here is an example
 \begin{small}
 \begin{coq_example}
 Notation "'If' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
- (at level 200, right associativity, format
-  "'[v   ' 'If'  c1 '/' '[' 'then'  c2  ']' '/' '[' 'else'  c3 ']' ']'").
+(at level 200, right associativity, format
+"'[v   ' 'If'  c1 '/' '[' 'then'  c2  ']' '/' '[' 'else'  c3 ']' ']'").
 \end{coq_example}
 \end{small}
 
@@ -770,6 +770,9 @@ expression. An abbreviation is a special form of notation with no
 parameter and only one symbol which is an identifier. This identifier
 is given with no quotes around. Example:
 
+\begin{coq_eval}
+Require Import List.
+\end{coq_eval}
 \begin{coq_example*}
 Notation List := (list nat).
 \end{coq_example*}