Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-12 00:12:49 -0800 (Thu, 12 Feb 2004)
Revision: 5368
Log message:
This is a new approach to implementing recursive sequents (as discussed
with Nathan and Cristian earlier today) - instead of modifying the hypothesis
type, modify the esequent type by adding a separate "array" with the "equality"
parts of the sequent hypothesis. This should make it much easier to process the
sequent in a binding-consistent order.
P.S. The new array component is allowed (but not required) to have zero length
to signify that the sequent is non-recursive.
This commit is the first step - I modifed some (but not all) interface files.