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
| phase::tl ->
let msg =
String.concat "\n\n\n"
- (List.map (fun (floc,msg) ->
+ (List.map (fun (_,_,floc,msg,significant) ->
let loc_descr =
match floc with
None -> ""
let (x, y) = HExtlib.loc_of_floc floc in
sprintf " at %d-%d" (x+offset) (y+offset)
in
- "*Error" ^ loc_descr ^ ": " ^ Lazy.force msg) phase)
+ "*" ^ (if not significant then "(Ignorable) " else "")
+ ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg) phase)
in
if msg = prev_msg then
aux (n+1) (msg,phases@[n]) tl
(aux (n+1) (msg,[n]) tl) in
let loc =
match errorll with
- ((Some floc,_)::_)::_ ->
+ ((_,_,Some floc,_,_)::_)::_ ->
let (x, y) = HExtlib.loc_of_floc floc in
let x = x + offset in
let y = y + offset in