Coq 8.2 リリース!

Coqがversion 8.1から8.2にバージョンアップしました。変更点は以下のいろいろ。

  • Haskellのような type class system が導入されました
  • coqcでコンパイル後のvoファイル を扱うcoqchkというツールが追加されました
  • Setoidのための書き換えタクティック setoid_rewrite が追加されました。
  • 再帰関数をFixpointで定義するときに、停止性を担保する引数を {struct hoge}のように書かなくてもよくなりました(もちろん書いてもよいです)
  • Agdaのような "forall {A}, P" という構文sugerが導入されました。"Implicit Arguments t [A]." という1行を書かなくてもよくなります
  • ExtractionOCamlのコードを生成する場合にlistとpairはそれぞれOCamlのlistとpairに賢く対応するようになりました
  • 有限集合に関するライブラリFSet, FMapあたりが大きく変わりました
  • CoqIDEのデフォルトフォントが変わりました
  • 最新のOCaml 3.11に対応しました
  • etc...

早速ダウンロードしよう!
http://coq.inria.fr/distrib-eng.html