diff options
| author | Hugo Herbelin | 2020-11-15 11:10:40 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-19 20:43:42 +0100 |
| commit | 115fe6ba6f77cabe8729cc39ec9c373c3b0173d3 (patch) | |
| tree | 73081ad04d0f72f88d7bedbcd93552475bc3174e /kernel/nativelambda.mli | |
| parent | a27fb3c67238cc41dc24308a233a02422e0f83f3 (diff) | |
Use a proper canonical structure entry for projections.
This is to make more explicit that arguments of the projection are not
kept.
We seize this opportunity to use QGlobRef equality on GlobRef.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions