diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-31 07:57:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-17 10:32:55 +0200 |
| commit | 979b7cbba63f6c033bab40ad5c552572ab5d7d71 (patch) | |
| tree | 0e81c375b96b6ab2e1e054a63ae05afdcd3b9f8c /engine/evd.ml | |
| parent | 5cd253c4d8e046d7eac108b48be2d510c114a49a (diff) | |
Two protections against failures when printing evar_map.
Delimit the scope of the failure to ease potential need for debugging
the debugging printer.
Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
Diffstat (limited to 'engine/evd.ml')
| -rw-r--r-- | engine/evd.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/engine/evd.ml b/engine/evd.ml index e4b174bcb..6ba8a5112 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"]" |