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 |