aboutsummaryrefslogtreecommitdiff
path: root/lib/objFile.mli
diff options
context:
space:
mode:
authorcoqbot-app[bot]2020-11-14 21:45:11 +0000
committerGitHub2020-11-14 21:45:11 +0000
commit6b7d6be8eb0b8c12804a53475e33c1489e3bc61e (patch)
tree40262a9fc8d62a2491d9e5c0f2e49d79751ebe3a /lib/objFile.mli
parent9a93f5836a5f7bab81384314ac11ff0aac7d1b7f (diff)
parent15183aafe292695c54ae234a1210c08c8e3cd378 (diff)
Merge PR #13369: Move destructuring let syntax closer to its documentation.
Reviewed-by: jfehrle
Diffstat (limited to 'lib/objFile.mli')
0 files changed, 0 insertions, 0 deletions