The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,

It's in a way or the other my fault.

(I suspect that spaces in path under window is the problem but let's be more carreful)

Can we continue the discution in this bug thread : https://coq.inria.fr/bugs/show_bug.cgi?id=2804#c1 ?

Pierre

Le 4 juin 12 à 03:37, Jason Gross a écrit :

I've tried deleting Makefile.coq, along with all the other files except for 'Makefile' and the *.v files, and I still get the same error.  I also get the error when running 'make clean'.

-Jason

On Sun, Jun 3, 2012 at 9:04 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

Jason Gross wrote:

I just switched from Coq 8.3pl3 to Coq 8.4beta2, and the Makefile I used for the project I'm working on no longer works; when I run make, I get
$ make
make -f Makefile.coq
make[1]: Entering directory `/cygdrive/d/Documents/Dropbox/MIT/2012 Summer/Categorical Informatics UROP/catdb'
Makefile.coq:34: *** missing separator.  Stop.
make[1]: Leaving directory `/cygdrive/d/Documents/Dropbox/MIT/2012 Summer/Categorical Informatics UROP/catdb'
Makefile:7: recipe for target `coq' failed
make: *** [coq] Error 2

Probably all you need to do is delete Makefile.coq before running 'make'.