Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2003-11-15 06:11:03 -0800 (Sat, 15 Nov 2003)
Revision: 5103
Log message:

      Aleksey Nogin wrote:
      
      > Minor thing - why nested if's? This should be just
      >   if (i <= Sequent.hyp_count p) && (alpha_equal t (Sequent.nth_hyp p i))
      >   then raise eq_exn else idT
      
      Yes. I was not sure how && works.
      Fixed.
      

Changes  Path
+2 -3 metaprl/support/tactics/dtactic.ml