exceptions and coercions

[Suresh Jagannathan]

I've finished tex'ing the safety=>soundness proof
and the proof of correctness for the closure convertor.
I've now started tex'ing the CPS language and small-step
transition semantics.

I've got a question about exceptions though.  Given

  let x = e1 in handle z => e2
  in  e

I have the flow rule for exceptions being:

  F(x) >= F(last(e1)) and F(last(e)) >= F(last(e2))

However, our notes indicate the closure converted
translation as being:

  let y1 = [e1]
  in X(y1,F(last(e1)),F(last(x)))  

  handle z =>

     let y2 = [e2]
     in X(y2,F(last(e2)),F(last(x)))


I'm confused about why the coercion inserted for the
handler coerces between F(last(e2)) and F(last(x));
shouldn't it be X(y2,F(last(e2)),F(last(e)))?

	  -- sj