diff options
| author | Hugo Herbelin | 2018-09-04 00:03:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-04 00:03:51 +0200 |
| commit | b40d68fa4fc07a9b585dbd602e94224d6b3f2a7a (patch) | |
| tree | c475991d3bec678e31b95f5b0f791e2aec6535c0 /dune | |
| parent | 8a59612e3043e8b9daa8d3723299e3d721cb492e (diff) | |
| parent | 60f396b240ce1e1a3622ecc512be62a168494efe (diff) | |
Merge PR #8263: Do not abstract over the named variable in unsafe introduction tactic.
Diffstat (limited to 'dune')
0 files changed, 0 insertions, 0 deletions