Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-04 03:05:41 -0700 (Wed, 04 Jun 2003)
Revision: 4641
Log message:
- Added a call-back interface to allow refiner to get ahold of the proof tree
of a derived rule being used.
- Fixed a number of bugs in Refine.term_of_extract (a few still remain,
missing safety checks mostly - some explicitly marked in comments).
- Added (temporarily, as I am hoping to implement a better API later) a function
term_of_extract to MP toploop - it will return the proof extract, given
extracts for rule assumptions.
Still remaining: restore the disabled code that allows refiner to call rewriter
with proper arguments when constructing the extract.