diff options
| author | Hugo Herbelin | 2018-10-08 17:46:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-08 20:42:14 +0200 |
| commit | ab237af7e952281e3fe695d888242cdf2abcaa90 (patch) | |
| tree | bcdb9c257db9ada14dac7b5f5d43fd26eef0e1da /kernel/nativecode.mli | |
| parent | d792c2bf18e68a6301f295c79c05f25738456ecf (diff) | |
Fixes #8672 (ill-formed pattern substitution in notation with "let").
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions