diff options
Diffstat (limited to 'vernac/explainErr.ml')
| -rw-r--r-- | vernac/explainErr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 04841c922..ed2dd274a 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -119,6 +119,6 @@ let process_vernac_interp_error ?(allow_uncaught=true) (exc, info) = in match e' with | None -> e - | Some (None, loc) -> (fst e, Loc.add_loc (snd e) loc) - | Some (Some msg, loc) -> + | Some (loc, None) -> (fst e, Loc.add_loc (snd e) loc) + | Some (loc, Some msg) -> (EvaluatedError (msg, Some (fst e)), Loc.add_loc (snd e) loc) |