Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-03-23 01:19:42 -0800 (Tue, 23 Mar 2004)
Revision: 5522
Log message:

      Changed the dT back from that "full fail-through" back ot only trying the
      items with the same pattern, and fixed all the cases of autoT looping.
      

Changes  Path
+18 -0 metaprl-branches/new_match_table/refiner/reflib/term_match_table.ml
+4 -0 metaprl-branches/new_match_table/refiner/reflib/term_match_table.mli
+2 -2 metaprl-branches/new_match_table/support/tactics/auto_tactic.ml
+29 -15 metaprl-branches/new_match_table/support/tactics/dtactic.ml
+17 -0 metaprl-branches/new_match_table/theories/itt/itt_field2.ml
+5682 -19578 metaprl-branches/new_match_table/theories/itt/itt_field2.prla
+18 -3 metaprl-branches/new_match_table/theories/itt/itt_rat.ml
+9060 -11602 metaprl-branches/new_match_table/theories/itt/itt_rat.prla
+11 -26 metaprl-branches/new_match_table/theories/itt/itt_set.ml
+801 -1038 metaprl-branches/new_match_table/theories/itt/itt_set.prla