diff options
| author | Gaëtan Gilbert | 2019-01-17 11:44:38 +0000 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-29 17:36:23 +0200 |
| commit | af3673b08204cb4d3d6994aa3a5bd6363bfd7459 (patch) | |
| tree | 3ec79c51ea0c3879f002a26546757c60c463f05c /kernel/typeops.ml | |
| parent | 05c5c3ab8e52ebe43179975b42142f2646b0479e (diff) | |
Fix #9344, #9348: incorrect unsafe to_constr in vnorm
Diffstat (limited to 'kernel/typeops.ml')
0 files changed, 0 insertions, 0 deletions