diff options
| author | coqbot-app[bot] | 2020-10-20 09:24:07 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-20 09:24:07 +0000 |
| commit | 11110938f4f3b3a570a2047b2f5e060412989e31 (patch) | |
| tree | 0d3b0abe727ae5e53c978fc19c8d7844a01046a5 /kernel/type_errors.ml | |
| parent | 48319ad16a7bff94c3bcfabb37181daa55b568c4 (diff) | |
| parent | 5da6b8c6546c2c1823592deb0bc1c64e85de0065 (diff) | |
Merge PR #13180: Respect Print Universes when printing primitive arrays
Reviewed-by: herbelin
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions