Changes by: Nathaniel Gray (n8gray at caltech.edu)
Date: 2004-07-08 00:25:35 -0700 (Thu, 08 Jul 2004)
Revision: 6042
Log message:
Changed Apply so that the list of type arguments is a sequent. For example:
. Apply{ 'f; 'args; sequent{ <H> >- }
Note that there is no conclusion to the sequent. This is one way of
distinguishing type lists from other kinds of sequents.
This change allows us to clear out a lot of ugly code, including the ListOfHyps
hack and some really gnarly stuff for type checking Apply expressions.