package rocq-camltac

Camltac is an OCaml plugin for Rocq that lets you run OCaml code within Rocq scripts. Camltac makes it possible to define OCaml meta-programs and tactics, and run them in the current Rocq state without the friction and boilerplate of setting up a plugin.

Camltac is both a tactic and a meta-programming language:

• As a tactic language, Camltac provides constructs inspired by Ltac2, including term quotations ({%constr| … |}), pattern matching (match%rocq), and antiquotations using ppx_rocq. Camltac makes it easy to define new tactics by providing the usual tacticals from Ltac2, and a dedicated FFI with Ltac and Ltac2.

• As a meta-programming language, Camltac offers a complete meta-programming experience by allowing access to Rocq's internal APIs and state. To ensure stability, Camltac includes the Ltac2 APIs which provide a simple entry point to meta-programming in OCaml.