Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-01-18 18:22:54 -0800 (Tue, 18 Jan 2005)
Revision: 6435
Log message:
(Bug 382) This patch:
1) Changes all the sequents to have exactly one conclusion
2) Fixes a lot of places in the code that confuses "goals" with "conclusions".
I tried making a clearer distinction between hyps/concls of a sequent and
assums/goals of a meta-sequent. In particular, the "sequent_goals" field
became "sequent_concl", "replace_goal" function became "replace_concl", etc.
3) The syntax allows for either one conclusion, or none. If no conclusions is
given, the xnil_term will be used.