diff options
| author | Gaëtan Gilbert | 2020-09-30 12:32:31 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-06 12:40:35 +0200 |
| commit | 661d84228fa1a6750b4a80f41c3e012e6de763bf (patch) | |
| tree | 0f0e9dba77310071bcc51c92c92d99dd6f3c9239 /dev | |
| parent | c8c1723747c7e0eb748861cc12aecca411848f4c (diff) | |
Simplify Implicit_quantifiers.combine_params a bit
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions