diff options
| author | Gaëtan Gilbert | 2020-02-06 20:25:10 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 6283c94c640d6b1f911b644583ee656a7a8b9a1f (patch) | |
| tree | 9d1c95a5b38fd6485bc8d8f9de2f2b30a8f542a0 /plugins/syntax/plugin_base.dune | |
| parent | b8fb594259f7abaedc4e335cfd8eacd0508fffcf (diff) | |
unsafe_type_of -> get_type_of in Rewrite.default_morphism
Diffstat (limited to 'plugins/syntax/plugin_base.dune')
0 files changed, 0 insertions, 0 deletions