aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-10-26 16:13:30 +0000
committerGitHub2020-10-26 16:13:30 +0000
commit970d9be15074e78ab2961cfe81a668cdf09ea4f4 (patch)
tree8688a81c9564d7fbacec5b2585bb612dff7329a4 /kernel/nativelambda.ml
parent9e7b0f9f248a1fae8e5681815bd621f182696c4f (diff)
parent3c73900038e904e007e0e83d53ac040dfc951fb0 (diff)
Merge PR #12768: Granting wish #12762: warning on duplicated catch-all pattern-matching clause with unused named variable
Reviewed-by: jfehrle Reviewed-by: vbgl Ack-by: gares
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions