fname
| ProofEngineTypes.Fail msg -> None, "Tactic error: " ^ Lazy.force msg
| Continuationals.Error s -> None, "Tactical error: " ^ Lazy.force s
+ | CicRefine.RefineFailure msg ->
+ None, "Refiner error: " ^ Lazy.force msg
| CicTypeChecker.TypeCheckerFailure msg ->
None, "Type checking error: " ^ Lazy.force msg
| CicTypeChecker.AssertFailure msg ->
None, "Type checking assertion failed: " ^ Lazy.force msg
| LibrarySync.AlreadyDefined s ->
None, "Already defined: " ^ UriManager.string_of_uri s
+ | CoercDb.EqCarrNotImplemented msg ->
+ None, ("EqCarrNotImplemented: " ^ Lazy.force msg)
| GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
let rec aux n ?(dummy=false) (prev_msg,phases) =
function
| phase::tl ->
let msg =
String.concat "\n\n\n"
- (List.map (fun (floc,msg) ->
+ (List.map (fun (_,_,floc,msg) ->
let loc_descr =
match floc with
None -> ""
(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