# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1230133711 18000
# Node ID 33500a15b8720a09d29e70f307baf70be3734591
# Parent  57018f21cd5c04f8155dfd513fbb329fa220bade
More manual bug reports from megacz

diff -r 57018f21cd5c -r 33500a15b872 doc/manual.tex
--- a/doc/manual.tex	Sun Dec 21 12:30:57 2008 -0500
+++ b/doc/manual.tex	Wed Dec 24 10:48:31 2008 -0500
@@ -435,11 +435,11 @@
 
 $$\infer{\Gamma \vdash \mt{fold} :: ((\mt{Name} \to \kappa_1 \to \kappa_2 \to \kappa_2) \to \kappa_2 \to \{\kappa_1\} \to \kappa_2}{}$$
 
-$$\infer{\Gamma \vdash (\overline c) :: (k_1 \times \ldots \times k_n)}{
-  \forall i: \Gamma \vdash c_i :: k_i
+$$\infer{\Gamma \vdash (\overline c) :: (\kappa_1 \times \ldots \times \kappa_n)}{
+  \forall i: \Gamma \vdash c_i :: \kappa_i
 }
-\quad \infer{\Gamma \vdash c.i :: k_i}{
-  \Gamma \vdash c :: (k_1 \times \ldots \times k_n)
+\quad \infer{\Gamma \vdash c.i :: \kappa_i}{
+  \Gamma \vdash c :: (\kappa_1 \times \ldots \times \kappa_n)
 }$$
 
 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c :: \kappa}{
@@ -584,6 +584,7 @@
 \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
   \Gamma \vdash e_1 : \$c_1
   & \Gamma \vdash e_2 : \$c_2
+  & \Gamma \vdash c_1 \sim c_2
 }$$
 
 $$\infer{\Gamma \vdash e \rcut c : \$c'}{
@@ -609,7 +610,7 @@
   & \Gamma_i \vdash e_i : \tau
 }$$
 
-$$\infer{\Gamma \vdash [c_1 \sim c_2] \Rightarrow e : [c_1 \sim c_2] \Rightarrow \tau}{
+$$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : \lambda [c_1 \sim c_2] \Rightarrow \tau}{
   \Gamma \vdash c_1 :: \{\kappa\}
   & \Gamma \vdash c_2 :: \{\kappa\}
   & \Gamma, c_1 \sim c_2 \vdash e : \tau