aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2018-10-11 14:33:29 +0200
committerThéo Zimmermann2018-10-11 14:33:29 +0200
commit12527ad84e9d06a124086b1d184f56eff2772b9c (patch)
treeaa5097b0fc8747c92b725a31b0ab108262747306 /kernel/nativelambda.ml
parentaa5cdbd67b160417fe353a79393a89ed99481548 (diff)
parentba88c14957640e07e7605841ef122b89f2f93bda (diff)
Merge PR #8648: Add minimal CHANGES entry about deprecated compat notations
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions