In fact, both were using `truediv`, which has been there since 2.2. I've taken this bit out.

My reading of the code around line 1015 is that it will always act on floats, in which case there's no difference between `truediv` and `div`. If both operands are Python integers, `div` does floor division, i.e. `div(1, 2) == 0`.