diff options
Diffstat (limited to 'vernac/explainErr.ml')
| -rw-r--r-- | vernac/explainErr.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 04841c922..040c86805 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -117,8 +117,9 @@ let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) = try Some (CList.find_map (fun f -> f e) !additional_error_info) with _ -> None in + let add_loc_opt ?loc info = Option.cata (fun l -> Loc.add_loc info l) info loc in match e' with | None -> e - | Some (None, loc) -> (fst e, Loc.add_loc (snd e) loc) - | Some (Some msg, loc) -> - (EvaluatedError (msg, Some (fst e)), Loc.add_loc (snd e) loc) + | Some (loc, None) -> (fst e, add_loc_opt ?loc (snd e)) + | Some (loc, Some msg) -> + (EvaluatedError (msg, Some (fst e)), add_loc_opt ?loc (snd e)) |