Camltac is an OCaml plugin for Rocq that lets you write OCaml meta-programs and tactics directly inside Rocq scripts.
| Repository | Description |
|---|---|
| Camltac | The Camltac plugin: OCaml as a Tactic Language for the Rocq Prover. |
| ppx_rocq | PPX syntax extensions for quoting Rocq terms in OCaml. |
| MLtac2 | Ltac2 APIs for OCaml. |
See the Camltac README for installation instructions and a quickstart, or the tour of Camltac for an overview of its features.
