From 74b38af4176f7125cf1138981f4ee1e539ca1cd7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 6 Feb 2003 14:49:01 +0000
Subject: Bug

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

(limited to 'doc')

diff --git a/doc/RefMan-syn.tex b/doc/RefMan-syn.tex
index bf8375d3ee..b367f0e9ea 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*}
 
-- 
cgit v1.2.3