diff options
| author | coqbot-app[bot] | 2020-09-09 06:01:26 +0000 |
|---|---|---|
| committer | GitHub | 2020-09-09 06:01:26 +0000 |
| commit | 215d3013312309d47dae01b66b1781b572d30783 (patch) | |
| tree | 24577158ced51623fda78424ef89c4618cc2c8bb /kernel/type_errors.mli | |
| parent | 0ab3e7f16064be178e7c48aeef5252cc0d0d3109 (diff) | |
| parent | d10c7e19fe760f139f31809975291b955705dc27 (diff) | |
Merge PR #12905: Lint stdlib with -mangle-names #2
Reviewed-by: anton-trunov
Ack-by: jashug
Ack-by: olaure01
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions