>609
Open Scope type_scope.
の１行を最初に書くと私の環境ではコンパイルとおりました。

Coq 8.1pl2 と8.2 でコンパイルが通ったことを確認しました。