The field_simp tactic can be really useful, but can also be really slow: its implementation is in need of a rewrite.
Until that has happened, some really slow field_simp calls were replaced by simp calls:
field_simp [x, y] is equivalent to simp ...; usually, this replacement itself does not provide a large speed-up, but squeezing the simp call does. (Squeezing the field_simp, i.e. replacing by the output of field_simp?, did not help much.)
This issue tracks these replacements: after field_simp has been improved, these calls should be reinstated.
The
field_simptactic can be really useful, but can also be really slow: its implementation is in need of a rewrite.Until that has happened, some really slow
field_simpcalls were replaced bysimpcalls:field_simp [x, y]is equivalent tosimp ...; usually, this replacement itself does not provide a large speed-up, but squeezing the simp call does. (Squeezing the field_simp, i.e. replacing by the output offield_simp?, did not help much.)This issue tracks these replacements: after field_simp has been improved, these calls should be reinstated.