Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-05-19 17:56:12 -0700 (Mon, 19 May 2003)
Revision: 4614
Log message:

      Added goals of the form ... >- t1 = t2 in T --> ... >- T type to trivialT
      

Changes	Path
+9 -7	metaprl/doc/itt_quickref.txt
+1 -1	metaprl/theories/itt/itt_logic.ml
+2 -14	metaprl/theories/itt/itt_squash.ml
+0 -2	metaprl/theories/itt/itt_squash.mli
+12 -5	metaprl/theories/itt/itt_struct.ml
+1 -0	metaprl/theories/itt/itt_struct.mli