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
let (x, y) = HExtlib.loc_of_floc floc in
let x = x + offset in
let y = y + offset in
- let flocb,floce = floc in
- let floc =
- {flocb with Lexing.pos_cnum = x}, {floce with Lexing.pos_cnum = y}
- in
+ let floc = HExtlib.floc_of_loc (x,y) in
Some floc
| _ -> None in
let rec explain =