diff options
author | 2017-08-11 13:20:11 +0200 | |
---|---|---|
committer | 2018-02-20 10:03:03 +0100 | |
commit | ead835b3e8c366800b8c95a28a89062abb62d807 (patch) | |
tree | 280a130d5cf54cf61c3d611e8d601d3a33e0674f /parsing/parsing.mllib | |
parent | 7ef99814a02a0eb7c37dd28fb9ce603e70501745 (diff) |
Canonically add an encoding in glob_constr of "as" operator for cases_pattern.
Diffstat (limited to 'parsing/parsing.mllib')
0 files changed, 0 insertions, 0 deletions