aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evd.ml6
1 files changed, 6 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml
index e4b174bcb3..6ba8a51120 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1258,6 +1258,12 @@ let pr_instance_status (sc,typ) =
| TypeProcessed -> str " [type is checked]"
end
+let protect f x =
+ try f x
+ with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
+
+let print_constr a = protect print_constr a
+
let pr_meta_map mmap =
let pr_name = function
Name id -> str"[" ++ pr_id id ++ str"]"