Commit 2021-05-31 21:08 bec3e595

feat(data/finset): provide the coercion finset α → Type* (#7575) There doesn't seem to be a good reason that finset doesn't have a coe_to_sort like set does. Before the change in this PR, we had to suffer the inconvenience of writing (↑s : set _) whenever we want the subtype of all elements of s. Now you can just write s. I removed the obvious instances of the ((↑s : set _) : Type*) pattern, although it definitely remains in some places. I'd rather do those in separate PRs since it does not really do any harm except for being annoying to type. There are also some parts of the API (polynomial.root_set stands out to me) that could be designed around the use of finsets rather than sets that are later proved to be finite, which I again would like to declare out of scope.