Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-26 06:59:36 -0800 (Mon, 26 Jan 2004)
Revision: 5282
Log message:

      int_sqequalC now takes << 'a ~ 'b >> as an argument - this makes it much easier
      to specify what exactly we want to substitute.
      

Changes  Path
+1 -1 metaprl/theories/itt/itt_int_base.ml
+2797 -2870 metaprl/theories/itt/itt_int_base.prla
+746 -762 metaprl/theories/itt/itt_nat.prla
+359 -373 metaprl/theories/itt/itt_poly.prla