Skip to content

Commit 57ec56d

Browse files
committed
fix(Tactic/FunProp): use correct trace class name (#30514)
1 parent 1572925 commit 57ec56d

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/Tactic/FunProp/Decl.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -80,7 +80,7 @@ def addFunPropDecl (declName : Name) : MetaM Unit := do
8080

8181
modifyEnv fun env => funPropDeclsExt.addEntry env decl
8282

83-
trace[Meta.Tactic.funProp.attr]
83+
trace[Meta.Tactic.fun_prop.attr]
8484
"added new function property `{declName}`\nlook up pattern is `{path}`"
8585

8686

0 commit comments

Comments
 (0)