Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-02-24 16:20:24 -0800 (Thu, 24 Feb 2000)
Revision: 2916
Log message:

      There is no need to call dest_msequent when we only want the goal, but
      not the assumtions.
      
      Speedup: 2% in p4.ml
      

Changes	Path
+10 -13	metaprl/filter/boot/tactic_boot.ml
+1 -0	metaprl/refiner/refiner/refine.ml
+1 -0	metaprl/refiner/refsig/refine_sig.ml