Coq: Error: Unable to locate library Coq.extraction.Extraction

0
votes

I'm taking the "Software foundations" course. Can't run the "Extraction" chapter. It fail on the first line Require Coq.extraction.Extraction. with the message Coq: Error: Unable to locate library Coq.extraction.Extraction.

I'm running it in CoqIde.

coqc -v: The Coq Proof Assistant, version 8.6 (October 2017) compiled on Oct 28 2017 14:23:55 with OCaml 4.05.0

CoqIde version: 8.6

CoqTop arguments: -Q /home/evgenii/mysources/coq/coq-excercises/lf LF

What am I missing?

1
coq

1 Answers

2
votes

Try replacing that line with Require Extraction. (Coq.extraction.Extraction seems to be a backwards-incompatible form.)

8.6 is pretty old, so you might have other compatibility problems if that doesn't match the version used by your distribution of Software Foundations. Have a look in Preface.v for the expected Coq version, and consider upgrading if there is a mismatch.