diff options
| author | Emilio Jesus Gallego Arias | 2017-05-15 02:25:52 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-05-15 04:51:10 +0200 |
| commit | e4ca8679e6700cfd6563890eb7d9e4ee59bede57 (patch) | |
| tree | af0e67b043fa3b6bab1cf29ca69f17f1dbd31dd5 /interp/notation.ml | |
| parent | b643916aed4093eb7f21116aaef726cab561bc27 (diff) | |
[interp] Rework check for casts inside patterns.
1969e10f25df0c913600099b7b98ea273a064017 introduced a check so a cast
in a pattern is not a fatal error.
We move this check to the internalization function, which is the
logical place to raise it, removing a bit boilerplate code.
Diffstat (limited to 'interp/notation.ml')
0 files changed, 0 insertions, 0 deletions