Quotations

quotation::={%quotation-kind| quotation-body |}quotation-kind::=constropen_constrpretermexpridentqualidvernacquotation-body::=quotation-textantiquotation*constr-quotation::={%constr| quotation-body |}

A quotation of the form {%kind| … |} builds a Rocq term or object in OCaml, using Rocq syntax.

Term quotations

{%expr| quotation-body |}

Returns the concrete syntax tree (CST) of the quoted term from the parser.

{%preterm| quotation-body |}

Builds an untyped preterm from the parsed expr. Unlike expr, preterm have resolved notations, names are qualified, and implicit arguments are made explicit.

{%constr| quotation-body |}

Elaborates the term to a constr by running type-inference on the obtained preterm.

{%open_constr| quotation-body |}

Behaves like {%constr| … |}, except that existential variables (holes) are allowed in the term.

For example, {%open_constr| 1 + _ |} is accepted, while {%constr| 1 + _ |} is rejected.

Other quotations

{%ident| quotation-body |}

Builds a Rocq identifier, following Rocq’s identifier parsing rules.

{%qualid| quotation-body |}

Builds a qualified Rocq identifier, i.e., a list of identifiers separated by dots.

Antiquotations

antiquotation::=%{ ocaml-expr }|%antiquotation-kind:{ ocaml-expr }antiquotation-kind::=constropen_constrpretermexpr

An antiquotation %{x} splices the term x in a quotation. It behaves similarly to $x in Ltac2, but unlike Ltac2, x does not have to be a variable (it can be any valid OCaml expression).

If the kind is not explicitly specified as in e.g. %preterm:{x}, it defaults to the enclosing quotation kind. Hence, x in the %{x} antiquotation is interpreted as a constr in {%constr| … |}, a preterm in {%preterm| … |}, and so on.