Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-26 00:28:10 -0800 (Thu, 26 Jan 2006)
Revision: 8611
Log message:

      - Make sure that selection options in tactic_arg do not pollute the "named
        terms" attributes on IO.
      
      - Cleaned up the .prla files that had junk in their tactic_arg attributes.
      

Changes  Path
+5 -3 metaprl/filter/base/filter_magic.ml
+2 -2 metaprl/tactics/proof/proof_boot.ml
+8 -9 metaprl/tactics/proof/tactic_boot.ml
+5637 -6949 metaprl/theories/czf/czf_itt_axioms.prla
+13676 -17752 metaprl/theories/czf/czf_itt_bool.prla
+3353 -4118 metaprl/theories/czf/czf_itt_coset.prla
+4147 -5770 metaprl/theories/czf/czf_itt_dall.prla
+3593 -4724 metaprl/theories/czf/czf_itt_dexists.prla
+9364 -11150 metaprl/theories/czf/czf_itt_eq.prla
+8140 -12019 metaprl/theories/czf/czf_itt_hom.prla
+2713 -3721 metaprl/theories/czf/czf_itt_iso.prla
+10081 -13803 metaprl/theories/czf/czf_itt_ker.prla
+3897 -5396 metaprl/theories/czf/czf_itt_member.prla
+6565 -7664 metaprl/theories/czf/czf_itt_nat.prla
+2651 -3565 metaprl/theories/czf/czf_itt_normal_subgroup.prla
+4455 -5484 metaprl/theories/czf/czf_itt_power.prla
+4903 -6474 metaprl/theories/czf/czf_itt_sep.prla
+7370 -8525 metaprl/theories/czf/czf_itt_set.prla
+3334 -4512 metaprl/theories/czf/czf_itt_set_bvd.prla
+7658 -9569 metaprl/theories/czf/czf_itt_union.prla
+1275 -1766 metaprl/theories/fol/cfol_itt_all.prla
+1704 -2242 metaprl/theories/fol/cfol_itt_and.prla
+1299 -1523 metaprl/theories/fol/fol_itt_or.prla
+2813 -3093 metaprl/theories/fol/fol_prop.prla
+4249 -6219 metaprl/theories/itt/applications/algebra/itt_field_e.prla
+6959 -6992 metaprl/theories/itt/applications/algebra/itt_grouplikeobj.prla
+3773 -3634 metaprl/theories/itt/applications/algebra/itt_ring_e.prla
+9851 -9624 metaprl/theories/itt/applications/algebra/itt_ring_uce.prla
+6441 -7607 metaprl/theories/itt/applications/algebra/itt_unitring.prla
+2852 -2845 metaprl/theories/itt/applications/datatypes/itt_bintree.prla
+4057 -5590 metaprl/theories/itt/applications/datatypes/itt_sort.prla
+3848 -7096 metaprl/theories/itt/applications/datatypes/itt_sortedtree.prla
+11540 -12003 metaprl/theories/itt/applications/supinf/itt_order.prla
+2780 -2660 metaprl/theories/itt/core/itt_bunion.prla
+5767 -6829 metaprl/theories/itt/core/itt_disect.prla
+6858 -7709 metaprl/theories/itt/core/itt_isect.prla
+1084 -1579 metaprl/theories/itt/core/itt_pointwise2.prla
+3626 -3895 metaprl/theories/itt/core/itt_prop_decide.prla
+2929 -3453 metaprl/theories/itt/core/itt_record_label.prla
+1533 -1333 metaprl/theories/itt/core/itt_record_label0.prla
+1727 -1692 metaprl/theories/itt/core/itt_struct3.prla
+4856 -5171 metaprl/theories/itt/core/itt_w.prla
+162 -177 metaprl/theories/itt/reflection/experimental/itt_hoas_lang.prla
+4406 -6441 metaprl/theories/itt/reflection/experimental/itt_hoas_relax.prla
+5826 -5809 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_bterm.prla
+2202 -2230 metaprl/theories/itt/reflection/experimental/itt_hoas_sequent_term.prla