2012-05-25から1日間の記事一覧

8.2 と 8.3 の互換性

Coq

久しぶりに Coq を触ったら, 昔書いた Coq のソースプログラムが通らなくなっていました. いろいろ原因を探ってみたところ, Coq 8.2 と Coq 8.3 で, 証明の開始時点での goal の形式が変わったためのようです. たとえば,Theorem eq_diff_0 (n m: nat) …