Fix the loops of `simp_all` in `scalar_tac`

[sonmarcho]

The call to simp_all in scalar_tac seems to loop at times, or at least take a lot more time than expected. For this reason, we set a low number of max steps here.

Note that removing this makes some proofs fail in this file (because the maximum number of heart beats gets exceeded).