Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-13 15:56:38 -0700 (Sun, 13 Jul 2003)
Revision: 4737
Log message:
This implements most of the context binding and scoping structure (as
required by the semantics of sequent schemas).
Still TODO:
- Make sure that variables in rule arguments are parsed according to the scoping
they have in a rule.
- Make sure that variables in term arguments in top loop are parsed according
to the scoping they have in the current mterm.
- Fix the rules that have ill-specified context restrictions, debug, etc.