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 を追加することで解決できました. こういう仕様変更って,ユーザは困らないのかなぁ….