From 9d4200175b9ca66c64e1ef86a5f75dc66c2e3007 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 7 Jan 2004 17:47:45 +0000
Subject: Bug

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

diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex
index 4df89ddf3e..77b14dbd8d 100755
--- a/doc/RefMan-lib.tex
+++ b/doc/RefMan-lib.tex
@@ -197,12 +197,12 @@ Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop :=
 
 The following abbreviations are allowed:
 \begin{center}
-  \begin{tabular}[h]{|l|r|}
+  \begin{tabular}[h]{|l|l|}
     \hline
-    \verb+(exists x:A, P)+     & \verb+(ex A [x:A]P)+ \\
-    \verb+(exists x, P)+       & \verb+(ex A [x:A]P)+ \\
-    \verb+(exists2 x:A, P & Q)+ & \verb+(ex2 A [x:A]P [x:A]Q)+ \\
-    \verb+(exists2 x, P & Q)+   & \verb+(ex2 A [x:A]P [x:A]Q)+ \\
+    \verb+exists x:A, P+     & \verb+ex A (fun x:A => P)+ \\
+    \verb+exists x, P+       & \verb+ex A (fun x:A => P)+ \\
+    \verb+exists2 x:A, P & Q+ & \verb+ex2 A (fun x:A => P) (fun x:A => Q)+ \\
+    \verb+exists2 x, P & Q+   & \verb+ex2 A (fun x:A => P) (fun x:A => Q)+ \\
     \hline
   \end{tabular}
 \end{center}
-- 
cgit v1.2.3