diff options
| author | Gaëtan Gilbert | 2020-02-06 20:22:13 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | b8fb594259f7abaedc4e335cfd8eacd0508fffcf (patch) | |
| tree | 672557a7dda635f9318e24dff1dc64eda044648a /dev/core.dbg | |
| parent | 791797fce5e11b83b88e6b869678ee7c39703043 (diff) | |
unsafe_type_of -> type_of in Rewrite.build_morphism_signature
Diffstat (limited to 'dev/core.dbg')
0 files changed, 0 insertions, 0 deletions