diff options
| author | Maxime Dénès | 2017-10-06 12:37:15 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-10-06 12:37:15 +0200 |
| commit | 3134ddd5dae8c9ab78a8aad181b2142f63907ecb (patch) | |
| tree | d31ff1ae34bc0a8fd0608ad19d545c916d0d85db /kernel/type_errors.ml | |
| parent | fb45ec112ebdf6f18143b844e317a555f14e3b74 (diff) | |
| parent | 8fa1d224dafde29f5b527d380c069f196a042c60 (diff) | |
Merge PR #1125: [pp] Minor optimization in `Pp.t` construction and gluing.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions