Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-24 22:14:42 -0700 (Wed, 24 May 2000)
Revision: 2985
Log message:

      Merged the unify_mm branch.
      

Changes	Path
+3 -7	metaprl/BUGS
+1 -3	metaprl/editor/ml/shell.ml
+1 -1	metaprl/filter/boot/tactic_boot.ml
+3 -3	metaprl/filter/boot/tactic_boot_sig.mlz
+3 -2	metaprl/refiner/reflib/jall.ml
+19 -26	metaprl/refiner/refsig/term_subst_sig.ml
+1 -1	metaprl/refiner/term_ds/term_base_ds.ml
+0 -1	metaprl/refiner/term_ds/term_base_ds.mli
+1 -9	metaprl/refiner/term_ds/term_ds.ml
+3 -4	metaprl/refiner/term_ds/term_ds_sig.ml
+2 -1	metaprl/refiner/term_ds/term_eval_ds.ml
+1 -0	metaprl/refiner/term_ds/term_op_ds.ml
+14 -169	metaprl/refiner/term_ds/term_subst_ds.ml
+0 -1	metaprl/refiner/term_ds/term_subst_ds.mli
+435 -501	metaprl/refiner/term_ds/term_unif_ds.ml
+68 -223	metaprl/refiner/term_ds/term_unif_ds.mli
+18 -169	metaprl/refiner/term_std/term_subst_std.ml
+5 -3	metaprl/theories/base/typeinf.ml
+2 -2	metaprl/theories/base/typeinf.mli
+1 -1	metaprl/theories/itt/itt_dfun.ml
+3 -3	metaprl/theories/itt/itt_dprod.ml
+1 -1	metaprl/theories/itt/itt_isect.ml
+6 -6	metaprl/theories/itt/itt_list.ml
+1 -1	metaprl/theories/itt/itt_logic.ml
+2 -2	metaprl/theories/itt/itt_prec.ml
+1 -1	metaprl/theories/itt/itt_quotient.ml
+7 -6	metaprl/theories/itt/itt_rfun.ml
+1 -1	metaprl/theories/itt/itt_set.ml
+2 -2	metaprl/theories/itt/itt_srec.ml
+6 -6	metaprl/theories/itt/itt_union.ml
+1 -1	metaprl/theories/itt/itt_w.ml
+1 -2	metaprl/theories/tptp/tptp_cache.ml
+23 -28	metaprl/theories/tptp/tptp_prove.ml
Deleted	metaprl/theories/tptp/tptp_prove1.ml
Deleted	metaprl/theories/tptp/tptp_prove1.mli