diff options
| author | Pierre-Marie Pédrot | 2020-10-22 11:33:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-22 11:33:37 +0200 |
| commit | 7118100aafd5b65d38ef3301afcb5b3e72889d19 (patch) | |
| tree | 271fd13c449cef7eade4ca6fd25cb0be02a0935f /lib | |
| parent | 235c550896604b6b030a31fbd98eddb7237ece44 (diff) | |
| parent | 0c1265f56a46e79aac85ae2c08cd6261141b0788 (diff) | |
Merge PR #13130: setoid_rewrite: record generated name when rewriting under lambda
Reviewed-by: ppedrot
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions