Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-09-02 03:39:19 -0700 (Thu, 02 Sep 2004)
Revision: 6159
Log message:

      Added a work-around for bug 175. Hopefully, once we start using extracts
      somewhere other that ITT (CIC, may be?), we would get more insight and
      finally figure out what's the right "truly general" way of specifying extraction
      is.
      

Changes	Path
+4 -4	metaprl/filter/base/filter_util.ml
+83 -66	metaprl/refiner/refiner/refine.ml
+2 -3	metaprl/refiner/refsig/refine_sig.ml
+3 -0	metaprl/theories/itt/itt_test.ml