diff options
| author | Gaëtan Gilbert | 2018-10-19 20:56:01 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-11-16 14:56:16 +0100 |
| commit | 86bf9da9ef88a0bc82f9d0527b01e424851f4f61 (patch) | |
| tree | e85b26e67b2f2584a58aab73e5582a6e738b1319 /dev/tools/github-check-prs.py | |
| parent | 778213b89d893b55e572fc1813c7209d647ed6b0 (diff) | |
Heads: simplify using that projections are always rigid
This avoids using Projection.constant in kind_of_head, which then
allows compute_head to not check whether the constant is a
compatibility definition (as in that case its body is [fun ... => x.(p)]).
Thus Heads stops caring about the compatibility projection system.
Diffstat (limited to 'dev/tools/github-check-prs.py')
0 files changed, 0 insertions, 0 deletions