The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Thu, Mar 11, 2010 at 12:45:26PM +0300, Evgeny Makarov wrote:
> Dear Coq users,
> 
> When trying to compile Coq trunk rev. 12704 I am getting the following 
> error:
> 
> OCAMLDEP4 parsing/g_constr.ml4
> Error: don't know what to do with pa_extend.cmo
> 

Hi Evgeny,

I've been unable to reproduce this error, even with ocaml 3.10.1 and
coq r12704. Which camlp5 are you using (mine is 5.11) ? What happen
if you try something like:

camlp5o -I .  pr_o.cmo pa_extend.cmo -loc loc -impl parsing/g_constr.ml4 -o 
parsing/g_constr.ml

If you get an error, I suspect there's something wrong with your
camlp5 installation. Otherwise, could you please try again with
"make VERBOSE=1" and get the precise camp4o command which is tried ?

Best regards,

Pierre Letouzey