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