Spent a good chunk of yesterday and today trying to hunt down a bug in our theorem prover that showed up since the deadline passed. I found the cause -- it's in contraction again: the scope of quantification of the evars isn't extending correctly to the noncontracted hypotheses -- but I haven't been able to fix it yet.
Advisor meeting went okay, talked about random things.
I spent a couple hours getting consumed by tom7's game escape, designing a level for it, Laser Paranoia. One is supposed to be able to register online and swap levels from within the game, but I haven't been able to get that working yet.