diff options
| author | Hugo Herbelin | 2016-07-31 07:57:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-08-17 10:32:55 +0200 |
| commit | 979b7cbba63f6c033bab40ad5c552572ab5d7d71 (patch) | |
| tree | 0e81c375b96b6ab2e1e054a63ae05afdcd3b9f8c /pretyping | |
| 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 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) |