diff options
| author | Jasper Hugunin | 2018-10-25 13:58:03 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2018-11-08 17:20:31 -0800 |
| commit | 46f6b27f9808848556f88032cb2af0a8a9f6c017 (patch) | |
| tree | 22ef5639425cac0944be9b49ef6a990bcd9f82d3 /plugins/extraction/ExtrHaskellString.v | |
| parent | 31825dc11a8e7fea42702182a3015067b0ed1140 (diff) | |
Standardize handling of Automatic Introduction.
This fixes #8791.
We explicitly specify for intro the names of binders which are
given by the user. This still can suffer from spurious collisions,
see #8819.
Diffstat (limited to 'plugins/extraction/ExtrHaskellString.v')
0 files changed, 0 insertions, 0 deletions