diff options
| author | Pierre-Marie Pédrot | 2019-05-16 22:32:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-24 09:00:10 +0200 |
| commit | 26169d33b45aae8bf2dfafa2b400a9780c73ea13 (patch) | |
| tree | d5d6e1b70c52cc2d833f7d6576e743f272e7ee90 /lib | |
| parent | f6aeed0b7de9581200749f9ded48360540ce8471 (diff) | |
Remove a last use of opacity-piercing function in Safe_typing.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions