AffeldtさんのSsreflectチュートリアルのソースをビルドする

目的

https://staff.aist.go.jp/reynald.affeldt/ssrcoq/ にある「Coq/SSReflectファイル」を手元で動かす

必要なもの

• coq-8.4
• ssreflect-1.5 (1.4でもOK?)

手順

次の内容でMakeというファイルを作る。

Make

-R .
bigop2_example.v
group_example.v
predicative_example.v
bigop_example.v
ssrbool_example.v
dependent_example.v
logic_example.v
ssrnat_example.v
eqtype_example.v
tactics_example.v
finset_example.v
matrix_example.v
tuple_example.v
fintype_example.v
permutation_example.v
view_example.v

次を実行

sh

coq_makefile -f Make -o Makefile