| Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s
| ProofEngineHelpers.Bad_pattern msg ->
None, "Bad pattern: " ^ Lazy.force msg
| Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s
| ProofEngineHelpers.Bad_pattern msg ->
None, "Bad pattern: " ^ Lazy.force msg