diff options
| author | Maxime Dénès | 2017-05-03 19:02:15 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-03 19:02:15 +0200 |
| commit | 2e50976a081c8b2b8a2a8dc04320324711b04381 (patch) | |
| tree | dcdcf53469746b7de387ecbea481f66d1623ef68 | |
| parent | 3c795ba6b5728e8a0a699ab15c773c52c48f33e4 (diff) | |
| parent | dba083b267a2aede3654dcebaab0013d284d32c7 (diff) | |
Merge PR#404: patch for printing types of let bindings
| -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 483e2b4320..1eec85f455 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -695,7 +695,7 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let c = detype (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) 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 t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in + let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in GLetIn (dl, na', c, t, r) let detype_rel_context ?(lax=false) where avoid env sigma sign = |