+ | DisambiguateChoices.Choice_not_found msg ->
+ None, ("Disambiguation choice not found: " ^ Lazy.force msg)
+ | MatitaEngine.EnrichedWithStatus (exn,_) ->
+ None, "EnrichedWithStatus "^snd(to_string exn)
+ | NTacStatus.Error (msg,None) ->
+ None, "NTactic error: " ^ Lazy.force msg
+ | NTacStatus.Error (msg,Some exn) ->
+ None, "NTactic error: " ^ Lazy.force msg ^ "\n" ^ snd(to_string exn)
+ | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+ let loc =
+ match errorll with
+ | ((_,_,loc_msg,_)::_)::_ ->
+ let floc, _ = Lazy.force loc_msg in
+ if floc = Stdpp.dummy_loc then None else
+ let (x, y) = HExtlib.loc_of_floc floc in
+ let x = x + offset in
+ let y = y + offset in
+ let floc = HExtlib.floc_of_loc (x,y) in
+ Some floc
+ | _ -> assert false
+ in
+ let annotated_errorll =
+ List.rev
+ (snd
+ (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res)
+ (0,[]) errorll)) in
+ let choices = compact_disambiguation_errors true annotated_errorll in
+ let errorll =
+ (List.map
+ (function (loffset,l) ->
+ List.map
+ (function
+ passes,envs_and_diffs,msg,significant ->
+ let _,env,diff = List.hd envs_and_diffs in
+ passes,env,diff,loffset,msg,significant
+ ) l
+ ) choices) in