Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-01-28 16:26:29 -0800 (Tue, 28 Jan 2003)
Revision: 4028
Log message:

      - Moved unify_mm from Term_ds to reflib. The code didn't have anything
      that really needed access to Term_ds internal interfaces and reflib
      is a more appropriate place for code like it (a basic proof-search
      helper tool that is not a part of "trusted" system core).
      
      - Removed Rob_ds from the list of compiled files. Since it's not currently
      being used, there does not seem to be any reason to have it compiled
      (VN, do you agree?)
      
      - Added limited support for TermMan.clause_addr to Term_std (it is true
      that Term_std does not have a agenric way fo addressing a goal, but it
      doesn't mean we can not make clause_addr work for positive numbers,
      which is what it is ever used for anyway).
      

Changes  Path
+1 -1 metaprl/filter/boot/tactic_boot_sig.mlz
+1 -0 metaprl/refiner/reflib/Files
+2 -1 metaprl/refiner/reflib/jall.ml
Added metaprl/refiner/reflib/unify_mm.ml
Properties metaprl/refiner/reflib/unify_mm.ml
Added metaprl/refiner/reflib/unify_mm.mli
Properties metaprl/refiner/reflib/unify_mm.mli
+0 -41 metaprl/refiner/refsig/term_subst_sig.ml
+0 -2 metaprl/refiner/term_ds/Files
+1 -0 metaprl/refiner/term_ds/rob_ds.ml
+1 -0 metaprl/refiner/term_ds/rob_ds.mli
+0 -26 metaprl/refiner/term_ds/term_subst_ds.ml
Deleted metaprl/refiner/term_ds/term_unif_ds.ml
Deleted metaprl/refiner/term_ds/term_unif_ds.mli
+1 -1 metaprl/refiner/term_gen/term_hash.mli
+5 -2 metaprl/refiner/term_gen/term_man_gen.ml
+0 -21 metaprl/refiner/term_std/term_subst_std.ml
+4 -3 metaprl/theories/base/typeinf.ml
+1 -1 metaprl/theories/base/typeinf.mli
+1 -0 metaprl/theories/itt/itt_dprod.ml
+1 -0 metaprl/theories/itt/itt_rfun.ml
+1 -1 metaprl/theories/itt/itt_union.ml
+3 -2 metaprl/theories/tptp/tptp_prove.ml