diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean index e6acb2d14f..bb2d5a3a43 100644 --- a/src/Lean/Elab/GuardMsgs.lean +++ b/src/Lean/Elab/GuardMsgs.lean @@ -200,7 +200,7 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S match filterFn msg with | .check => toCheck := toCheck.add msg | .drop => pure () - | pass => toPassthrough := toPassthrough.add msg + | .pass => toPassthrough := toPassthrough.add msg let map ← getFileMap let reportPos? := if reportPositions then