Revert "fix: elaborate linarith arguments without errToSorry"

This reverts commit 383ec12.

Author: kmill

Mathlib/Tactic/Linarith/Frontend.lean

@@ -389,13 +389,6 @@ syntax (name := nlinarith) "nlinarith" "!"? linarithArgsRest : tactic
 @[inherit_doc nlinarith] macro "nlinarith!" rest:linarithArgsRest : tactic =>
   `(tactic| nlinarith ! $rest:linarithArgsRest)
 
-/-- Elaborate `t` in a way that is suitable for linarith. -/
-def elabLinarithArg (tactic : String) (t : Term) : TacticM Expr := Term.withoutErrToSorry do
-  let (e, mvars) ← elabTermWithHoles t none `linarith (allowNaturalHoles := true)
-  unless mvars.isEmpty do
-    throwErrorAt t "Argument passed to {tactic} has metavariables:{indentD e}"
-  return e
-
 /--
 Allow elaboration of `LinarithConfig` arguments to tactics.
 -/
@@ -406,7 +399,7 @@ elab_rules : tactic
     withMainContext do commitIfNoEx do
       liftMetaFinishingTactic <|
         Linarith.linarith o.isSome
-          (← ((args.map (TSepArray.getElems)).getD {}).mapM (elabLinarithArg "linarith")).toList
+          (← ((args.map (TSepArray.getElems)).getD {}).mapM (elabTerm ·.raw none)).toList
           ((← elabLinarithConfig (mkOptionalNode cfg)).updateReducibility bang.isSome)
 
 -- TODO restore this when `add_tactic_doc` is ported
@@ -427,7 +420,7 @@ elab_rules : tactic
         [(nlinarithExtras : GlobalBranchingPreprocessor)]) }
     liftMetaFinishingTactic <|
       Linarith.linarith o.isSome
-        (← ((args.map (TSepArray.getElems)).getD {}).mapM (elabLinarithArg "nlinarith")).toList
+        (← ((args.map (TSepArray.getElems)).getD {}).mapM (elabTerm ·.raw none)).toList
         (cfg.updateReducibility bang.isSome)
 
 -- TODO restore this when `add_tactic_doc` is ported

test/linarith.lean

@@ -544,29 +544,3 @@ example (k : ℤ) (h : k < 1) (h₁ : -1 < k) : k = 0 := by
   -- linarith preprocessor to fail.
   change _ at h₁
   linarith
-
-/-- error: unknown identifier 'garbage' -/
-#guard_msgs in
-example (q : Prop) (p : ∀ (x : ℤ), q → 1 = 2) : 1 = 2 := by
-  linarith [p _ garbage]
-
-/-- error: unknown identifier 'garbage' -/
-#guard_msgs in
-example (q : Prop) (p : ∀ (x : ℤ), q → 1 = 2) : 1 = 2 := by
-  nlinarith [p _ garbage]
-
-/--
-error: Argument passed to linarith has metavariables:
-  p ?a
--/
-#guard_msgs in
-example (q : Prop) (p : ∀ (x : ℤ), 1 = 2) : 1 = 2 := by
-  linarith [p ?a]
-
-/--
-error: Argument passed to nlinarith has metavariables:
-  p ?a
--/
-#guard_msgs in
-example (q : Prop) (p : ∀ (x : ℤ), 1 = 2) : 1 = 2 := by
-  nlinarith [p ?a]