From d73bf48c107e7f3e08f2fc5777bbbd42b4e1bc7c Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Mon, 28 Jan 2013 13:54:13 +0000
Subject: Added backtrace information to anomalies

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

(limited to 'checker')

diff --git a/checker/checker.ml b/checker/checker.ml
index 1b7af51783..b3c8b0e8c9 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -238,8 +238,6 @@ let rec explain_exn = function
       hov 0 (str "Out of memory")
   | Stack_overflow ->
       hov 0 (str "Stack overflow")
-  | Anomaly (s,pps) ->
-      hov 1 (anomaly_string () ++ where s ++ pps ++ report ())
   | Match_failure(filename,pos1,pos2) ->
       hov 1 (anomaly_string () ++ str "Match failure in file " ++
 	     str (guill filename) ++ str " at line " ++ int pos1 ++
@@ -283,6 +281,8 @@ let rec explain_exn = function
 		   str ", characters " ++ int e ++ str "-" ++
 		   int (e+6) ++ str ")")) ++
 	       report ())
+  | e when is_anomaly e ->
+      print_anomaly e
   | reraise ->
       hov 0 (anomaly_string () ++ str "Uncaught exception " ++
 	       str (Printexc.to_string reraise)++report())
-- 
cgit v1.2.3