coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Dominic Mulligan <dominic.p.mulligan AT googlemail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Building the Containers library
- Date: Fri, 12 Oct 2012 11:43:58 +0100
Hi,
I am trying to install Lescuyer's Containers library with Coq 8.4:
coqtop --version
The Coq Proof Assistant, version 8.4 (October 2012)
compiled on Oct 12 2012 10:02:11 with OCaml 3.12.1
Downloading the source tar ball and performing a "make -j" I get the
following:
make -j
...
File "src/generate.ml", line 45, characters 35-58:
Error: Unbound module Rawterm
make: *** [src/generate.cmxs] Error 2
make: *** Waiting for unfinished jobs....
Identifier 'UsualOrderedType' now a keyword
File "src/generate.ml", line 45, characters 35-58:
Error: Unbound module Rawterm
make: *** [src/generate.cmo] Error 2
File "src/generate.ml", line 45, characters 35-58:
Error: Unbound module Rawterm
make: *** [src/generate.cmx] Error 2
I can't seem to find reference to this problem elsewhere, which suggests
maybe I am doing something wrong.
Can anybody shed some light on what is happening here?
Dominic
- [Coq-Club] Building the Containers library, Dominic Mulligan, 10/12/2012
- Re: [Coq-Club] Building the Containers library, Guillaume Melquiond, 10/12/2012
- Re: [Coq-Club] Building the Containers library, Dominic Mulligan, 10/12/2012
- Re: [Coq-Club] Building the Containers library, Guillaume Melquiond, 10/12/2012
Archive powered by MHonArc 2.6.18.