Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-08-06 18:48:31 -0700 (Thu, 06 Aug 1998)
Revision: 2420
Log message:

      Added unify_subst type to retain unification info between separate
      calls to TermSubst.unify.  This requires that type inference be modified,
      and there are still some small modifications to be made in Itt_rfun.
      We need to do some optimization in Cycle_dag and unification.
      

Changes	Path
+24 -0	metaprl/mllib/cycle_dag.ml
+4 -0	metaprl/mllib/cycle_dag.mli
+10 -1	metaprl/refiner/refsig/term_subst_sig.ml
+21 -7	metaprl/refiner/term_ds/term_subst_ds.mlp
+7 -0	metaprl/refiner/term_std/term_subst_std.mlp
+6 -6	metaprl/theories/base/typeinf.ml
+2 -2	metaprl/theories/base/typeinf.mli
+2 -1	metaprl/theories/itt/itt_dfun.ml
+3 -3	metaprl/theories/itt/itt_dprod.ml
+2 -1	metaprl/theories/itt/itt_isect.ml
+7 -2	metaprl/theories/itt/itt_list.ml
+1 -1	metaprl/theories/itt/itt_logic.ml
+3 -2	metaprl/theories/itt/itt_prec.ml
+2 -1	metaprl/theories/itt/itt_quotient.ml
+8 -5	metaprl/theories/itt/itt_rfun.ml
+2 -1	metaprl/theories/itt/itt_set.ml
+3 -2	metaprl/theories/itt/itt_srec.ml
+5 -5	metaprl/theories/itt/itt_union.ml
+2 -1	metaprl/theories/itt/itt_w.ml
+1 -1	metaprl/theories/tactic/sequent.mli
+1 -1	metaprl/theories/tactic/tactic_type.ml
+2 -2	metaprl/theories/tactic/tactic_type.mli
+40 -34	metaprl/theories/tptp/tptp_prove.ml
+1 -1	metaprl/theories/tptp/tptp_prove.mli