From bdd0eae625b0cfcf66d2c7b87d958ec52abc8f1c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 30 Dec 2020 20:20:57 -0800
Subject: [PATCH] chore: missing `)` in trace message

---
 src/Lean/Meta/Tactic/Subst.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Subst.lean b/src/Lean/Meta/Tactic/Subst.lean
index 6c07ef1f56..f6c7472d77 100644
--- a/src/Lean/Meta/Tactic/Subst.lean
+++ b/src/Lean/Meta/Tactic/Subst.lean
@@ -29,7 +29,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
       match a with
       | Expr.fvar aFVarId _ => do
         let aFVarIdOriginal := aFVarId
-        trace[Meta.Tactic.subst]! "substituting {a} (id: {aFVarId} with {b}"
+        trace[Meta.Tactic.subst]! "substituting {a} (id: {aFVarId}) with {b}"
         let mctx ← getMCtx
         if mctx.exprDependsOn b aFVarId then
           throwTacticEx `subst mvarId m!"'{a}' occurs at{indentExpr b}"