Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-06-08 04:55:06 -0700 (Thu, 08 Jun 2000)
Revision: 3007
Log message:

      Smarter type inference algorithm capable of doing things like
      
      # ti <<lambda{x.spread{'x;u,v.it}}>>;;
      - : Refiner.Refiner.Refine.term = x:(Top X Top) --> Unit
      

Changes  Path
+4 -0 metaprl/BUGS
+18 -3 metaprl/filter/boot/tactic_boot_sig.mlz
+45 -11 metaprl/theories/base/typeinf.ml
+9 -1 metaprl/theories/base/typeinf.mli
+3 -10 metaprl/theories/itt/itt_atom.ml
+6 -8 metaprl/theories/itt/itt_bool.ml
+1 -1 metaprl/theories/itt/itt_derive.ml
+2 -10 metaprl/theories/itt/itt_dfun.ml
+25 -25 metaprl/theories/itt/itt_dprod.ml
+34 -6 metaprl/theories/itt/itt_equal.ml
+5 -0 metaprl/theories/itt/itt_equal.mli
+10 -18 metaprl/theories/itt/itt_fset.ml
+5 -13 metaprl/theories/itt/itt_fun.ml
+6 -6 metaprl/theories/itt/itt_int.ml
+2 -11 metaprl/theories/itt/itt_isect.ml
+0 -1 metaprl/theories/itt/itt_isect.mli
+2 -2 metaprl/theories/itt/itt_isect.prla
+16 -24 metaprl/theories/itt/itt_list.ml
+16 -31 metaprl/theories/itt/itt_logic.ml
+11 -6 metaprl/theories/itt/itt_prec.ml
+2 -10 metaprl/theories/itt/itt_prod.ml
+4 -6 metaprl/theories/itt/itt_quotient.ml
+29 -33 metaprl/theories/itt/itt_rfun.ml
+2 -10 metaprl/theories/itt/itt_set.ml
+3 -2 metaprl/theories/itt/itt_sort.ml
+5 -4 metaprl/theories/itt/itt_srec.ml
+3 -10 metaprl/theories/itt/itt_subtype.ml
+27 -23 metaprl/theories/itt/itt_union.ml
+4 -5 metaprl/theories/itt/itt_unit.ml
+2 -5 metaprl/theories/itt/itt_void.ml
+1 -0 metaprl/theories/itt/itt_void.mli
+8 -12 metaprl/theories/itt/itt_w.ml