Search code examples
coq

Reference in Coq Lists library not found

I'm trying to use the concat function as it appears in https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html. I tried the following:

Require Import Arith Coq.Lists.List.
Import ListNotations.

Definition CON (l : list nat):= (concat [[0]; l]).

but I get the error Error: The reference concat was not found in the current environment. I thought this should work since I've already imported the library, so I don't know where this error comes from.

I'm using version 8.4pl3 (January 2014). Could be a version issue?

Solution

  • concat was added in this commit. I think it was close to the end of the 8.4pl3 release so it was not pushed to the release, but rather to the next 8.5