aboutsummaryrefslogtreecommitdiff
path: root/kernel/vmbytecodes.ml
diff options
context:
space:
mode:
authorHugo Herbelin2020-11-15 11:10:40 +0100
committerHugo Herbelin2020-11-19 20:43:42 +0100
commit115fe6ba6f77cabe8729cc39ec9c373c3b0173d3 (patch)
tree73081ad04d0f72f88d7bedbcd93552475bc3174e /kernel/vmbytecodes.ml
parenta27fb3c67238cc41dc24308a233a02422e0f83f3 (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/vmbytecodes.ml')
0 files changed, 0 insertions, 0 deletions