diff options
| -rw-r--r-- | engine/evd.ml | 6 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 2 |
2 files changed, 7 insertions, 1 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"]" diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index d4066f387b..85125a502e 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -689,7 +689,7 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = | BLetIn -> let c = detype (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) - let s = Retyping.get_sort_family_of (snd env) sigma ty in + let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in let c = if s != InProp then c else GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in GLetIn (dl, na', c, r) |