Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-04 18:48:17 -0700 (Sun, 04 Jun 2000)
Revision: 3006
Log message:

      Define type inference types only once, not in 5 places.
      

Changes	Path
+2 -2	metaprl/filter/boot/tactic_boot.ml
+20 -6	metaprl/filter/boot/tactic_boot_sig.mlz
+1 -5	metaprl/theories/base/typeinf.ml
+8 -17	metaprl/theories/base/typeinf.mli
+2 -3	metaprl/theories/itt/itt_rfun.ml
+1 -2	metaprl/theories/itt/itt_union.ml