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 /kernel/nativecode.mli | |
| 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 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions