cur
cur copied to clipboard
add universe level inference
I don't know how to do this locally. The algorithm Coq uses is a module-level constraint solver, which I disapprove of :(
yeah i agree. just remembered it was missing and couldnt find an issue for it