Bug

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

1 files changed, 3 insertions, 3 deletions

diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index bf8375d3e..b367f0e9e 100755
--- a/doc/RefMan-syn.tex
+++ b/doc/RefMan-syn.tex
@@ -178,7 +178,7 @@ to be done. Here is an example.
 
 \begin{coq_example*}
 Notation "'EX' x | p"     := (ex ? [x]p) (at level 10).
-Notation "'EX' x | p & q" := (ex2 t [x]p [x]q) (at level 10).
+Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q) (at level 10).
 \end{coq_example*}
 
 In order to factorise the left part of the rules, the subexpression
@@ -191,7 +191,7 @@ as follows.
 
 \begin{coq_example*}
 Notation "'EX' x | p"     := (ex ? [x]p) (at level 10, p at level 9).
-Notation "'EX' x | p & q" := (ex2 t [x]p [x]q)
+Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q)
   (at level 10, p at level 9).
 \end{coq_example*}
 
@@ -200,7 +200,7 @@ to put q at the same level as p, hence the final version of the rules
 
 \begin{coq_example*}
 Notation "'EX' x | p"     := (ex ? [x]p) (at level 10, p at level 9).
-Notation "'EX' x | p & q" := (ex2 t [x]p [x]q)
+Notation "'EX' x | p & q" := (ex2 ? [x]p [x]q)
   (at level 10, p, q at level 9).
 \end{coq_example*}