Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-05-12 01:57:03 -0700 (Thu, 12 May 2005)
Revision: 7265
Log message:

      The exception wrappers in filter_exn and refine_exn were turning all
      exceptions into ToploopIgnoreExn (this is a fairly recent thing added by
      Jason). However, it is wrong to blindly turn a RefineError into
      ToploopIgnoreExn (since things like "expand" havily depend on RefineError's
      staying RefineErrors). To address this, I changed tghe wrapper to check
      whether the exception they just printed is a RefineError and if it is, then
      raise RefineError(ToploopIgnoreError) instead of the ToploopIgnoreExn.
      
      P.S. This "fixes" 3 proofs (they were complete, but had "junk" in them that
      caused "expand" to abort).
      

Changes	Path
+8 -1	metaprl/filter/base/filter_exn.ml
+14 -4	metaprl/refiner/reflib/refine_exn.ml