refactor: generalize addMatcherInfo (#5068)

works in any `MonadEnv`.
leanprover · Aug 16, 2024 · 53e6e99 · 53e6e99
1 parent 59ca274
commit 53e6e99
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean
@@ -92,7 +92,7 @@ def getMatcherInfo? (env : Environment) (declName : Name) : Option MatcherInfo :
 
 end Extension
 
-def addMatcherInfo (matcherName : Name) (info : MatcherInfo) : MetaM Unit :=
+def addMatcherInfo [Monad m] [MonadEnv m] (matcherName : Name) (info : MatcherInfo) : m Unit :=
   modifyEnv fun env => Extension.addMatcherInfo env matcherName info
 
 end Match