Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-16 12:42:32 -0800 (Sun, 16 Jan 2005)
Revision: 6411
Log message:
This addresses the problem with failed rewrites that
include contexts. The problem was the scope of the
rewrite arguments.
For example, in the following rule, the argument
is intended to be interpreted as being
within the sequent context.
prim concl_subst TyEqual{'t1; 't2} :
sequent { <H> >- TyEqual{'t1; 't2} } -->
sequent { <H> >- 'e in 't2 } -->
sequent { <H> >- 'e in 't1 }
Rewrites are different--the args are intended to
be closed.