feat: add simp option - <simproc-name>

We can now disable `simproc`s using the same notation we use to
disable rewriting rules in the simplifier.

src/Lean/Elab/Tactic/Simp.lean

@@ -168,7 +168,9 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simprocs) (eras
             thms := thms.eraseCore (.fvar fvar.fvarId!)
           else
             let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
-            if ctx.config.autoUnfold then
+            if (← Simp.isSimproc declName) then
+              simprocs := simprocs.erase declName
+            else if ctx.config.autoUnfold then
               thms := thms.eraseCore (.decl declName)
             else
               thms ← thms.erase (.decl declName)

tests/lean/run/simproc1.lean

@@ -24,3 +24,9 @@ example : x + foo 2 = 12 + x := by
   -- `simp only` does not use the default simproc set, but we can provide simprocs as arguments
   simp only [reduce_foo]
   rw [Nat.add_comm]
+
+example : x + foo 2 = 12 + x := by
+  -- We can use `-` to disable `simproc`s
+  fail_if_success simp [-reduce_foo]
+  simp
+  rw [Nat.add_comm]