Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-09-01 20:28:23 -0700 (Mon, 01 Sep 2003)
Revision: 4910
Log message:

      Cleaning up and refactoring the refiner implementation.
      
      Now refiner should keep enough information around to be able
      to figure out which axioms a proof is dependent on.
      
      Still to do: need to be able to actually extract out the dependency
      information and a UI to print it (including UI for checking whether
      teh rule is fully grounded or not).
      

Changes	Path
+1 -1	metaprl/filter/filter/filter_prog.ml
+379 -521	metaprl/refiner/refiner/refine.ml
+3 -4	metaprl/refiner/refsig/refine_sig.ml