Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-06-04 13:56:02 -0700 (Wed, 04 Jun 2003)
Revision: 4647
Log message:
Term extraction from proofs finally works!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
The current implementation is full of holes (basically, a lot of safety
checks still need to be added - I believe most of these places are
at least commented with a TODO now), but it's a start.
To access the extracts from toploop, call the (temporarily added) term_of_extract
function. It takes a list of terms that act as extracts for assumptions (the
conclusion part of the sequent only) and outputs the extract for the goal
(full sequent).