diff options
| author | Hugo Herbelin | 2020-10-16 22:15:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 15:45:36 +0100 |
| commit | cf4105502388e437c1cf361b5c3ddd8a482eef04 (patch) | |
| tree | 4ac4a1ad1c52b6ae793ba762c350edca3c7b0df7 /kernel/kernel.mllib | |
| parent | fb186f25abeb0565bb6e238345f0c5147b697322 (diff) | |
Suggesting to use injection when an injection pattern is given to destruct.
This hopefully clarifies the confusing role of destruct (see #13205).
Diffstat (limited to 'kernel/kernel.mllib')
0 files changed, 0 insertions, 0 deletions