cur icon indicating copy to clipboard operation
cur copied to clipboard

add universe level inference

Open stchang opened this issue 4 years ago • 2 comments

stchang avatar Jul 02 '20 16:07 stchang

I don't know how to do this locally. The algorithm Coq uses is a module-level constraint solver, which I disapprove of :(

wilbowma avatar Jul 02 '20 22:07 wilbowma

yeah i agree. just remembered it was missing and couldnt find an issue for it

stchang avatar Jul 02 '20 22:07 stchang