Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-07-14 22:17:00 -0700 (Sat, 14 Jul 2001)
Revision: 3333
Log message:

      When eliminating a quotient hyp, dT will now use a simplier rule
      (and use thinT ThinOption). quotientT may be used instead to get
      additional equality hyps (and no thinning).
      

Changes	Path
+1 -1	metaprl/theories/itt/itt_pointwise2.prla
+17 -9	metaprl/theories/itt/itt_quotient.ml
+1 -0	metaprl/theories/itt/itt_quotient.mli
+2 -2	metaprl/theories/itt/itt_quotient.prla