Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-02 23:15:19 -0800 (Thu, 02 Mar 2006)
Revision: 8832
Log message:

      My initial fix for the crw bug was not quite right either. Even this one is
      not correct, strictly speaking, but it will only be wrong on cases that we do
      not have (when we have the same context both on the hyp list of the outer
      judgment sequent and nested in one of the clause of that sequent).
      
      The correct fix is relatively simple, but will take at least a few hours -
      will do it after the paper deadlines.
      

Changes  Path
+11 -3 metaprl/refiner/refiner/refine.ml
+5 -0 metaprl/refiner/rewrite/rewrite_match_redex.ml