がcoqideを使用して、コマンドは `インポートBigN`は8.6 COQ使用して働いていた必要とするが、CoQは8.7

Question

に私はのCoQ 8.6でBIGNUM

$ opam upgrade bignum 
Already up-to-date. 

をインストールするためにOPAMを使用していないRequire Import BigN.はCoQは8.7でライブラリをインポートしたが、 Iエラーが発生します。 私は、このコード行をファイルbignum_problem.vに分離します。そして、 coqc bignum_problemを実行すると、Coqのモジュールの応答

File "./bignum_problem.v", line 1, characters 15-19:

Error: Unable to locate library BigN .

ドキュメントを生成し、私はファイルBigN.voを必要とするが、そのようなファイルが.opamディレクトリに表示されていないことを示唆しています。私は何が欠けていますか？

Answer 1

bignumはOCam1ライブラリーを指すと思われます。代わりにcoq-bignumsをインストールすることをお勧めします。私はそのライブラリを自分のマシンにインストールしたので、コマンドでBigNを要求することができました。

From Bignums Require Import BigN.