使用coqide,命令`Require Import BigN`使用coq 8.6但不在coq 8.7中工作

Question

我用OPAM来安装bignum

$ opam upgrade bignum
Already up-to-date.

使用coq 8.6,代码Require Import BigN.导入了库,但是使用coq 8.7我得到了一个错误.所以我在文件bignum_problem.v中隔离了这行代码.然后运行 coqc bignum_problem产生响应

文件"./bignum_problem.v",第1行,字符15-19:

错误:无法找到库BigN.

Coq模块的文档表明我需要一个文件BigN.vo但是.opam目录中没有这样的文件.我错过了什么？

Answer 1

它似乎bignum指的是一个OCaml库; 你可能想要安装coq-bignums.我刚刚在我的机器上安装了该库,并且可以BigN使用该命令

From Bignums Require Import BigN.