2012年10月22日
make clean 大事だな、きっと
- 2012-10-22 (Mon)
- 一般
Proof General で Compile Before Require のオプションを使っているのだけど，たまには rm *.vo *.glob してやったほうが良いのかもしれない．とりあえず意味不明な挙動が解消された気がする．……気がするだけかもしれない．
つか，Proof. typeclasses eauto. Qed. で証明できるのに証明が必要とかわけわからん．いまひとつ typeclass のリゾルバの挙動がつかめん．Implicit arguments の決定とのタイミングとかが問題なのか？
- Comments: 0
- TrackBack (Close): -