Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-29 15:41:42 -0700 (Tue, 29 Apr 2003)
Revision: 4519
Log message:
Moved the "remove the unneeded hyp bindings" call out of term normalization
and added it at appropriate places of proof_boot and refiner. This is needed
to make sure that the sequents unrelated to proofs (e.g. documentation)
are never touched.