My understanding (please correct me if I'm wrong) is that Coq uses camlp{4,5} only as an extensible parser library in order to parse its own language (which can be extended with user-defined notations). In particular, Coq does not use the following camlp{4,5} features:

This is not entirely correct. Coq uses camlp4's extensible ocaml syntax in quite a bit of its code. (though less than it use to, I hear). The following features are used:

- the alternative representation of OCaml AST
- the Camlp4 grammar definitions for OCaml syntax(es)
- quotations/antiquotations to produce fragments of the OCaml AST
- OCaml syntax extensions to define grammar entries
- custom OCaml syntax extension for the Coq source code itself

Though quotations are used *very* sparsely (mostly in legacy code, they are not maintained).

Arnaud Spiwack