Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-04 13:34:06 -0700 (Mon, 04 Aug 2003)
Revision: 4813
Log message:
The new explicit-contexts code discovered a bug, now we have to
figure out how to fix it.
Consider the following rewrite, which is obviously sensible.
Lambda{x. 'e['x]} : TyAll{y. 't['y]}
<-->
Lambda{x. TyConstrain{'e['x]; 't['x]}} : TyAll{y. 't['y]}
Now consider the sequent form, which does something similar,
but fails because of the context substitution.
sequent [Lambda] { <H> >- 'e } : sequent [TyAll] { <K> >- 't<|K|> }
<-->
sequent [Lambda] { <H> >- TyConstrain{'e; 't<|H|>} } :
sequent [TyAll] { <H> >- 't<|K|> }