brew install ssreflect git clone https://github.com/mathink/Cat_on_Coq cd Cat_on_Coq perl -i -pe 's/COC\.//g' *.v perl -i -pe 's/-R \. COC//' _CoqProject make all emacs Functor.v 環境 ProofGeneral Version 4.2.