diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:56:49 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:56:49 +0100 |
commit | 2ae7674c6788742c021988ac02caabceec958957 (patch) | |
tree | 8f8c17a32a4a77ace1eac05760847c8c12d35670 /kernel/entries.ml | |
parent | 14c041012bd375cae018f83d107c836fca3d1f01 (diff) | |
parent | 6cb9ab00a62b87587b00147d4abd82e684220b03 (diff) |
Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212
Diffstat (limited to 'kernel/entries.ml')
0 files changed, 0 insertions, 0 deletions