Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-16 19:25:34 -0700 (Wed, 16 Jul 2003)
Revision: 4753
Log message:

      - Moved the find_subterm function from DTactic to TermAddr module (where it can
      interact more nicely with sequents and SO variables)
      
      - Term quotations inside resource annotations should now be parsed correctly
      (e.g. the bound contexts should be figured based on what they are in the
      rule/rewrite statement).
      
      The top-loop now loads correctly! :-) But still raises exceptions on most
      basic things (e.g, ls) :-(
      

Changes  Path
+6 -1 metaprl-branches/bound_contexts/filter/base/filter_util.ml
+2 -0 metaprl-branches/bound_contexts/filter/base/filter_util.mli
+22 -12 metaprl-branches/bound_contexts/filter/filter/filter_parse.ml
+1 -1 metaprl-branches/bound_contexts/filter/filter/term_grammar.ml
+1 -1 metaprl-branches/bound_contexts/refiner/refiner/refiner_ds.ml
+1 -1 metaprl-branches/bound_contexts/refiner/refiner/refiner_std.ml
+1 -0 metaprl-branches/bound_contexts/refiner/refsig/term_addr_sig.ml
+1 -1 metaprl-branches/bound_contexts/refiner/refsig/term_meta_sig.ml
+58 -0 metaprl-branches/bound_contexts/refiner/term_ds/term_addr_ds.ml
+3 -0 metaprl-branches/bound_contexts/refiner/term_ds/term_addr_ds.mli
+24 -0 metaprl-branches/bound_contexts/refiner/term_gen/term_addr_gen.ml
+3 -0 metaprl-branches/bound_contexts/refiner/term_gen/term_addr_gen.mli
+1 -1 metaprl-branches/bound_contexts/refiner/term_gen/term_meta_gen.ml
+0 -22 metaprl-branches/bound_contexts/support/tactics/dtactic.ml