aboutsummaryrefslogtreecommitdiff
path: root/kernel/section.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2021-01-06 13:04:20 +0000
committerGitHub2021-01-06 13:04:20 +0000
commit30f497eaf34f2cf641c3fe854fc9066ae19eea67 (patch)
tree473734cdc4ea6769de9a5563a0e9e6eeb56dce20 /kernel/section.ml
parent960178db193c8a78b9414abad13536693ee5b9b8 (diff)
parenta95654a21c350f19ad0da67713359cbf6c49e95a (diff)
Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)
Reviewed-by: mattam82 Reviewed-by: SkySkimmer Ack-by: gares Ack-by: jfehrle
Diffstat (limited to 'kernel/section.ml')
0 files changed, 0 insertions, 0 deletions