Builtins and relevant files

Rocq-Elpi's API surface (the predicates and data types Elpi code can use to interact with Rocq) is documented in a handful of generated/hand-written .elpi files. Throughout this manual, inline references like coq.say or term link directly to the declaration of a predicate/type inside these files, at the commit the manual was built from.

• coq-builtin.elpi documents the HOAS encoding of Rocq terms and the API to access Rocq. Example roles: coq.say, term, app, @global!.

• coq-builtin-synterp.elpi documents APIs to interact with Rocq at parsing time. Example role: coq.say.

• elpi-builtin.elpi documents Elpi's standard library, you may look here for list processing code. Example roles: std.do! (the std. prefix is stripped before lookup), true (no prefix stripped), int, uvar, std.

• coq-lib.elpi provides some utilities to manipulate Rocq terms; it is an addendum to coq-builtin. Example roles: coq.subst-prod, coq.indt-spec.

• coq-lib-common.elpi. Example roles: coq.parse-attributes, attribute-signature.

• elpi-reduction.elpi. Example role: hd-beta.

• elpi-ltac.elpi the coq.ltac.* bridge to Ltac1. Example role: refine (the coq.ltac. prefix is stripped before lookup, e.g. this links to coq.ltac.refine).

• elpi-command-template.elpi provides the pre-loaded code for Elpi Command (execution phase) and Elpi Tactic.

• elpi-command-template-synterp.elpi provides the pre-loaded code for Elpi Command (parsing phase).

• elpi-tactic-template.elpi provides the pre-loaded code for Elpi Tactic (note tactics also load elpi-command-template.elpi above).