Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-28 01:07:16 -0700 (Wed, 28 May 2003)
Revision: 4626
Log message:

      *** !!!!!!!!!!!!! WARNING !!!!!!!!!!!!!!!! ***
      *** This commit breaks .prlb compatibility ***
      
      I've cleaned up (and removed) some code on the way
      towards implementing a full support for extracting
      computational content from proofs.
      

Changes	Path
+1 -1	metaprl/filter/base/filter_cache.ml
+2 -2	metaprl/filter/base/filter_magic.ml
+33 -524	metaprl/filter/boot/proof_boot.ml
+1 -9	metaprl/filter/boot/proof_term_boot.ml
+0 -24	metaprl/filter/boot/tactic_boot.ml
+5 -13	metaprl/filter/boot/tactic_boot_sig.mlz
+2 -6	metaprl/refiner/refiner/refine.ml
+5 -8	metaprl/refiner/reflib/theory.ml
+1 -1	metaprl/support/shell/package_info.ml
+0 -8	metaprl/support/shell/proof_edit.ml
+0 -2	metaprl/support/shell/proof_edit.mli
+0 -1	metaprl/support/shell/shell.ml
+0 -1	metaprl/support/shell/shell.mli