diff options
| author | coqbot-app[bot] | 2020-11-16 16:24:02 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 16:24:02 +0000 |
| commit | a400dbf104ea3bf0fef51a62e774fb4ff60a7397 (patch) | |
| tree | 296319fab9b42a4ad2c67e879de777996ecc26b5 /kernel/float64_common.ml | |
| parent | 58b24bdf4393d5522df63d31b2adc9eb08c417d8 (diff) | |
| parent | cf4105502388e437c1cf361b5c3ddd8a482eef04 (diff) | |
Merge PR #13212: Suggesting to use injection when an injection pattern is given to destruct (wish #13205)
Reviewed-by: gares
Ack-by: Blaisorblade
Ack-by: RalfJung
Diffstat (limited to 'kernel/float64_common.ml')
0 files changed, 0 insertions, 0 deletions