chore: remove two mathport syntax stubs (#14693)

The `hint` and `rw_search` tactics have been implemented by now.

Author: grunweg

Mathlib/Mathport/Syntax.lean

@@ -225,9 +225,6 @@ syntax generalizingClause := " generalizing" (ppSpace ident)+
 /- E -/ syntax (name := nthRwLHS) "nth_rw_lhs " num rwRuleSeq (location)? : tactic
 /- E -/ syntax (name := nthRwRHS) "nth_rw_rhs " num rwRuleSeq (location)? : tactic
 
-/- S -/ syntax (name := rwSearch) "rw_search" (config)? rwRuleSeq : tactic
-/- S -/ syntax (name := rwSearch?) "rw_search?" (config)? rwRuleSeq : tactic
-
 /- M -/ syntax (name := piInstanceDeriveField) "pi_instance_derive_field" : tactic
 /- M -/ syntax (name := piInstance) "pi_instance" : tactic
 
@@ -267,8 +264,6 @@ syntax generalizingClause := " generalizing" (ppSpace ident)+
 
 /- N -/ syntax (name := addTacticDoc) (docComment)? "add_tactic_doc " term : command
 
-/- M -/ syntax (name := addHintTactic) "add_hint_tactic " tactic : command
-
 /- S -/ syntax (name := listUnusedDecls) "#list_unused_decls" : command
 
 /- N -/ syntax (name := defReplacer) "def_replacer " ident Parser.Term.optType : command

scripts/nolints.json

@@ -533,7 +533,6 @@
  ["docBlame", "Mathlib.Notation3.prettyPrintOpt"],
  ["docBlame", "Mathlib.Tactic.abstract"],
  ["docBlame", "Mathlib.Tactic.acMono"],
- ["docBlame", "Mathlib.Tactic.addHintTactic"],
  ["docBlame", "Mathlib.Tactic.addTacticDoc"],
  ["docBlame", "Mathlib.Tactic.applyField"],
  ["docBlame", "Mathlib.Tactic.applyNormed"],
@@ -610,8 +609,6 @@
  ["docBlame", "Mathlib.Tactic.revertTargetDeps"],
  ["docBlame", "Mathlib.Tactic.rintro?"],
  ["docBlame", "Mathlib.Tactic.rsimp"],
- ["docBlame", "Mathlib.Tactic.rwSearch"],
- ["docBlame", "Mathlib.Tactic.rwSearch?"],
  ["docBlame", "Mathlib.Tactic.safe"],
  ["docBlame", "Mathlib.Tactic.sample"],
  ["docBlame", "Mathlib.Tactic.setArgsRest"],