Search code examples
coqopam

Using coqide, the command `Require Import BigN` worked using coq 8.6 but not in coq 8.7

I used OPAM to install bignum

$ opam upgrade bignum
Already up-to-date.

With coq 8.6 the code Require Import BigN. imported the library but with coq 8.7 I get an error. So I isolate this line of code in a file bignum_problem.v. Then running coqc bignum_problem produces the response

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

Error: Unable to locate library BigN.

The documentation for Coq modules suggests that I need a file BigN.vo but no such file appears in the .opam directory. What am I missing?

Solution

  • It seems that bignum refers to an OCaml library; you might want to install coq-bignums instead. I just installed that library on my machine and was able to require BigN with the command

    From Bignums Require Import BigN.