fname
| ProofEngineTypes.Fail msg -> None, "Tactic error: " ^ Lazy.force msg
| Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s
- | CicRefine.RefineFailure msg ->
+ | ProofEngineHelpers.Bad_pattern msg ->
+ None, "Bad pattern: " ^ Lazy.force msg
+ | CicRefine.RefineFailure msg
+ | CicRefine.AssertFailure msg ->
None, "Refiner error: " ^ Lazy.force msg
| CicTypeChecker.TypeCheckerFailure msg ->
None, "Type checking error: " ^ Lazy.force msg