Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-12-06 20:35:31 -0800 (Mon, 06 Dec 2004)
Revision: 6337
Log message:

      Rewrote the proof squashing code. Hopefully this will fix bug 160 and other
      relatex issues.
      

Changes  Path
+65 -63 metaprl/tactics/proof/proof_boot.ml