diff options
| author | Pierre Courtieu | 2017-05-03 11:37:08 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2017-05-03 18:50:04 +0200 |
| commit | 952e9aea47d3fad2d0f488d968ff0e90fa403ebc (patch) | |
| tree | 28abee0a59949e89a15e748a014a331af04fdf75 /kernel/type_errors.mli | |
| parent | 3c795ba6b5728e8a0a699ab15c773c52c48f33e4 (diff) | |
Adding an even more compact mode for goal display.
We want to print variables in vertical boxes as much as possible.
The criterion to distinguish "variable" from "hypothesis" is not
obvious. We chose this one but may change it in the future:
X:T is a variable if T is not of type Prop AND T is "simple" which
means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall
Ti:Type, but not Ti:nat).
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions