aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-12-03 19:25:25 +0000
committerGitHub2020-12-03 19:25:25 +0000
commit632b960ada4392ddd8be6f2e49caab46b93c022f (patch)
tree68873105244017ded126a01e4e4a2eb1e0a99675 /kernel/nativelambda.mli
parentafbc39d8c4f24e2e8ccda0fcb861fb947f3f4c71 (diff)
parent6a3586d80dd068c2067a8e47effed8122d0bd3b3 (diff)
Merge PR #13558: [refman] Fix error names.
Reviewed-by: jfehrle
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions