fb135b8cfe
Currently this will fail in two tests, because of changes in #3965. * Sometimes we need to add an additional universe annotation, or we get a `stuck at solving universe constraint max u ?u =?= u`. * Sometimes we need to specify arguments that could previously be found by unification. --------- Co-authored-by: Leonardo de Moura <leomoura@amazon.com> |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lean-toolchain | ||