From 179651bfda99fc80e150d77ce0eccb08d9c98522 Mon Sep 17 00:00:00 2001
From: jforest
Date: Sun, 7 Nov 2010 22:27:34 +0000
Subject: correcting a non catch error reported as an anomaly (Ploc.Exc)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13625 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/cerrors.ml | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 61c8e4874f..68483f5e24 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -81,6 +81,10 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       msg
   | EvaluatedError (msg,Some reraise) ->
       msg ++ explain_exn_default_aux anomaly_string report_fn reraise
+  | Ploc.Exc(loc,exc) -> 
+      hov 0 ((if loc = dummy_loc then (mt ())
+               else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
+               ++ explain_exn_default_aux anomaly_string report_fn exc)
   | reraise ->
       hov 0 (anomaly_string () ++ str "Uncaught exception " ++
 	       str (Printexc.to_string reraise) ++ report_fn ())
-- 
cgit v1.2.3