diff options
| author | Pierre-Marie Pédrot | 2019-04-15 13:59:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-15 13:59:18 +0200 |
| commit | 4b9119d8090e366ecd2e803ad30a9dd839bc8ec9 (patch) | |
| tree | 4ae4ee4190595b0510ff092c19a8ea21fd2ecb22 /pretyping/patternops.ml | |
| parent | 6d92ac48719a7abdcf33721c78f2c69101db5bf8 (diff) | |
| parent | e9738ee2d21a84fc946d168aeaa68b169b309fd8 (diff) | |
Merge PR #9927: Don't store closures in summary (reduction effects)
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping/patternops.ml')
0 files changed, 0 insertions, 0 deletions