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

Question

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. Therefore, I isolate this line of code in the bignum_problem.v file. Then running coqc bignum_problemcauses a response

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

Error: Cannot find the library BigN.

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

Answer 1

, bignum OCaml; coq-bignums. BigN

From Bignums Require Import BigN.