ssrnatはCoq 8.7に含まれていますか？

Question

Coq 8.7は一般的なSsreflectライブラリを統合しています。そのライブラリは、したがって、次のようにインポートすることができます。

From Coq Require Import ssreflect ssrfun ssrbool. 

しかし、私はssrnatをインポートしようとすると、それはそれはUnable to locate library ssrnat with prefix Coqだと文句を言い、私はどちらかのディスク上のCoqの分布のssrnatを見つけることができません。 ssrnatは何らかの理由で意図的に含まれていなかったか、別のモジュールにフォルダが含まれていたか、インストールに何か問題がありましたか？いつの日か、我々はより多くのライブラリがデフォルトで用意されてい拡張配布を提供したいと考えていますが、

Answer 1

ssrnatは、メインのCoqのディストリビューションに含まれていません。

Coq 8.7では、戦術言語自体ssreflectに加えて、いくつかの基本的なサポートライブラリssrfun ssrboolが含まれていました。

ssrnatは数学的な数学的な階層を利用しているので、これはもっと「侵略的な」変化です。

幸いにして、含まれているプラ​​グインのおかげで、ssrnatのインストールは非常に簡単な作業です。