Changes by: Carl Witty (cwitty at newtonlabs.com)
Date: 1999-06-13 18:14:10 -0700 (Sun, 13 Jun 1999)
Revision: 2709
Log message:

      Changed the behavior of the dT and eqcdT tactics on goals with
      conclusions of the form
      << (quot x1, y1: 'A1 // 'E1['x; 'y]) =
         (quot x2, y2: 'A2 // 'E2['x1; 'x2]) in univ[@i:l] >>
      (to use the quotientWeakEquality rule instead of the quotientEquality
      rule).  The old behavior is recovered with altT.
      
      I would be very surprised if this broke any proofs; the original
      tactic created subgoals of the same form as the current goal, and I
      don't think there's any way to prove those subgoals.
      

Changes	Path
+8 -5	metaprl/theories/itt/itt_quotient.ml