diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-08-31 17:40:28 +0200 |
|---|---|---|
| committer |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-03 13:39:18 +0200 |
| commit | 6ba75b01a7e39f48a325b04fd891939927b981da (patch) | |
| tree | 3725d6f85e58a5d5b5707607ca3727030fd87434 /checker | |
| parent | c11bd7b181d6e53910dc8d39c5360f35c7b24674 (diff) | |
Term_typing: remove unused argument to internal function.
The function is defined with a typo but called with the same env that
is mistakenly not shadowed.
An alternative to this commit would be to fix the typo.
Diffstat (limited to 'checker')
0 files changed, 0 insertions, 0 deletions