wilbowma/cur

add universe level inference

Opened this issue · 2 comments

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