diff options
| author | Gaëtan Gilbert | 2020-08-27 11:12:14 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-09-30 11:37:03 +0200 |
| commit | 0fa5751429e92f6555e9cbe3e3509fec658b879c (patch) | |
| tree | 4993e6fdc0714e8f353a421e56709e89f52af27b /kernel/type_errors.mli | |
| parent | 2c802aaf74c83274ae922c59081c01bfc267d31b (diff) | |
interp_context_evars: removed unused [shift] argument
Became unused in e034b4090ca45410853db60ae2a5d2f220b48792
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions