diff options
| author | Hugo Herbelin | 2019-11-18 16:27:15 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-08 18:23:53 +0100 |
| commit | d696eb98189eccdc2f6adb851e54af37e7f8d83b (patch) | |
| tree | d7ab5a496defc1004cb851cceb46664d34ca0e46 /vernac | |
| parent | 756d2f4db5eae51c8c01a40550b8c4553bd30f53 (diff) | |
When printing term together with its type, use info that term is in context.
This governs the printing of the explicitation of implicit arguments
and the removal of coercions.
E.g., "Check coe foo." where coe is a coercion with codomain B will show:
foo
: B
instead of
coe foo
: B
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/prettyp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml index ea49cae9db..fdf999b5b8 100644 --- a/vernac/prettyp.ml +++ b/vernac/prettyp.ml @@ -545,7 +545,7 @@ let print_located_qualid ref = print_located_qualid "object" LocAny ref (**** Gallina layer *****) let gallina_print_typed_value_in_env env sigma (trm,typ) = - (pr_leconstr_env env sigma trm ++ fnl () ++ + (pr_leconstr_env ~inctx:true env sigma trm ++ fnl () ++ str " : " ++ pr_letype_env env sigma typ) (* To be improved; the type should be used to provide the types in the @@ -554,7 +554,7 @@ let gallina_print_typed_value_in_env env sigma (trm,typ) = synthesizes the type nat of the abstraction on u *) let print_named_def env sigma name body typ = - let pbody = pr_lconstr_env env sigma body in + let pbody = pr_lconstr_env ~inctx:true env sigma body in let ptyp = pr_ltype_env env sigma typ in let pbody = if Constr.isCast body then surround pbody else pbody in (str "*** [" ++ str name ++ str " " ++ @@ -596,7 +596,7 @@ let gallina_print_section_variable env sigma id = with_line_skip (print_name_infos (GlobRef.VarRef id)) let print_body env evd = function - | Some c -> pr_lconstr_env env evd c + | Some c -> pr_lconstr_env ~inctx:true env evd c | None -> (str"<no body>") let print_typed_body env evd (val_0,typ) = |