diff options
| author | Maxime Dénès | 2017-11-06 13:12:46 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-06 13:12:46 +0100 |
| commit | 9805457c2f63c27a281a2b8bbbaa771e4b695f68 (patch) | |
| tree | 927703ca0b7c043026933d054b879ee34087c755 /checker/type_errors.ml | |
| parent | ca5e66889022f7ba7d3b6003aaccad3ec521e878 (diff) | |
| parent | 6304c843c01cd1cb4fcd940d74f6ddb414cb6914 (diff) | |
Merge PR #6074: Refining PR#924 (insensitivity of projection heuristics to alphabet).
Diffstat (limited to 'checker/type_errors.ml')
0 files changed, 0 insertions, 0 deletions