summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Arith/Scalar.lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Arith/Scalar.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 9441be86..86b2e216 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -38,7 +38,7 @@ elab "scalar_tac_preprocess" : tactic =>
-- A tactic to solve linear arithmetic goals in the presence of scalars
def scalarTac (splitGoalConjs : Bool) : Tactic.TacticM Unit := do
- intTac splitGoalConjs scalarTacExtraPreprocess
+ intTac "scalar_tac" splitGoalConjs scalarTacExtraPreprocess
elab "scalar_tac" : tactic =>
scalarTac false