coq

coq copied to clipboard

I have an example at https://gist.github.com/JasonGross/8852236 (very bottom) where the unification engine churns for 3-4 seconds before deciding that terms are unifiable. I'm not sure if anything can be done about this, but I figured I'd mention it. I'll try to trim down the gist at some point; unfortunately, it's around 8000 lines right now.