The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

On Mon, Nov 7, 2011 at 7:21 AM, Daniel de Rauglaudre
<daniel.de_rauglaudre AT inria.fr>
 wrote:
> Hi,
>
> On Mon, Nov 07, 2011 at 11:14:44AM +0100, Gyesik Lee wrote:
>
>> OCAMLC4   parsing/pcoq.ml4
>> File "parsing/pcoq.ml4", line 749, characters 8-300:
>> Error: The constructor Gramext.Slist1sep expects 3 argument(s),
>>        but is applied here to 2 argument(s)
>
> Perhaps a problem of version of Camlp5. Which version do you have ?
> (type "camlp5 -v"). Perhaps its version is not compatible with this
> version of Coq, because too old or too new.
>
Sorry to bring back a not so recent thread, but this information
should be useful for other people having trouble compiling Coq 8.2pl2
with new versions of Camlp5.

I had the same problem on Ubuntu 11.10 with Ocaml version 3.12.0 and
Camlp5 version 6.02.2. There is, however, a patch by Stéphane Glondu
in the Debian repository targeted exactly at this problem:

You can get it by clicking the "raw" link on this page:
wget 
http://anonscm.debian.org/gitweb/?p=pkg-ocaml-maint/packages/coq.git;a=blob_plain;f=debian/patches/0003-Fix-build-with-camlp5-6.02.1.patch;hb=6b3bd571d555c4db91ab210da9a302b2f2181e23

And apply it in your coq-8.2pl2 dir like this:
patch -p1 < debian_patches_0003-Fix-build-with-camlp5-6.02.1.patch

This did the job for me, hope it works for others as well.

Regards,
Catalin