aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativevalues.ml
diff options
context:
space:
mode:
authorThéo Zimmermann2019-05-22 17:37:13 +0200
committerThéo Zimmermann2019-05-22 17:37:13 +0200
commited7d118e8ee9a6725daafde31845981f5da8d2b4 (patch)
treeda08f806e3de0ababeae38276cef6ce26e41ce51 /kernel/nativevalues.ml
parent2744d61704e2fdd96bdc2c60c9d7f7af8367f4d4 (diff)
parentb7af4ae98cdb0ea2ff421d4ebf19dc614e60d575 (diff)
Merge PR #10178: Improve doc for generalizing binders
Reviewed-by: Zimmi48
Diffstat (limited to 'kernel/nativevalues.ml')
0 files changed, 0 insertions, 0 deletions