Overview

Camltac is a tactic and meta-programming language for the Rocq Prover that lets you write OCaml code within Rocq files. Using Camltac, you can define OCaml tactics and meta-programs, and run them on-the-fly inside your Rocq session.

Writing OCaml code in Camltac comes with all the benefits of OCaml: native performance, a helpful type-system, tooling support, nice ergonomics, and a rich ecosystem of libraries and preprocessors. Moreover, recent versions of OCaml 5 come with support for parallelism and algebraic effects, which lets you express more meta-programs easily.

In addition to regular OCaml features, Camltac provides a few additional ones for writing tactics:

• You can build Rocq terms in Camltac using quotations such as {%constr| … |} (equivalent to Ltac2’s constr:(…));

• Camltac supports antiquotations (%{…}) inside quotations, pattern matching over terms (match%rocq x with), and pattern matching over goals (match%rocq goal with).

• Camltac ships with the entire Ltac2 APIs, and provides the usual tacticals to compose tactics together.

For the motivation behind Camltac and how it compares to Ltac2, OCaml plugins, and other tactic languages, have a look at Why Camltac?.

If you’d like to play immediately with Camltac, the next page shows a few small examples to try out. You can head to Installation to install Camltac.