diff --git a/src/Init/Lean/Meta/Tactic/Util.lean b/src/Init/Lean/Meta/Tactic/Util.lean index 154eacfb25..404f93afe4 100644 --- a/src/Init/Lean/Meta/Tactic/Util.lean +++ b/src/Init/Lean/Meta/Tactic/Util.lean @@ -37,7 +37,7 @@ mctx ← getMCtx; opts ← getOptions; pure $ ppGoal env mctx opts mvarId -@[inline] protected def orelse{α} (x y : MetaM α) : MetaM α := do +@[inline] protected def orelse {α} (x y : MetaM α) : MetaM α := do s ← get; catch x (fun _ => do restore s.env s.mctx s.postponed; y) instance Meta.hasOrelse {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩