chore: remove ported tactic from Mathport syntax (#14385)

`move_add`, `move_mul` and `move_oper` are all available in `Mathlib`.
leanprover-community · Jul 3, 2024 · 343699a · 343699a
1 parent e6737c3
commit 343699a
Showing 1 changed file with 0 additions and 6 deletions.
diff --git a/Mathlib/Mathport/Syntax.lean b/Mathlib/Mathport/Syntax.lean
@@ -253,12 +253,6 @@ syntax generalizingClause := " generalizing" (ppSpace ident)+
 
 /- E -/ syntax (name := wittTruncateFunTac) "witt_truncate_fun_tac" : tactic
 
-/- M -/ syntax (name := moveOp) "move_op " term:max ppSpace rwRule,+ (location)? : tactic
-macro (name := moveMul) "move_mul " pats:rwRule,+ loc:(location)? : tactic =>
-  `(tactic| move_op (·*·) $pats,* $(loc)?)
-macro (name := moveAdd) "move_add " pats:rwRule,+ loc:(location)? : tactic =>
-  `(tactic| move_op (·+·) $pats,* $(loc)?)
-
 /- S -/ syntax (name := intro) "intro" : attr
 /- S -/ syntax (name := intro!) "intro!" : attr