aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/top_printers.ml2
1 files changed, 1 insertions, 1 deletions
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)