http://hal.archives-ouvertes.fr/docs/00/40/77/78/PDF/RT-367.pdf のざっくりした訳 方針 正確な訳にするよりも、意味がつかめる訳に。(時間がないので) パラグラフは崩さない 訳語の統一とかはあとで考える tacticもtacticsもタクティクスと訳してしまってるのは、あとでなんとかします。 イントロダクション ssreflectはCoqをベースにした言語です SSreflectはCoqをベースにした証明を行なうための形式言語です。Coqを定義言語と使いつつ、追加のタクティクス(推論や長い証明を書くのに便利なやつ)を提供します。 また既にこの拡張は非常に効果的であると実証されています。(参考: ssreflectを利用した4色定理の証明) ssreflectの追加したタクティクスはほとんどありません。ただし各タクティクスを組合せ