From a03d2a3ae9eb0d318f28c494c37c77c4fe962e81 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 2 Dec 2002 12:47:11 +0000
Subject: `\"' redevenu �chappement pour `"'

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

(limited to 'doc')

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}
-- 
cgit v1.2.3