diff options
| author | Pierre-Marie Pédrot | 2019-09-30 11:06:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-02 00:25:13 +0200 |
| commit | 004d7aeeca9f5ae4ceb9f109fa90a87e58457680 (patch) | |
| tree | f3658039f353f0e706d33c758e5845441dd9b786 /kernel/nativelambda.mli | |
| parent | 77fd11a9f012a2878e13451e9d8a9f500c6392eb (diff) | |
Postpone the computation of relative constraints in universe unification.
Should be 1:1 equivalent to the previous code, this is semantics preserving
factorization.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions