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 |