diff options
| author | Pierre-Marie Pédrot | 2020-04-02 23:31:39 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-09 13:35:52 +0200 |
| commit | 97939fdb603fe41c26a99a501fffa8b10bd07bbe (patch) | |
| tree | 90a696b45b3af663a8e62a7542f2846024f8a721 /kernel/nativecode.ml | |
| parent | 84cd299416a669c73a3357e42e589d32cb467e1d (diff) | |
Remove a unused computation in alias code.
The effects field of the UniqueProjection constructor was never accessed.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions