From 64a4b9851f49f5c0d859d60def1f1de8e9549a9d Mon Sep 17 00:00:00 2001
From: glondu
Date: Mon, 5 May 2008 15:09:38 +0000
Subject: Minor updates in the documentation of notations.

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

diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex
index dcac68f1a1..9f607f05e4 100644
--- a/doc/refman/RefMan-syn.tex
+++ b/doc/refman/RefMan-syn.tex
@@ -73,7 +73,7 @@ Consider for example the new notation
 Notation "A \/ B" := (or A B).
 \end{coq_example*}
 
-Clearly, an expression such as {\tt (A:Prop)True \verb=/\= A \verb=\/=
+Clearly, an expression such as {\tt forall A:Prop, True \verb=/\= A \verb=\/=
 A \verb=\/= False} is ambiguous. To tell the {\Coq} parser how to
 interpret the expression, a priority between the symbols \verb=/\= and
 \verb=\/= has to be given. Assume for instance that we want conjunction
@@ -179,7 +179,7 @@ See the next section for more about factorization.
 
 \subsection{Simple factorization rules}
 
-{\Coq} extensible parsing is performed by Camlp4 which is essentially a
+{\Coq} extensible parsing is performed by Camlp5 which is essentially a
 LL1 parser. Hence, some care has to be taken not to hide already
 existing rules by new rules. Some simple left factorization work has
 to be done. Here is an example.
-- 
cgit v1.2.3