Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-13 19:19:35 -0700 (Sun, 13 Jun 1999)
Revision: 2710
Log message:

      Added equalityEquality to the eqcd resource, so eqcdT and dT 0 can handle
      << ('a1 = 'b1 in 'T1) = ('a2 = 'b2 in 'T2) in univ[i:l] >>.
      
      Updated documentation.
      

Changes  Path
+12 -4 metaprl/doc/itt_quickref.txt
+3 -0 metaprl/theories/itt/itt_equal.ml