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