PR !4#13010: feat: relax universe constraint is stoneCech...

Stream: triage

[Random Issue Bot]

Today I chose PR 13010 for discussion!

feat: relax universe constraint is stoneCechExtend
Created by @Anatole Dedecker (@ADedecker) on 2024-05-18
Labels: merge-conflict

Is this PR still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

(I fixed the typo in the PR title)

[Patrick Massot]

This PR is no longer relevant as a new feature since this feature has been added in another PR in the mean time. It could be still relevant as a refactor.