Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-17 21:00:43 -0800 (Thu, 17 Mar 2005)
Revision: 6969
Log message:

      Changed splitITE to use TermAddr functionality for finding appropriate
      if-then-else locations, instead of using its own ad-hoc version which didn't
      play nicely with nested sequents (such as reflected bterms).
      

Changes  Path
+6 -6 metaprl/refiner/refiner/refiner_debug.ml
+2 -1 metaprl/refiner/refsig/term_addr_sig.ml
+35 -42 metaprl/refiner/term_ds/term_addr_ds.ml
+9 -16 metaprl/refiner/term_gen/term_addr_gen.ml
+14 -4 metaprl/support/tactics/dtactic.ml
+1 -0 metaprl/tactics/proof/tactic_boot_sig.ml
+17 -48 metaprl/theories/itt/itt_bool.ml
+21061 -27085 metaprl/theories/itt/itt_fset.prla
+10744 -11406 metaprl/theories/itt/itt_int_base.prla
+598 -568 metaprl/theories/itt/itt_list2.prla
+35 -7 metaprl/util/gen_refiner_debug.pl