mac で coq

coq という証明支援システムについて教えてもらったので、macで環境構築をした。

coqの開発環境を整えるには、

• Download | The Coq Proof Assistant からMac版をダウンロードする
• proofgeneralというemacsプラグインを落とす

という二つの手順を踏むのだが、init.elへproofgeneralを公式から導入しようとすると、次のようなエラーが！

isar/isar-unicode-tokens.el:686:37:Error: the function `isar-markup-ml' is not known to be defined.
make[1]: *** [isar/isar-unicode-tokens.elc] Error 1
make: *** [compile] Error 2

isar-markup-mlという関数がないですよと言われているのだが、どう解決するか。
emacsattic/proofgeneral · GitHub
から、最新版を落とすと、解決する。