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?

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.