diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.mllib | 2 | ||||
| -rw-r--r-- | checker/checker.ml | 7 |
2 files changed, 7 insertions, 2 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index c12b5953a1..c93051fa18 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,9 +1,9 @@ Coq_config Pp_control -Compat Flags Pp Loc +Compat Segmenttree Unicodetable Unicode diff --git a/checker/checker.ml b/checker/checker.ml index a75aed5332..976030ef5d 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -274,7 +274,12 @@ let rec explain_exn = function (* let ctx = Check.get_env() in hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error ctx e)*) - | Loc.Exc_located (loc,exc) -> + | Loc.Exc_located (loc, exc) -> + hov 0 ((if loc = Loc.ghost then (mt ()) + else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) + ++ explain_exn exc) + | Compat.Exc_located (loc, exc) -> + let loc = Compat.to_coqloc loc in hov 0 ((if loc = Loc.ghost then (mt ()) else (str"At location " ++ print_loc loc ++ str":" ++ fnl ())) ++ explain_exn exc) |