CODEWITHSUNDEEP
coqopam
Barry Jay
Barry Jay

Reputation: 73

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?

Upvotes: 4

Views: 161

Answers (1)

Arthur Azevedo De Amorim
Arthur Azevedo De Amorim

Reputation: 23602

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.

Upvotes: 6

Related Questions