`\"' redevenu �chappement pour `"'

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

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index c5fa4bb521..ed286f5584 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -104,7 +104,7 @@ Notation "A /\ B" (and A B) (at level 6, right associativity).
 Notation "A \/ B" (or A B)  (at level 7, right associativity).
 \end{coq_example*}
 
-By default, no associativity is assigned to the notation and the
+By default, the notation is considered non associative and its
 precedence level is 1. The list of level already assigned
 is on figure~\ref{coq-symbols}.
 
@@ -319,7 +319,7 @@ and it is equivalent to
 where {\tt x} and {\tt y} are fresh names distinct from {\qualid}. Here is an example.
 
 \begin{coq_example*}
-Infix "/\" and (at level 6, right associativity).
+Infix "/\\" and (at level 6, right associativity).
 \end{coq_example*}
 
 \section{Symbolic interpretation scopes}