From 53e6e99a29362bc8069330f2bf045a10c8f65912 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Fri, 16 Aug 2024 08:24:32 +0200 Subject: [PATCH] refactor: generalize addMatcherInfo (#5068) works in any `MonadEnv`. --- src/Lean/Meta/Match/MatcherInfo.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean index d21e1ae66d40..360bdbeb775a 100644 --- 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