The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

You haven't given enough information for most of us to have any idea how to help you.  Try pasting the full output of the following commands, to be run in the source directory of Coq (you seem to be calling it /coq?):

uname -a

./configure

and then run `make clean` and then run `make VERBOSE=1`, and paste the last 10-15 lines of output here.  I suspect something went wrong in your ./configure process, so seeing the output of that might help diagnose the error.

Also, is this coq-8.4pl3.tar.gz exactly as downloaded from the website, or did you try to apply Vladimir's patches (necessary for his foundations library)?  If you tried to apply his patches, I expect the problem is that his patches are for Coq 8.3, not 8.4.  If you haven't, then I hope that the output from ./configure will help.

-Jason

On Sun, Jan 5, 2014 at 2:04 PM, Bill Richter <richter AT math.northwestern.edu> wrote:

   What version of Coq are you trying to compile? Which distribution
   are you running?

Stéphane, I'm sorry for not including that.  I think I'm using Coq 8.4pl3, which I downloaded as
coq-8.4pl3.tar.gz.

--
Best,
Bill