Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-05-05 16:57:47 -0700 (Fri, 05 May 2000)
Revision: 2955
Log message:

      Changed the typeinf tactic to use MM unification. Now this branch will compile.
      

Changes	Path
+1 -0	metaprl-branches/unify_mm/refiner/refsig/term_subst_sig.ml
+1 -0	metaprl-branches/unify_mm/refiner/term_ds/term_subst_ds.ml
+1 -0	metaprl-branches/unify_mm/refiner/term_ds/term_unif_ds.ml
+1 -0	metaprl-branches/unify_mm/refiner/term_ds/term_unif_ds.mli
+2 -1	metaprl-branches/unify_mm/refiner/term_std/term_subst_std.ml
+1 -1	metaprl-branches/unify_mm/theories/itt/itt_dfun.ml
+3 -3	metaprl-branches/unify_mm/theories/itt/itt_dprod.ml
+1 -1	metaprl-branches/unify_mm/theories/itt/itt_isect.ml
+6 -6	metaprl-branches/unify_mm/theories/itt/itt_list.ml
+1 -1	metaprl-branches/unify_mm/theories/itt/itt_logic.ml
+2 -2	metaprl-branches/unify_mm/theories/itt/itt_prec.ml
+1 -1	metaprl-branches/unify_mm/theories/itt/itt_quotient.ml
+4 -4	metaprl-branches/unify_mm/theories/itt/itt_rfun.ml
+1 -1	metaprl-branches/unify_mm/theories/itt/itt_set.ml
+2 -2	metaprl-branches/unify_mm/theories/itt/itt_srec.ml
+2 -2	metaprl-branches/unify_mm/theories/itt/itt_union.ml
+1 -1	metaprl-branches/unify_mm/theories/itt/itt_w.ml