diff options
| author | Pierre-Marie Pédrot | 2021-03-06 10:56:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-03-06 10:56:25 +0100 |
| commit | c738d6540ddadaa29ea6b3181f6ee462792fe9ce (patch) | |
| tree | b3fc0859ccf3d65f7993ec78936229601db82935 /pretyping/pretype_errors.ml | |
| parent | 8a61edf00c8f219fff852b70fb9c74e5d3e2aca1 (diff) | |
| parent | 220e54a9cfa4d9f5da550542a8b6ca5ab90c1698 (diff) | |
Merge PR #13902: [coercion] expose coercion_info
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions