diff options
| author | Emilio Jesus Gallego Arias | 2020-07-20 16:11:35 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-20 18:15:08 +0200 |
| commit | 708869a116102fb29baa9379c103999f2e8e2dc2 (patch) | |
| tree | 61e6742c4aaa0caf69f2957c416d8fdeec462a6c /dev | |
| parent | f44202e28f38aa900801b0c90514690b6a401bed (diff) | |
[declare] Remove some dead code in declare_mutual_definition
This is a leftover after the unification of constant information,
`kind` is now correctly set by the single caller of
`Obls.add_mutual_definitions`.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions