Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-04 03:05:41 -0700 (Thu, 04 Sep 2003)
Revision: 4929
Log message:
Changed the Refine.extract to contain a pointer to the sentinel used to
create the extract, which in turn contains a pointer to the refiner.
Using these pointer, we garantee that in any extract all parts were
created using the same sentinel and that a derived rule can only be justified
by an extract that was created using the appropriate refiner.
Note - this may cause problems when construction extract from a distributed proof,
as Refine module now expects things to be pointer-equal...