5e952598dc
This PR fixes (1) an issue where private names are not unresolved when they are pretty printed, (2) an issue where in `pp.universes` mode names were allowed to shadow local names, (3) an issue where in `match` patterns constants shadowing locals wouldn't use `_root_`, and (4) an issue where tactics might have an incorrect "try this" when `pp.fullNames` is set. Adds more delaboration tests for name unresolution. It also cleans up the `delabConst` delaborator so that it uses `unresolveNameGlobalAvoidingLocals`, rather than doing any local context analysis itself. The `inPattern` logic has been removed; it was a heuristic added back in #575, but it now leads to incorrect results (and in `match` patterns, local names shadow constants in name resolution). |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||