Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-25 00:54:40 -0800 (Wed, 25 Feb 2004)
Revision: 5409
Log message:

      *******************************************
      *               WARNING                   *
      * This commit breaks .prla compatibility! *
      * Export your proofs before updating!!!   *
      *******************************************
      
      Removing the unused ref_parent field from the tactic_arg (as well as related
      fields from related data structures).
      

Changes  Path
+6 -3 metaprl/filter/base/filter_magic.ml
+0 -34 metaprl/tactics/proof/proof_boot.ml
+25 -93 metaprl/tactics/proof/proof_term_boot.ml
+0 -14 metaprl/tactics/proof/tactic_boot.ml
+1 -13 metaprl/tactics/proof/tactic_boot_sig.ml