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