delete mathport syntax when porting?

Stream: mathlib4

[Thomas Murrills]

I just want to confirm: when we port a tactic and move tactic syntax from Syntax.lean, do we also delete that syntax from Syntax.lean?

(If so, somehow I've missed that part of the procedure this whole time...whoops :upside_down:)

[Thomas Murrills]

Ok, judging by past PR's, I think I know the answer...

[Moritz Doll]

You are also supposed to import your tactic at the top of Syntax.lean, so you would get an error if you don't delete the syntax in the file.

[Thomas Murrills]

Fixed a couple: !4#2343