8.2 と 8.3 の互換性

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

Theorem eq_diff_0 (n m: nat) : n = m -> n - m = 0.

という定理を証明しようとすると，8.2 では

============================
   forall n m : nat, n = m -> n - m = 0

で開始されますが，8.3 では

   n : nat
   m : nat
============================
   n = m -> n - m = 0

で開始されてしまいます．

互換性に関する公式の情報によると， -compat 8.2 というオプションを追加すると動作するらしいのですが， 新しいプログラムに混ぜて再利用するときには不都合なので， とりあえず，

Ltac gen_clear := repeat (match goal with [x:_|-_] => generalize x; clear x end).

という tactic を定義して， 動作しなくなった全ての証明の始めのところに gen_clear を追加することで解決できました． こういう仕様変更って，ユーザは困らないのかなぁ…．