diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-10-24 17:53:42 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-10-27 10:12:55 +0200 |
| commit | 6ecb796d462896a19212bcc5b8c0036833c6c85f (patch) | |
| tree | 8db7a5281797c86f8333a3c0e683b7bf6f9c0a40 /test-suite/output/Tactics.out | |
| parent | 5da679d276e106a62cc3368ceb7358da289ea10a (diff) | |
Proper fix for #3753 (anomaly with implicit arguments and renamings)
Instead of circumventing the problem on the caller's side, as was done
in Arguments, we simply avoid failing as there was no real reason for
this anomaly to be triggered. If the list of renamings is shorter than
the one of implicits, we simply interpret the remaining arguments as not
renamed.
Diffstat (limited to 'test-suite/output/Tactics.out')
0 files changed, 0 insertions, 0 deletions