fix: Tactic.orelse was using the wrong try ... catch ...

This commit is contained in:
Leonardo de Moura 2020-11-03 15:09:10 -08:00
parent bfba03c6e1
commit 27c495c198

View file

@ -51,15 +51,15 @@ def BacktrackableState.restore (b : BacktrackableState) : TacticM Unit := do
let b ← saveBacktrackableState
try x catch ex => b.restore; h ex
@[inline] protected def orelse {α} (x y : TacticM α) : TacticM α := do
try x catch _ => y
instance : MonadExcept Exception TacticM := {
throw := throw,
tryCatch := Tactic.tryCatch
}
instance {α} : OrElse (TacticM α) := ⟨Tactic.orelse⟩
@[inline] protected def orElse {α} (x y : TacticM α) : TacticM α := do
try x catch _ => y
instance {α} : OrElse (TacticM α) := ⟨Tactic.orElse⟩
structure SavedState :=
(core : Core.State)