aboutsummaryrefslogtreecommitdiff
path: root/kernel/genOpcodeFiles.ml
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-09-22 17:42:57 +0000
committerGitHub2020-09-22 17:42:57 +0000
commit46bc7d034aa57c21825371e99b25c6f86c0812d1 (patch)
tree927868586fb64c5a4c6810ea59095e99b9fd979c /kernel/genOpcodeFiles.ml
parentc3a73c5e923953efea016a81d380e58b2cccb4f9 (diff)
parent899e3cd4bba5c6ba0ec6ec60f20acf4ae507fa27 (diff)
Merge PR #12960: Fixes #9403 and #10803: missing flattening of nested applications in notations
Reviewed-by: ejgallego Ack-by: maximedenes
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions