The Coq mailing list

[Jeehoon Kang <jeehoon.kang AT sf.snu.ac.kr>]

Dear Ralf,

I also wonder if how I can check which of camlp4 or camlp5 is used in my Coq binary..  But if you installed Coq via opam or from tarball, it is highly likely that your Coq uses camlp5.  It is the default option.

Note that you can `opam install coq.8.5.2~camlp4` to obtain the camlp4-based version of Coq.

Jeehoon

2016-08-03 18:37 GMT+09:00 Ralf Jung <jung AT mpi-sws.org>:

Hi,

> Those warnings are not produced by Coq, but rather by CAMLP4/5, and
> therefore the warning mechanism is useless here.
>
> Warnings cannot be turned off in CAMLP4 because the relevant API has
> been missing for ages, whereas it is possible in CAMLP5 (if they appear
> in Coq otherwise it's a bug, and it may well be one in your example). In
> any case, I advise you to switch to CAMLP5 if you didn't do so already.

It seems I have both CAMLP4 and CAMLP5 installed. How can I tell which
one Coq is using? "coqc --version" only shows the ocaml version:

> $ coqc --version
> The Coq Proof Assistant, version 8.5pl2 (July 2016)
> compiled on Jul 21 2016 11:30:45 with OCaml 4.02.3

Kind regards,
Ralf

--

Jeehoon Kang (Ph.D. student)

Software Foundations Laboratory

Seoul National University