From eb2b1d56eb8f1fdcb30dcee6577d2c71e468c007 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Nov 2020 08:03:37 -0800
Subject: [PATCH] chore: argument name

---
 src/Lean/Meta/Tactic/Util.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Util.lean b/src/Lean/Meta/Tactic/Util.lean
index cb0e35f043..e00498dd93 100644
--- a/src/Lean/Meta/Tactic/Util.lean
+++ b/src/Lean/Meta/Tactic/Util.lean
@@ -26,8 +26,8 @@ def appendTagSuffix (mvarId : MVarId) (suffix : Name) : MetaM Unit := do
   let tag ← getMVarTag mvarId
   setMVarTag mvarId (appendTag tag suffix)
 
-def mkFreshExprSyntheticOpaqueMVar (type : Expr) (userName : Name := Name.anonymous) : MetaM Expr :=
-  mkFreshExprMVar type MetavarKind.syntheticOpaque userName
+def mkFreshExprSyntheticOpaqueMVar (type : Expr) (tag : Name := Name.anonymous) : MetaM Expr :=
+  mkFreshExprMVar type MetavarKind.syntheticOpaque tag
 
 def throwTacticEx {α} (tacticName : Name) (mvarId : MVarId) (msg : MessageData) (ref := Syntax.missing) : MetaM α :=
   throwError! "tactic '{tacticName}' failed, {msg}\n{MessageData.ofGoal mvarId}"