diff options
| author | herbelin | 2004-01-07 17:47:45 +0000 |
|---|---|---|
| committer | herbelin | 2004-01-07 17:47:45 +0000 |
| commit | 9d4200175b9ca66c64e1ef86a5f75dc66c2e3007 (patch) | |
| tree | c69e779179432cd1c0dae84542144341dca8bd6e /doc | |
| parent | 4a6a87154e9914345b5eb493119de8044ee68fd2 (diff) | |
Bug
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8473 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rwxr-xr-x | doc/RefMan-lib.tex | 10 |
1 files 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} |