From d46ed1de8e9c928eed1121ae77bd308ecb88205b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 7 Nov 2010 23:35:56 +0000
Subject: Delayed the evar normalization in error messages to the last minute
 before the message is delivered to the user. Should avoid useless computation
 in heavily backtracking tactics (auto, try, ...).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13628 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/top_printers.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7b1fba0110..7af0a357ab 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -57,7 +57,7 @@ let ppsconstr x = ppconstr (Declarations.force x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let pprawconstr = (fun x -> pp(pr_lrawconstr x))
 let pppattern = (fun x -> pp(pr_constr_pattern x))
-let pptype = (fun x -> pp(pr_ltype x))
+let pptype = (fun x -> try pp(pr_ltype x) with e -> pp (str (Printexc.to_string e)))
 
 let ppfconstr c = ppconstr (Closure.term_of_fconstr c)
 
-- 
cgit v1.2.3