Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-04-24 19:57:22 -0700 (Sat, 24 Apr 2004)
Revision: 5717
Log message:

      Enabled rwh to go through sequent-term.
      Basically I've copied sequent case from apply_fun_higher_term to
      apply_var_fun_higher_term,
      copied apply_fun_higher_hyps to apply_var_fun_higher_hyps
      and there I add hyp and context names to the list of bound variables
      for the rest the sequent (not including current hyp/context).
      I didn't really test it but tried in CIC theory.
      

Changes	Path
+20 -1	metaprl/refiner/term_ds/term_addr_ds.ml