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 /printing | |
| 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 'printing')
| -rw-r--r-- | printing/printer.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index bb54f587fd..18d6bcb3f1 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -281,7 +281,7 @@ let pr_compacted_decl env sigma decl = ids, mt (), typ | CompactedDecl.LocalDef (ids,c,typ) -> (* Force evaluation *) - let pb = pr_lconstr_env env sigma c in + let pb = pr_lconstr_env ~inctx:true env sigma c in let pb = if isCast c then surround pb else pb in ids, (str" := " ++ pb ++ cut ()), typ in @@ -300,7 +300,7 @@ let pr_rel_decl env sigma decl = | RelDecl.LocalAssum _ -> mt () | RelDecl.LocalDef (_,c,_) -> (* Force evaluation *) - let pb = pr_lconstr_env env sigma c in + let pb = pr_lconstr_env ~inctx:true env sigma c in let pb = if isCast c then surround pb else pb in (str":=" ++ spc () ++ pb ++ spc ()) in let ptyp = pr_ltype_env env sigma typ in |