diff options
author | 2017-12-05 09:56:49 +0100 | |
---|---|---|
committer | 2017-12-05 09:56:49 +0100 | |
commit | 2ae7674c6788742c021988ac02caabceec958957 (patch) | |
tree | 8f8c17a32a4a77ace1eac05760847c8c12d35670 /lib/heap.mli | |
parent | 14c041012bd375cae018f83d107c836fca3d1f01 (diff) | |
parent | 6cb9ab00a62b87587b00147d4abd82e684220b03 (diff) |
Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212
Diffstat (limited to 'lib/heap.mli')
0 files changed, 0 insertions, 0 deletions